Cartesian morphisms

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

This file has been adapted to FiberedCategory/Cocartesian, please try to change them in sync.

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

• A. Grothendieck, M. Raynaud, SGA 1
• Stacks: Fibred Categories

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 : Prop

A morphism φ : a ⟶ b in 𝒳 lying over f : R ⟶ S in 𝒮 is cartesian if for all morphisms φ' : a' ⟶ b, also lying over f, there exists a unique morphism χ : a' ⟶ a lifting 𝟙 R such that φ' = χ ≫ φ.

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 χ φ = φ'

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 : Prop

A morphism φ : a ⟶ b in 𝒳 lying over f : R ⟶ S in 𝒮 is strongly cartesian if for all morphisms φ' : a' ⟶ b and all diagrams of the form

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

such that φ' lifts g ≫ f, there exists a lift χ of g such that φ' = χ ≫ φ.

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 χ φ = φ'

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 ⋯

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.

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 ⋯

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 IsStronglyCartesian.map will also be given by a IsStronglyCartesian.map. In other words, given diagrams

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

and

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

and

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

such that φ and φ' are strongly cartesian morphisms, and such that f' = g ≫ f and f'' = g' ≫ f'. 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.