Documentation

Mathlib.CategoryTheory.FiberedCategory.Cartesian

Cartesian morphisms #

This file defines cartesian resp. strongly cartesian morphisms with respect to a functor p : 𝒳 ⥤ 𝒮.

Main definitions #

IsCartesian p f φ expresses that φ is a cartesian morphism lying over f with respect to p in the sense of SGA 1 VI 5.1. This means that for any morphism φ' : a' ⟶ b lying over f there is a unique morphism τ : a' ⟶ a lying over 𝟙 R, such that φ' = τ ≫ φ.

IsStronglyCartesian p f φ expresses that φ is a strongly cartesian morphism lying over f with respect to p, see https://stacks.math.columbia.edu/tag/02XK.

Implementation #

The constructor of IsStronglyCartesian has been named universal_property', and is mainly intended to be used for constructing instances of this class. To use the universal property, we generally recommended to use the lemma IsStronglyCartesian.universal_property instead. The difference between the two is that the latter is more flexible with respect to non-definitional equalities.

References #

class CategoryTheory.Functor.IsCartesian {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) extends CategoryTheory.Functor.IsHomLift :

The proposition that a morphism φ : a ⟶ b in 𝒳 lying over f : R ⟶ S in 𝒮 is a cartesian morphism.

See SGA 1 VI 5.1.

cond : CategoryTheory.IsHomLiftAux p f φ
universal_property : ∀ {a' : 𝒳} (φ' : a' ⟶ b) [inst : p.IsHomLift f φ'], ∃! χ : a' ⟶ a, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

Instances

theorem CategoryTheory.Functor.IsCartesian.universal_property {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :

∃! χ : a' ⟶ a, p.IsHomLift (CategoryTheory.CategoryStruct.id R) χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

class CategoryTheory.Functor.IsStronglyCartesian {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) extends CategoryTheory.Functor.IsHomLift :

The proposition that a morphism φ : a ⟶ b in 𝒳 lying over f : R ⟶ S in 𝒮 is a strongly cartesian morphism.

See https://stacks.math.columbia.edu/tag/02XK

cond : CategoryTheory.IsHomLiftAux p f φ
universal_property' : ∀ {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [inst : p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'], ∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

Instances

theorem CategoryTheory.Functor.IsStronglyCartesian.universal_property' {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] {p : CategoryTheory.Functor 𝒳 𝒮} {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCartesian f φ] {a' : 𝒳} (g : p.obj a' ⟶ R) (φ' : a' ⟶ b) [p.IsHomLift (CategoryTheory.CategoryStruct.comp g f) φ'] :

∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

noncomputable def CategoryTheory.Functor.IsCartesian.map {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :

a' ⟶ a

Given a cartesian morphism φ : a ⟶ b lying over f : R ⟶ S in 𝒳, and another morphism φ' : a' ⟶ b which also lifts f, then IsCartesian.map f φ φ' is the morphism a' ⟶ a lifting 𝟙 R obtained from the universal property of φ.

Equations

CategoryTheory.Functor.IsCartesian.map p f φ φ' = Classical.choose ⋯

Instances For

instance CategoryTheory.Functor.IsCartesian.map_isHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :

p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.map p f φ φ')

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.IsCartesian.fac_assoc {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] {Z : 𝒳} (h : b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ') (CategoryTheory.CategoryStruct.comp φ h) = CategoryTheory.CategoryStruct.comp φ' h

@[simp]

theorem CategoryTheory.Functor.IsCartesian.fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCartesian.map p f φ φ') φ = φ'

theorem CategoryTheory.Functor.IsCartesian.map_uniq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsHomLift f φ'] (ψ : a' ⟶ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ] (hψ : CategoryTheory.CategoryStruct.comp ψ φ = φ') :

ψ = CategoryTheory.Functor.IsCartesian.map p f φ φ'

Given a cartesian morphism φ : a ⟶ b lying over f : R ⟶ S in 𝒳, and another morphism φ' : a' ⟶ b which also lifts f. Then any morphism ψ : a' ⟶ a lifting 𝟙 R such that g ≫ ψ = φ' must equal the map induced from the universal property of φ.

theorem CategoryTheory.Functor.IsCartesian.ext {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (ψ : a' ⟶ a) (ψ' : a' ⟶ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ] [p.IsHomLift (CategoryTheory.CategoryStruct.id R) ψ'] (h : CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.comp ψ' φ) :

ψ = ψ'

Given a cartesian morphism φ : a ⟶ b lying over f : R ⟶ S in 𝒳, and two morphisms ψ ψ' : a' ⟶ a such that ψ ≫ φ = ψ' ≫ φ. Then we must have ψ = ψ'.

@[simp]

theorem CategoryTheory.Functor.IsCartesian.map_self {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] :

CategoryTheory.Functor.IsCartesian.map p f φ φ = CategoryTheory.CategoryStruct.id a

noncomputable def CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :

a' ≅ a

The canonical isomorphism between the domains of two cartesian morphisms lying over the same object.

Equations

One or more equations did not get rendered due to their size.

Instances For

instance CategoryTheory.Functor.IsCartesian.of_iso_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : 𝒳} (φ' : a' ≅ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ'.hom] :

p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ'.hom φ)

Precomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.

Equations

⋯ = ⋯

instance CategoryTheory.Functor.IsCartesian.of_comp_iso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {b' : 𝒳} (φ' : b ≅ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ'.hom] :

p.IsCartesian f (CategoryTheory.CategoryStruct.comp φ φ'.hom)

Postcomposing a cartesian morphism with an isomorphism lifting the identity is cartesian.

Equations

⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCartesian.universal_property {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) (f' : R' ⟶ S) (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

∃! χ : a' ⟶ a, p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp χ φ = φ'

The universal property of a strongly cartesian morphism.

This lemma is more flexible with respect to non-definitional equalities than the field universal_property' of IsStronglyCartesian.

instance CategoryTheory.Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] :

p.IsCartesian f φ

Equations

⋯ = ⋯

noncomputable def CategoryTheory.Functor.IsStronglyCartesian.map {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

a' ⟶ a

Given a diagram

a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S

such that φ is strongly cartesian, and a morphism φ' : a' ⟶ b. Then map is the map a' ⟶ a lying over g obtained from the universal property of φ.

Equations

CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ' = Classical.choose ⋯

Instances For

instance CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

p.IsHomLift g (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ')

Equations

⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.IsStronglyCartesian.fac_assoc {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] {Z : 𝒳} (h : b ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ') (CategoryTheory.CategoryStruct.comp φ h) = CategoryTheory.CategoryStruct.comp φ' h

@[simp]

theorem CategoryTheory.Functor.IsStronglyCartesian.fac {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ') φ = φ'

theorem CategoryTheory.Functor.IsStronglyCartesian.map_uniq {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryTheory.CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] (ψ : a' ⟶ a) [p.IsHomLift g ψ] (hψ : CategoryTheory.CategoryStruct.comp ψ φ = φ') :

ψ = CategoryTheory.Functor.IsStronglyCartesian.map p f φ hf' φ'

Given a diagram

a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S

such that φ is strongly cartesian, and morphisms φ' : a' ⟶ b, ψ : a' ⟶ a such that ψ ≫ φ = φ'. Then ψ is the map induced by the universal property.

theorem CategoryTheory.Functor.IsStronglyCartesian.ext {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {a' : 𝒳} (g : R' ⟶ R) {ψ : a' ⟶ a} {ψ' : a' ⟶ a} [p.IsHomLift g ψ] [p.IsHomLift g ψ'] (h : CategoryTheory.CategoryStruct.comp ψ φ = CategoryTheory.CategoryStruct.comp ψ' φ) :

ψ = ψ'

Given a diagram

a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S

such that φ is strongly cartesian, and morphisms ψ ψ' : a' ⟶ a such that g ≫ ψ = φ' = g ≫ ψ'. Then we have that ψ = ψ'.

@[simp]

theorem CategoryTheory.Functor.IsStronglyCartesian.map_self {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] :

CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ = CategoryTheory.CategoryStruct.id a

@[simp]

theorem CategoryTheory.Functor.IsStronglyCartesian.map_comp_map_assoc {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {R'' : 𝒮} {a' : 𝒳} {a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'} (H : f' = CategoryTheory.CategoryStruct.comp g f) (H' : f'' = CategoryTheory.CategoryStruct.comp g' f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b) [p.IsStronglyCartesian f' φ'] [p.IsHomLift f'' φ''] {Z : 𝒳} (h : a ⟶ Z) :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ'') h

@[simp]

theorem CategoryTheory.Functor.IsStronglyCartesian.map_comp_map {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : 𝒮} {R'' : 𝒮} {a' : 𝒳} {a'' : 𝒳} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'} (H : f' = CategoryTheory.CategoryStruct.comp g f) (H' : f'' = CategoryTheory.CategoryStruct.comp g' f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b) [p.IsStronglyCartesian f' φ'] [p.IsHomLift f'' φ''] :

CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCartesian.map p f' φ' H' φ'') (CategoryTheory.Functor.IsStronglyCartesian.map p f φ H φ') = CategoryTheory.Functor.IsStronglyCartesian.map p f φ ⋯ φ''

When its possible to compare the two, the composition of two IsCocartesian.map will also be given by a IsCocartesian.map. In other words, given diagrams

a''         a'        a --φ--> b          a' --φ'--> b          a'' --φ''--> b
|           |         |        |    and   |          |    and   |            |
v           v         v        v          v          v          v            v
R'' --g'--> R' --g--> R --f--> S          R' --f'--> S          R'' --f''--> S

such that φ and φ' are strongly cartesian morphisms. Then composing the induced map from a'' ⟶ a' with the induced map from a' ⟶ a gives the induced map from a'' ⟶ a.

instance CategoryTheory.Functor.IsStronglyCartesian.comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {T : 𝒮} {a : 𝒳} {b : 𝒳} {c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c} [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian g ψ] :

p.IsStronglyCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)

Given two strongly cartesian morphisms φ, ψ as follows

a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T

Then the composite φ ≫ ψ is also strongly cartesian.

Equations

⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCartesian.of_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {T : 𝒮} {a : 𝒳} {b : 𝒳} {c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c} [p.IsStronglyCartesian g ψ] [p.IsStronglyCartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)] [p.IsHomLift f φ] :

p.IsStronglyCartesian f φ

Given two commutative squares

a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T

such that φ ≫ ψ and ψ are strongly cartesian, then so is φ.

instance CategoryTheory.Functor.IsStronglyCartesian.of_iso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift f φ.hom] :

p.IsStronglyCartesian f φ.hom

Equations

⋯ = ⋯

instance CategoryTheory.Functor.IsStronglyCartesian.of_isIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] [CategoryTheory.IsIso φ] :

p.IsStronglyCartesian f φ

Equations

⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCartesian.isIso_of_base_isIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {S : 𝒮} {a : 𝒳} {b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] [CategoryTheory.IsIso f] :

CategoryTheory.IsIso φ

A strongly cartesian morphism lying over an isomorphism is an isomorphism.

noncomputable def CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso {𝒮 : Type u₁} {𝒳 : Type u₂} [CategoryTheory.Category.{v₁, u₁} 𝒮] [CategoryTheory.Category.{v₂, u₂} 𝒳] (p : CategoryTheory.Functor 𝒳 𝒮) {R : 𝒮} {R' : 𝒮} {S : 𝒮} {a : 𝒳} {a' : 𝒳} {b : 𝒳} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryTheory.CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :

a' ≅ a

The canonical isomorphism between the domains of two strongly cartesian morphisms lying over isomorphic objects.

Equations

One or more equations did not get rendered due to their size.

Instances For