Cocartesian morphisms

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

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

Main definitions

IsCocartesian p f φ expresses that φ is a cocartesian morphism lying over f : R ⟶ S with respect to p. This means that for any morphism φ' : a ⟶ b' lying over f there is a unique morphism τ : b ⟶ b' lying over 𝟙 S, such that φ' = φ ≫ τ.

IsStronglyCocartesian p f φ expresses that φ is a strongly cocartesian morphism lying over f with respect to p.

Implementation

The constructor of IsStronglyCocartesian 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 IsStronglyCocartesian.universal_property instead. The difference between the two is that the latter is more flexible with respect to non-definitional equalities.

class CategoryTheory.Functor.IsCocartesian {𝒮 : 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 cocartesian if for all morphisms φ' : a ⟶ b', also lying over f, there exists a unique morphism χ : b ⟶ b' lifting 𝟙 S such that φ' = φ ≫ χ.

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

theorem CategoryTheory.Functor.IsCocartesian.universal_property {𝒮 : Type u₁} {𝒳 : Type u₂} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [inst_2 : p.IsHomLift f φ'], ∃! χ : b ⟶ b', p.IsHomLift (CategoryTheory.CategoryStruct.id S) χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'

class CategoryTheory.Functor.IsStronglyCocartesian {𝒮 : 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 cocartesian if for all morphisms φ' : a ⟶ b' and all diagrams of the form

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

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

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

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

theorem CategoryTheory.Functor.IsStronglyCocartesian.universal_property' {𝒮 : Type u₁} {𝒳 : Type u₂} : ∀ {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳} {p : CategoryTheory.Functor 𝒳 𝒮} {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) {φ : a ⟶ b} [self : p.IsStronglyCocartesian f φ] {b' : 𝒳} (g : S ⟶ p.obj b') (φ' : a ⟶ b') [inst_2 : p.IsHomLift (CategoryTheory.CategoryStruct.comp f g) φ'], ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'

noncomputable def CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] : b ⟶ b'

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

Equations

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

instance CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] : p.IsHomLift (CategoryTheory.CategoryStruct.id S) (CategoryTheory.Functor.IsCocartesian.map p f φ φ')

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.IsCocartesian.map p f φ φ') = φ'

@[simp]

theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] {Z : 𝒳} (h : b' ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsCocartesian.map p f φ φ') h) = CategoryTheory.CategoryStruct.comp φ' h

theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] (ψ : b ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ] (hψ : CategoryTheory.CategoryStruct.comp φ ψ = φ') : ψ = CategoryTheory.Functor.IsCocartesian.map p f φ φ'

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

theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (ψ : b ⟶ b') (ψ' : b ⟶ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ] [p.IsHomLift (CategoryTheory.CategoryStruct.id S) ψ'] (h : CategoryTheory.CategoryStruct.comp φ ψ = CategoryTheory.CategoryStruct.comp φ ψ') : ψ = ψ'

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

@[simp]

theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] : CategoryTheory.Functor.IsCocartesian.map p f φ φ = CategoryTheory.CategoryStruct.id b

noncomputable def CategoryTheory.Functor.IsCocartesian.codomainUniqueUpToIso {𝒮 : 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.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsCocartesian f φ'] : b ≅ b'

The canonical isomorphism between the codomains of two cocartesian morphisms lying over the same object.

Equations

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

instance CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {b' : 𝒳} (φ' : b ≅ b') [p.IsHomLift (CategoryTheory.CategoryStruct.id S) φ'.hom] : p.IsCocartesian f (CategoryTheory.CategoryStruct.comp φ φ'.hom)

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

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f φ] {a' : 𝒳} (φ' : a' ≅ a) [p.IsHomLift (CategoryTheory.CategoryStruct.id R) φ'.hom] : p.IsCocartesian f (CategoryTheory.CategoryStruct.comp φ'.hom φ)

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

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') (f' : R ⟶ S') (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : ∃! χ : b ⟶ b', p.IsHomLift g χ ∧ CategoryTheory.CategoryStruct.comp φ χ = φ'

The universal property of a strongly cocartesian morphism.

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

instance CategoryTheory.Functor.IsStronglyCocartesian.isCocartesian_of_isStronglyCocartesian {𝒮 : 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.IsStronglyCocartesian f φ] : p.IsCocartesian f φ

Equations

• ⋯ = ⋯

noncomputable def CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : b ⟶ b'

Given a diagram

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

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

Equations

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

instance CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : p.IsHomLift g (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ')

Equations

• ⋯ = ⋯

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ') = φ'

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] {Z : 𝒳} (h : b' ⟶ Z) : CategoryTheory.CategoryStruct.comp φ (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ') h) = CategoryTheory.CategoryStruct.comp φ' h

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryTheory.CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] (ψ : b ⟶ b') [p.IsHomLift g ψ] (hψ : CategoryTheory.CategoryStruct.comp φ ψ = φ') : ψ = CategoryTheory.Functor.IsStronglyCocartesian.map p f φ hf' φ'

Given a diagram

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

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

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') {ψ : b ⟶ b'} {ψ' : b ⟶ b'} [p.IsHomLift g ψ] [p.IsHomLift g ψ'] (h : CategoryTheory.CategoryStruct.comp φ ψ = CategoryTheory.CategoryStruct.comp φ ψ') : ψ = ψ'

Given a diagram

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

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

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] : CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ = CategoryTheory.CategoryStruct.id b

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {S'' : 𝒮} {b' : 𝒳} {b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'} {g' : S' ⟶ S''} (H : f' = CategoryTheory.CategoryStruct.comp f g) (H' : f'' = CategoryTheory.CategoryStruct.comp f' g') (φ' : a ⟶ b') (φ'' : a ⟶ b'') [p.IsStronglyCocartesian f' φ'] [p.IsHomLift f'' φ''] : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ H φ') (CategoryTheory.Functor.IsStronglyCocartesian.map p f' φ' H' φ'') = CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ''

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

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

and

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

and

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

such that φ and φ' are strongly cocartesian morphisms, and such that f' = f ≫ g and f'' = f' ≫ g'. Then composing the induced map from b ⟶ b' with the induced map from b' ⟶ b'' gives the induced map from b ⟶ b''.

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] {S' : 𝒮} {S'' : 𝒮} {b' : 𝒳} {b'' : 𝒳} {f' : R ⟶ S'} {f'' : R ⟶ S''} {g : S ⟶ S'} {g' : S' ⟶ S''} (H : f' = CategoryTheory.CategoryStruct.comp f g) (H' : f'' = CategoryTheory.CategoryStruct.comp f' g') (φ' : a ⟶ b') (φ'' : a ⟶ b'') [p.IsStronglyCocartesian f' φ'] [p.IsHomLift f'' φ''] {Z : 𝒳} (h : b'' ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ H φ') (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f' φ' H' φ'') h) = CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.IsStronglyCocartesian.map p f φ ⋯ φ'') h

instance CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] [p.IsStronglyCocartesian g ψ] : p.IsStronglyCocartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)

Given two strongly cocartesian morphisms φ, ψ as follows

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

Then the composite φ ≫ ψ is also strongly cocartesian.

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] [p.IsStronglyCocartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)] [p.IsHomLift g ψ] : p.IsStronglyCocartesian g ψ

Given two commutative squares

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

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

instance CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ.hom

Equations

• ⋯ = ⋯

instance CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ

Equations

• ⋯ = ⋯

theorem CategoryTheory.Functor.IsStronglyCocartesian.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.IsStronglyCocartesian f φ] [CategoryTheory.IsIso f] : CategoryTheory.IsIso φ

A strongly cocartesian arrow lying over an isomorphism is an isomorphism.

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

The canonical isomorphism between the codomains of two strongly cocartesian arrows lying over isomorphic objects.

Equations

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