Documentation

Mathlib.CategoryTheory.FiberedCategory.Cartesian

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 #

source
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 p.IsHomLift f Ļ† :
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.

Instances
    source
    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 p.IsHomLift f Ļ† :
    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.

    Instances
      source
      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
      Instances For
        source
        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 Ļ† Ļ†')
        source
        @[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 Ļ† Ļ†') Ļ† = Ļ†'
        source
        @[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
        source
        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 Ļ†.

        source
        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) [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 Ļˆ = Ļˆ'.

        source
        @[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
        source
        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.
        Instances For
          source
          @[simp]
          theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom {š’® : 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 Ļ†'] :
          (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f Ļ† Ļ†').hom = CategoryTheory.Functor.IsCartesian.map p f Ļ† Ļ†'
          source
          @[simp]
          theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv {š’® : 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 Ļ†'] :
          (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f Ļ† Ļ†').inv = CategoryTheory.Functor.IsCartesian.map p f Ļ†' Ļ†
          source
          instance CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv_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.IsCartesian f Ļ†'] :
          p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f Ļ† Ļ†').hom
          source
          instance CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom_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.IsCartesian f Ļ†'] :
          p.IsHomLift (CategoryTheory.CategoryStruct.id R) (CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso p f Ļ† Ļ†').inv
          source
          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.

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

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

          source
          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 Ļ†
          source
          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
          Instances For
            source
            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' Ļ†')
            source
            @[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' Ļ†') Ļ† = Ļ†'
            source
            @[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
            source
            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.

            source
            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} [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 Ļˆ = Ļˆ'.

            source
            @[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
            source
            @[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.

            source
            @[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
            source
            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.

            source
            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 Ļ†.

            source
            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
            source
            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 Ļ†
            source
            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.

            source
            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.
            Instances For
              source
              @[simp]
              theorem CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_inv {š’® : 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' Ļ†'] :
              (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h Ļ† Ļ†').inv = CategoryTheory.Functor.IsStronglyCartesian.map p f' Ļ†' ā‹Æ Ļ†
              source
              @[simp]
              theorem CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_hom {š’® : 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' Ļ†'] :
              (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h Ļ† Ļ†').hom = CategoryTheory.Functor.IsStronglyCartesian.map p f Ļ† h Ļ†'
              source
              instance CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_inv_isHomLift {š’® : 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' Ļ†'] :
              p.IsHomLift g.hom (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h Ļ† Ļ†').hom
              source
              instance CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_hom_isHomLift {š’® : 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' Ļ†'] :
              p.IsHomLift g.inv (CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso p h Ļ† Ļ†').inv