Co-Cartesian morphisms

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

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

Main definitions

IsCocartesian p f φ expresses that φ is a co-Cartesian 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 co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) extends p.IsHomLift f φ : Prop

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

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

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

A morphism φ : a ⟶ b in 𝒳 lying over f : R ⟶ S in 𝒮 is strongly co-Cartesian 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 φ' = χ ≫ φ.

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

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

Given a co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {b' : 𝒳} (φ' : a ⟶ b') [p.IsHomLift f φ'] : p.IsHomLift (CategoryStruct.id S) (IsCocartesian.map p f φ φ')

@[simp]

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

@[simp]

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

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

Given a co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {b' : 𝒳} (ψ ψ' : b ⟶ b') [p.IsHomLift (CategoryStruct.id S) ψ] [p.IsHomLift (CategoryStruct.id S) ψ'] (h : CategoryStruct.comp φ ψ = CategoryStruct.comp φ ψ') : ψ = ψ'

Given a co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] : IsCocartesian.map p f φ φ = CategoryStruct.id b

noncomputable def CategoryTheory.Functor.IsCocartesian.codomainUniqueUpToIso {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : 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 co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] {b' : 𝒳} (φ' : b ≅ b') [p.IsHomLift (CategoryStruct.id S) φ'.hom] : p.IsCocartesian f (CategoryStruct.comp φ φ'.hom)

Postcomposing a co-Cartesian morphism with an isomorphism lifting the identity is co-Cartesian.

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

Precomposing a co-Cartesian morphism with an isomorphism lifting the identity is co-Cartesian.

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

The universal property of a strongly co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] : p.IsCocartesian f φ

noncomputable def CategoryTheory.Functor.IsStronglyCocartesian.map {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = 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 co-Cartesian, 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} {g : S ⟶ S'} {f' : R ⟶ S'} (hf' : f' = CategoryStruct.comp f g) (φ' : a ⟶ b') [p.IsHomLift f' φ'] : p.IsHomLift g (map p f φ hf' φ')

@[simp]

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

@[simp]

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

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

Given a diagram

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

such that φ is strongly co-Cartesian, 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCocartesian f φ] {S' : 𝒮} {b' : 𝒳} (g : S ⟶ S') {ψ ψ' : b ⟶ b'} [p.IsHomLift g ψ] [p.IsHomLift g ψ'] (h : CategoryStruct.comp φ ψ = CategoryStruct.comp φ ψ') : ψ = ψ'

Given a diagram

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

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

@[simp]

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

@[simp]

theorem CategoryTheory.Functor.IsStronglyCocartesian.map_comp_map {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : 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' = CategoryStruct.comp f g) (H' : f'' = CategoryStruct.comp f' g') (φ' : a ⟶ b') (φ'' : a ⟶ b'') [p.IsStronglyCocartesian f' φ'] [p.IsHomLift f'' φ''] : CategoryStruct.comp (map p f φ H φ') (map p f' φ' H' φ'') = 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 co-Cartesian 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₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : 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' = CategoryStruct.comp f g) (H' : f'' = CategoryStruct.comp f' g') (φ' : a ⟶ b') (φ'' : a ⟶ b'') [p.IsStronglyCocartesian f' φ'] [p.IsHomLift f'' φ''] {Z : 𝒳} (h : b'' ⟶ Z) : CategoryStruct.comp (map p f φ H φ') (CategoryStruct.comp (map p f' φ' H' φ'') h) = CategoryStruct.comp (map p f φ ⋯ φ'') h

instance CategoryTheory.Functor.IsStronglyCocartesian.comp {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : 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 (CategoryStruct.comp f g) (CategoryStruct.comp φ ψ)

Given two strongly co-Cartesian morphisms φ, ψ as follows

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

Then the composite φ ≫ ψ is also strongly co-Cartesian.

theorem CategoryTheory.Functor.IsStronglyCocartesian.of_comp {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c} [p.IsStronglyCocartesian f φ] [p.IsStronglyCocartesian (CategoryStruct.comp f g) (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 co-Cartesian, then so is ψ.

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

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

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

A strongly co-Cartesian arrow lying over an isomorphism is an isomorphism.

noncomputable def CategoryTheory.Functor.IsStronglyCocartesian.codomainIsoOfBaseIso {𝒮 : Type u₁} {𝒳 : Type u₂} [Category.{v₁, u₁} 𝒮] [Category.{v₂, u₂} 𝒳] (p : Functor 𝒳 𝒮) {R S S' : 𝒮} {a b b' : 𝒳} {f : R ⟶ S} {f' : R ⟶ S'} {g : S ≅ S'} (h : f' = 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 co-Cartesian arrows lying over isomorphic objects.

Equations

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