Cartesian lifts

We introduce the structures Display.Cartesian and Display.CoCartesian carrying data witnessing that a given lift is cartesian and cocartesian, respectively.

Specialized to the display category structure of a functor P : E ⥤ C, we obtain the class CartMor of cartesian morphisms in E. The type CartMor P is defined in terms of the predicate isCartesianMorphism.

Given a displayed category structure on a type family F : C → Type, and an object I : C, we shall refer to the type F I as the "fiber" of F at I. For a morphism f : I ⟶ J in C, and objects X : F I and Y : F J, we shall refer to a hom-over g : X ⟶[f] Y as a "lift" of f to X and Y.

We prove the following closure properties of the class CartMor of cartesian morphisms:

• cart_id proves that the identity morphism is cartesian.
• cart_comp proves that the composition of cartesian morphisms is cartesian.
• cart_iso_closed proves that the class of cartesian morphisms is closed under isomorphisms.
• cart_pullback proves that, if P preserves pullbacks, then the pullback of a cartesian morphism is cartesian.

instCatCart provides a category instance for the class of cartesian morphisms, and Cart.forget provides the forgetful functor from the category of cartesian morphisms to the domain category E.

Main declarations

• CartLift f Y is the type of cartesian lifts of a morphism f with fixed target Y.
• CoCartLift f X is the type of cocartesian lifts of a morphism f with fixed source X.

Given g : CartLift f Y, we have

• g.1 is the lift of f to Y.
• g.homOver : CartLift.toLift.src ⟶[f] Y is a morphism over f.
• g.homOver.hom is the underlying morphism of g.homOver.
• g.is_cart is the proof that g.homOver is cartesian.

Similarly, given g : CoCartLift f X, we have

• g.1 is the lift of f from X.
• g.homOver : X ⟶[f] CoCartLift.toCoLift.tgt is a morphism over f.
• g.homOver.hom is the underlying morphism of g.homOver.
• g.is_cocart is the proof that g.homOver is cocartesian.

class CategoryTheory.Display.Cartesian {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : Type (max (max (max u_1 u_3) u_4) u_5)

A lift g : X ⟶[f] Y is cartesian if for every morphism u : K ⟶ I in the base and every hom-over g' : Z ⟶[u ≫ f] Y over the composite u ≫ f, there is a unique morphism k : Z ⟶[u] X over u such that k ≫ g = g'.

       _ _ _ _ _ _ _ _ _ _ _
      /           g'        \
     |                      v
     Z - - - - > X --------> Y
     _   ∃!k     _   g       _
     |           |           |
     |           |           |
     v           v           v
     K --------> I --------> J
          u            f

• uniq_lift : ⦃K : C⦄ → ⦃Z : F K⦄ → (u : K ⟶ I) → (g' : Z ⟶[CategoryTheory.CategoryStruct.comp u f] Y) → Unique { k : Z ⟶[u] X // CategoryTheory.DisplayStruct.comp_over k g = g' }

class CategoryTheory.Display.Cartesian' {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_5, u_2} E] {P : CategoryTheory.Functor E C} {X : E} {Y : E} (g : X ⟶ Y) : Type (max (max u_2 u_4) u_5)

• uniq_lift : ⦃Z : E⦄ → (u : P.obj Z ⟶ P.obj X) → (g' : Z ⟶ Y) → Unique { k : Z ⟶ X // CategoryTheory.CategoryStruct.comp k g = g' ∧ P.map k = u }

class CategoryTheory.Display.CoCartesian {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) : Type (max (max (max u_1 u_3) u_4) u_5)

A lift g : X ⟶[f] Y is cocartesian if for all morphisms u in the base and g' : X ⟶[f ≫ u] Z, there is a unique morphism k : Y ⟶[u] Z over u such that g ≫ k = g'.

       _ _ _ _ _ _ _ _ _ _ _
      /          g'         \
     |                      v
     X ------- > Y - - - - > Z
     _    g      _    ∃!k    _
     |           |           |
     |           |           |
     v           v           v
     I --------> J --------> K
          f            u

• uniq_lift : ⦃K : C⦄ → ⦃Z : F K⦄ → (u : J ⟶ K) → (g' : X ⟶[CategoryTheory.CategoryStruct.comp f u] Z) → Unique { k : Y ⟶[u] Z // CategoryTheory.DisplayStruct.comp_over g k = g' }

def CategoryTheory.Display.Cartesian.gap {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) [CategoryTheory.Display.Cartesian g] {K : C} {Z : F K} {u : K ⟶ I} (g' : Z ⟶[CategoryTheory.CategoryStruct.comp u f] Y) : Z ⟶[u] X

gap g u g' is the canonical map from a lift g' : Z ⟶[u ≫ f] X to a cartesian lift g of f.

Equations

• CategoryTheory.Display.Cartesian.gap g g' = ↑default

def CategoryTheory.Display.Cartesian.gapCast {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) [CategoryTheory.Display.Cartesian g] {K : C} {Z : F K} (u : K ⟶ I) {f' : K ⟶ J} (g' : Z ⟶[f'] Y) (w : f' = CategoryTheory.CategoryStruct.comp u f) : Z ⟶[u] X

A variant of gaplift for g' : Z ⟶[f'] Y with casting along f' = u ≫ f baked into the definition.

Equations

• CategoryTheory.Display.Cartesian.gapCast g u g' w = ↑default

@[simp]

theorem CategoryTheory.Display.Cartesian.gap_cast {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) [CategoryTheory.Display.Cartesian g] {K : C} {Z : F K} (u : K ⟶ I) {f' : K ⟶ J} (g' : Z ⟶[f'] Y) (w : f' = CategoryTheory.CategoryStruct.comp u f) : CategoryTheory.Display.Cartesian.gapCast g u g' w = CategoryTheory.Display.Cartesian.gap g (w ▸ g')

@[simp]

theorem CategoryTheory.Display.Cartesian.gap_prop {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) [CategoryTheory.Display.Cartesian g] {K : C} {Z : F K} (u : K ⟶ I) (g' : Z ⟶[CategoryTheory.CategoryStruct.comp u f] Y) : CategoryTheory.DisplayStruct.comp_over (CategoryTheory.Display.Cartesian.gap g g') g = g'

The composition of the gap lift and the cartesian hom-over is the given hom-over.

@[simp]

theorem CategoryTheory.Display.Cartesian.gaplift_uniq {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {f : I ⟶ J} {X : F I} {Y : F J} (g : X ⟶[f] Y) [CategoryTheory.Display.Cartesian g] {K : C} {Z : F K} {u : K ⟶ I} (g' : Z ⟶[CategoryTheory.CategoryStruct.comp u f] Y) (v : Z ⟶[u] X) (hv : CategoryTheory.DisplayStruct.comp_over v g = g') : v = CategoryTheory.Display.Cartesian.gap g g'

The uniqueness part of the universal property of the gap lift.

instance CategoryTheory.Display.Cartesian.instId {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {X : F I} : CategoryTheory.Display.Cartesian (𝟙ₒ X)

The identity hom-over is cartesian.

Equations

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

instance CategoryTheory.Display.Cartesian.instComp {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} {K : C} {X : F I} {Y : F J} {Z : F K} {f₁ : I ⟶ J} {f₂ : J ⟶ K} (g₁ : X ⟶[f₁] Y) [CategoryTheory.Display.Cartesian g₁] (g₂ : Y ⟶[f₂] Z) [CategoryTheory.Display.Cartesian g₂] : CategoryTheory.Display.Cartesian (CategoryTheory.DisplayStruct.comp_over g₁ g₂)

Cartesian based-lifts are closed under composition.

Equations

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

class CategoryTheory.Display.CartLift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} (f : I ⟶ J) (tgt : F J) extends CategoryTheory.Display.Lift : Type (max (max (max u_1 u_3) u_4) u_5)

The type of cartesian lifts of a morphism f with fixed target.

• src : F I
• homOver : CategoryTheory.Display.CartLift.toLift.src ⟶[f] tgt
• is_cart : CategoryTheory.Display.Cartesian CategoryTheory.Display.CartLift.toLift.homOver

def CategoryTheory.Display.HasCartLift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} (f : I ⟶ J) (tgt : F J) : Prop

Mere existence of a cartesian lift with fixed target.

Equations

• CategoryTheory.Display.HasCartLift f tgt = Nonempty (CategoryTheory.Display.CartLift f tgt)

class CategoryTheory.Display.CoCartLift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} (f : I ⟶ J) (src : F I) extends CategoryTheory.Display.CoLift : Type (max (max (max u_1 u_3) u_4) u_5)

The type of cocartesian lifts of a morphism f with fixed source.

• tgt : F J
• homOver : src ⟶[f] CategoryTheory.Display.CoCartLift.toCoLift.tgt
• is_cocart : CategoryTheory.Display.CoCartesian CategoryTheory.Display.CoCartLift.toCoLift.homOver

def CategoryTheory.Display.HasCoCartLift {C : Type u_1} [CategoryTheory.Category.{u_4, u_1} C] {F : C → Type u_3} [CategoryTheory.Display F] {I : C} {J : C} (f : I ⟶ J) (src : F I) : Prop

Equations

• CategoryTheory.Display.HasCoCartLift f src = Nonempty (CategoryTheory.Display.CoCartLift f src)