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 #

class CategoryTheory.Functor.IsCartesian {š’® : 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 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
    class CategoryTheory.Functor.IsStronglyCartesian {š’® : 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 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 φ' = χ ≫ φ.

    Stacks Tag 02XK

    Instances
      noncomputable def CategoryTheory.Functor.IsCartesian.map {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :

      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
        instance CategoryTheory.Functor.IsCartesian.map_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :
        @[simp]
        theorem CategoryTheory.Functor.IsCartesian.fac {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsHomLift f φ'] :
        CategoryStruct.comp (IsCartesian.map p f φ φ') φ = φ'
        @[simp]
        theorem CategoryTheory.Functor.IsCartesian.fac_assoc {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsHomLift f φ'] {Z : š’³} (h : b ⟶ Z) :
        theorem CategoryTheory.Functor.IsCartesian.map_uniq {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsHomLift f φ'] (ψ : a' ⟶ a) [p.IsHomLift (CategoryStruct.id R) ψ] (hψ : CategoryStruct.comp ψ φ = φ') :
        ψ = 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 φ.

        theorem CategoryTheory.Functor.IsCartesian.ext {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (ψ ψ' : a' ⟶ a) [p.IsHomLift (CategoryStruct.id R) ψ] [p.IsHomLift (CategoryStruct.id R) ψ'] (h : CategoryStruct.comp ψ φ = 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 ψ = ψ'.

        @[simp]
        theorem CategoryTheory.Functor.IsCartesian.map_self {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] :
        noncomputable def CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :

        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
          @[simp]
          theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :
          (domainUniqueUpToIso p f φ φ').hom = IsCartesian.map p f φ φ'
          @[simp]
          theorem CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :
          (domainUniqueUpToIso p f φ φ').inv = IsCartesian.map p f φ' φ
          instance CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_inv_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :
          instance CategoryTheory.Functor.IsCartesian.domainUniqueUpToIso_hom_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsCartesian f φ] {a' : š’³} (φ' : a' ⟶ b) [p.IsCartesian f φ'] :
          instance CategoryTheory.Functor.IsCartesian.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.IsCartesian f φ] {a' : š’³} (φ' : a' ≅ a) [p.IsHomLift (CategoryStruct.id R) φ'.hom] :

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

          instance CategoryTheory.Functor.IsCartesian.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.IsCartesian f φ] {b' : š’³} (φ' : b ≅ b') [p.IsHomLift (CategoryStruct.id S) φ'.hom] :

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

          theorem CategoryTheory.Functor.IsStronglyCartesian.universal_property {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} (g : R' ⟶ R) (f' : R' ⟶ S) (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

          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.

          instance CategoryTheory.Functor.IsStronglyCartesian.isCartesian_of_isStronglyCartesian {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] :
          p.IsCartesian f φ
          noncomputable def CategoryTheory.Functor.IsStronglyCartesian.map {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :

          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
            instance CategoryTheory.Functor.IsStronglyCartesian.map_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :
            p.IsHomLift g (map p f φ hf' φ')
            @[simp]
            theorem CategoryTheory.Functor.IsStronglyCartesian.fac {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] :
            CategoryStruct.comp (map p f φ hf' φ') φ = φ'
            @[simp]
            theorem CategoryTheory.Functor.IsStronglyCartesian.fac_assoc {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] {Z : š’³} (h : b ⟶ Z) :
            CategoryStruct.comp (map p f φ hf' φ') (CategoryStruct.comp φ h) = CategoryStruct.comp φ' h
            theorem CategoryTheory.Functor.IsStronglyCartesian.map_uniq {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] {R' : š’®} {a' : š’³} {g : R' ⟶ R} {f' : R' ⟶ S} (hf' : f' = CategoryStruct.comp g f) (φ' : a' ⟶ b) [p.IsHomLift f' φ'] (ψ : a' ⟶ a) [p.IsHomLift g ψ] (hψ : CategoryStruct.comp ψ φ = φ') :
            ψ = 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.

            theorem CategoryTheory.Functor.IsStronglyCartesian.ext {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : 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 : CategoryStruct.comp ψ φ = 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 ψ = ψ'.

            @[simp]
            theorem CategoryTheory.Functor.IsStronglyCartesian.map_self {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R S : š’®} {a b : š’³} (f : R ⟶ S) (φ : a ⟶ b) [p.IsStronglyCartesian f φ] :
            map p f φ ⋯ φ = CategoryStruct.id a
            @[simp]
            theorem CategoryTheory.Functor.IsStronglyCartesian.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.IsStronglyCartesian f φ] {R' R'' : š’®} {a' a'' : š’³} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'} (H : f' = CategoryStruct.comp g f) (H' : f'' = CategoryStruct.comp g' f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b) [p.IsStronglyCartesian 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 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.

            @[simp]
            theorem CategoryTheory.Functor.IsStronglyCartesian.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.IsStronglyCartesian f φ] {R' R'' : š’®} {a' a'' : š’³} {f' : R' ⟶ S} {f'' : R'' ⟶ S} {g : R' ⟶ R} {g' : R'' ⟶ R'} (H : f' = CategoryStruct.comp g f) (H' : f'' = CategoryStruct.comp g' f') (φ' : a' ⟶ b) (φ'' : a'' ⟶ b) [p.IsStronglyCartesian f' φ'] [p.IsHomLift f'' φ''] {Z : š’³} (h : a ⟶ Z) :
            CategoryStruct.comp (map p f' φ' H' φ'') (CategoryStruct.comp (map p f φ H φ') h) = CategoryStruct.comp (map p f φ ⋯ φ'') h
            instance CategoryTheory.Functor.IsStronglyCartesian.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.IsStronglyCartesian f φ] [p.IsStronglyCartesian g ψ] :

            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.

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

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

            A strongly cartesian morphism lying over an isomorphism is an isomorphism.

            noncomputable def CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R R' S : š’®} {a a' b : š’³} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :

            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
              @[simp]
              theorem CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_hom {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R R' S : š’®} {a a' b : š’³} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :
              (domainIsoOfBaseIso p h φ φ').hom = map p f φ h φ'
              @[simp]
              theorem CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso_inv {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R R' S : š’®} {a a' b : š’³} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :
              (domainIsoOfBaseIso p h φ φ').inv = map p f' φ' ⋯ φ
              instance CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_inv_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R R' S : š’®} {a a' b : š’³} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :
              p.IsHomLift g.hom (domainIsoOfBaseIso p h φ φ').hom
              instance CategoryTheory.Functor.IsStronglyCartesian.domainUniqueUpToIso_hom_isHomLift {š’® : Type u₁} {š’³ : Type uā‚‚} [Category.{v₁, u₁} š’®] [Category.{vā‚‚, uā‚‚} š’³] (p : Functor š’³ š’®) {R R' S : š’®} {a a' b : š’³} {f : R ⟶ S} {f' : R' ⟶ S} {g : R' ≅ R} (h : f' = CategoryStruct.comp g.hom f) (φ : a ⟶ b) (φ' : a' ⟶ b) [p.IsStronglyCartesian f φ] [p.IsStronglyCartesian f' φ'] :
              p.IsHomLift g.inv (domainIsoOfBaseIso p h φ φ').inv