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ā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) extends p.IsHomLift f φ :

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

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

    Stacks Tag 02XK

    Instances
      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 φ'] :

      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ā‚‚} [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 φ'] :
        @[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) :
        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 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ā‚‚} [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 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ā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCocartesian f φ] :
        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 φ'] :

        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ā‚‚} [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] :

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

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

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

          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 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ā‚‚} [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' φ'] :

          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ā‚‚} [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 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ā‚‚} [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 cocartesian, 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 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ā‚‚} [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 ψ] :

            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.

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

            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ā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ≅ b) [p.IsHomLift 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 φ] :
            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 cocartesian 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' φ'] :

            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