Documentation

Mathlib.CategoryTheory.FiberedCategory.Cocartesian

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 :

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 Ļ†' = Ļ† ā‰« Ļ‡.

Instances
    theorem CategoryTheory.Functor.IsCocartesian.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.IsCocartesian f Ļ†] {b' : š’³} (Ļ†' : a āŸ¶ b') [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 :

    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.

    Instances
      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} [self : p.IsStronglyCocartesian f Ļ†] {b' : š’³} (g : S āŸ¶ p.obj b') (Ļ†' : a āŸ¶ b') [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
      Instances For
        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 Ļ†'] :
        Equations
        • ā‹Æ = ā‹Æ
        @[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) :
        @[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 Ļ†'] :
        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 Ļ† Ļˆ = Ļ†') :

        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 Ļ†] :
        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.
        Instances For
          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
          Instances For
            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_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) :
            @[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' Ļ†'] :
            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 Ļ† Ļˆ = Ļ†') :

            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 Ļ†] :
            @[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) :
            @[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'' Ļ†''] :

            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''.

            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 Ļˆ] :

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

            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.
            Instances For