Cartesian Lifts

For a functor P : E ⥤ C, the structure BasedLift provides the type of lifts of a given morphism in the base with fixed source and target in the fibers of P: More precisely, BasedLift P f is the type of morphisms in the domain category E which are lifts of f.

We provide various useful constructors:

• BasedLift.tauto regards a morphism g of the domain category E as a based-lift of its image P g under functor P.
• BasedLift.id and BasedLift.comp provide the identity and composition of based-lifts, respectively.
• We can cast a based-lift along an equality of the base morphisms using the equivalence BasedLift.cast.

There are also typeclasses CartesianBasedLift and CoCartesianBasedLift carrying data witnessing that a given based-lift is cartesian and cocartesian, respectively.

For a functor P : E ⥤ C, we provide the class CartMor of cartesian morphisms in E. The type CartMor Pis defined in terms of the predicate isCartesianMorphism.

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.

Finally, We provide the following notations:

• x ⟶[f] y for BasedLift P f x y
• f ≫[l] g for the composition of based-lifts given by BasedLift.comp f g

theorem CategoryTheory.BasedLift.ext_iff {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {src : P ⁻¹ c} {tgt : P ⁻¹ d} (x y : CategoryTheory.BasedLift P f src tgt), x = y ↔ x.hom = y.hom

theorem CategoryTheory.BasedLift.ext {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {src : P ⁻¹ c} {tgt : P ⁻¹ d} (x y : CategoryTheory.BasedLift P f src tgt), x.hom = y.hom → x = y

structure CategoryTheory.BasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (src : P ⁻¹ c) (tgt : P ⁻¹ d) : Type u_4

The type of lifts of a given morphism in the base with fixed source and target in the fibers of the domain and codomain respectively.

• hom : ↑src ⟶ ↑tgt
• over : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f

theorem CategoryTheory.BasedLift.over {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {src : P ⁻¹ c} {tgt : P ⁻¹ d} (self : CategoryTheory.BasedLift P f src tgt) : CategoryTheory.CategoryStruct.comp (P.map self.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f

def CategoryTheory.«term_⟶[_]_» : Lean.TrailingParserDescr

Equations

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

theorem CategoryTheory.Lift.ext {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {tgt : P ⁻¹ d} (x y : CategoryTheory.Lift P f tgt), x.src = y.src → HEq x.based_lift y.based_lift → x = y

theorem CategoryTheory.Lift.ext_iff {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {tgt : P ⁻¹ d} (x y : CategoryTheory.Lift P f tgt), x = y ↔ x.src = y.src ∧ HEq x.based_lift y.based_lift

structure CategoryTheory.Lift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (tgt : P ⁻¹ d) : Type (max u_2 u_4)

A lift of a morphism in the base with a fixed target in the fiber of the codomain

• src : P ⁻¹ c
• based_lift : CategoryTheory.BasedLift P f self.src tgt

theorem CategoryTheory.CoLift.ext {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {src : P ⁻¹ c} (x y : CategoryTheory.CoLift P f src), x.tgt = y.tgt → HEq x.based_colift y.based_colift → x = y

theorem CategoryTheory.CoLift.ext_iff {C : Type u_1} {E : Type u_2} : ∀ {inst : CategoryTheory.Category.{u_3, u_1} C} {inst_1 : CategoryTheory.Category.{u_4, u_2} E} {P : CategoryTheory.Functor E C} {c d : C} {f : c ⟶ d} {src : P ⁻¹ c} (x y : CategoryTheory.CoLift P f src), x = y ↔ x.tgt = y.tgt ∧ HEq x.based_colift y.based_colift

structure CategoryTheory.CoLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (src : P ⁻¹ c) : Type (max u_2 u_4)

A lift of a morphism in the base with a fixed source in the fiber of the domain

• tgt : P ⁻¹ d
• based_colift : CategoryTheory.BasedLift P f src self.tgt

def CategoryTheory.HasLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (y : P ⁻¹ d) : Prop

HasLift P f y represents the mere existence of a lift of the morphism f with target y.

Equations

• CategoryTheory.HasLift P f y = Nonempty (CategoryTheory.Lift P f y)

def CategoryTheory.HasCoLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (x : P ⁻¹ c) : Prop

HasColift P f x represents the mere existence of a lift of the morphism f with source x.

Equations

• CategoryTheory.HasCoLift P f x = Nonempty (CategoryTheory.CoLift P f x)

theorem CategoryTheory.BasedLift.hom_ext {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {g₁ : CategoryTheory.BasedLift P f x y} {g₂ : CategoryTheory.BasedLift P f x y} (h : g₁.hom = g₂.hom) : g₁ = g₂

Two based-lifts of the same base morphism are equal if their underlying morphisms are equal in the domain category.

@[simp]

theorem CategoryTheory.BasedLift.over_base {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P f x y) : P.map g.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

instance CategoryTheory.BasedLift.instCoeOutHomValEqObj {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (x : P ⁻¹ c) (y : P ⁻¹ d) : CoeOut (CategoryTheory.BasedLift P f x y) (↑x ⟶ ↑y)

Coercion from BasedLift to the domain category.

Equations

• CategoryTheory.BasedLift.instCoeOutHomValEqObj P f x y = { coe := fun (l : CategoryTheory.BasedLift P f x y) => l.hom }

@[simp]

theorem CategoryTheory.BasedLift.tauto_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} (g : e ⟶ e') : (CategoryTheory.BasedLift.tauto g).hom = g

def CategoryTheory.BasedLift.tauto {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} (g : e ⟶ e') : CategoryTheory.BasedLift P (P.map g) (Fiber.tauto e) (Fiber.tauto e')

BasedLift.tauto regards a morphism g of the domain category E as a based-lift of its image P g under functor P.

Equations

• CategoryTheory.BasedLift.tauto g = { hom := g, over := ⋯ }

theorem CategoryTheory.BasedLift.tauto_over_base {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} (f : P.obj x ⟶ P.obj y) (e : CategoryTheory.BasedLift P f (Fiber.tauto x) (Fiber.tauto y)) : P.map e.hom = f

@[simp]

theorem CategoryTheory.BasedLift.instCoeTautoBasedLift_coe {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} {g : e ⟶ e'} : CoeDep.coe g = CategoryTheory.BasedLift.tauto g

instance CategoryTheory.BasedLift.instCoeTautoBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} {g : e ⟶ e'} : CoeDep (e ⟶ e') g (CategoryTheory.BasedLift P (P.map g) (Fiber.tauto e) (Fiber.tauto e'))

A tautological based-lift associated to a given morphism in the domain E.

Equations

• CategoryTheory.BasedLift.instCoeTautoBasedLift = { coe := CategoryTheory.BasedLift.tauto g }

instance CategoryTheory.BasedLift.instCoeFiberHom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {y : P ⁻¹ c} : Coe (CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y) (x ⟶ y)

Regarding a based-lift x ⟶[𝟙 c] y of the identity morphism 𝟙 c as a morphism in the fiber P⁻¹ c .

Equations

• CategoryTheory.BasedLift.instCoeFiberHom = { coe := fun (f : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y) => ⟨f.hom, ⋯⟩ }

@[simp]

theorem CategoryTheory.BasedLift.ofFiberHom_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {y : P ⁻¹ c} (f : x ⟶ y) : (CategoryTheory.BasedLift.ofFiberHom f).hom = ↑f

def CategoryTheory.BasedLift.ofFiberHom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {y : P ⁻¹ c} (f : x ⟶ y) : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x y

BasedLift.ofFiberHom regards a morphism in the fiber category P⁻¹ c as a based-lift of the identity morphism of c.

Equations

• CategoryTheory.BasedLift.ofFiberHom f = { hom := ↑f, over := ⋯ }

def CategoryTheory.BasedLift.id {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} (x : P ⁻¹ c) : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x x

The identity based-lift.

Equations

• CategoryTheory.BasedLift.id x = { hom := CategoryTheory.CategoryStruct.id ↑x, over := ⋯ }

theorem CategoryTheory.BasedLift.id_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} : (CategoryTheory.BasedLift.id x).hom = CategoryTheory.CategoryStruct.id ↑x

def CategoryTheory.BasedLift.comp {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {I : C} {J : C} {K : C} {f : I ⟶ J} {f' : J ⟶ K} {X : P ⁻¹ I} {Y : P ⁻¹ J} {Z : P ⁻¹ K} (g : CategoryTheory.BasedLift P f X Y) (g' : CategoryTheory.BasedLift P f' Y Z) : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp f f') X Z

The composition of based-lifts

Equations

• (g ≫[l] g') = { hom := CategoryTheory.CategoryStruct.comp g.hom g'.hom, over := ⋯ }

def CategoryTheory.BasedLift.«term_≫ₗ_» : Lean.TrailingParserDescr

Equations

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

def CategoryTheory.BasedLift.«term_≫[l]_» : Lean.TrailingParserDescr

Equations

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

theorem CategoryTheory.BasedLift.comp_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {d' : C} {f₁ : c ⟶ d} {f₂ : d ⟶ d'} {x : P ⁻¹ c} {y : P ⁻¹ d} {z : P ⁻¹ d'} (g₁ : CategoryTheory.BasedLift P f₁ x y) (g₂ : CategoryTheory.BasedLift P f₂ y z) : (g₁ ≫[l] g₂).hom = CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom

The underlying morphism of a composition of based-lifts is the composition of the underlying morphisms.

@[simp]

theorem CategoryTheory.BasedLift.comp_hom' {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {d' : C} {f₁ : c ⟶ d} {f₂ : d ⟶ d'} {x : P ⁻¹ c} {y : P ⁻¹ d} {z : P ⁻¹ d'} {g₁ : CategoryTheory.BasedLift P f₁ x y} {g₂ : CategoryTheory.BasedLift P f₂ y z} {h : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp f₁ f₂) x z} : (g₁ ≫[l] g₂) = h ↔ CategoryTheory.CategoryStruct.comp g₁.hom g₂.hom = h.hom

theorem CategoryTheory.BasedLift.tauto_comp_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} {e'' : E} {g : e ⟶ e'} {g' : e' ⟶ e''} : (CategoryTheory.BasedLift.tauto g ≫[l] CategoryTheory.BasedLift.tauto g').hom = CategoryTheory.CategoryStruct.comp g g'

theorem CategoryTheory.BasedLift.comp_tauto_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} {z : E} {f : P.obj x ⟶ P.obj y} {l : CategoryTheory.BasedLift P f (Fiber.tauto x) (Fiber.tauto y)} {g : y ⟶ z} : (l ≫[l] CategoryTheory.BasedLift.tauto g).hom = CategoryTheory.CategoryStruct.comp l.hom g

@[simp]

theorem CategoryTheory.BasedLift.cast_apply_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {f' : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (h : f = f') (g : CategoryTheory.BasedLift P f x y) : ((CategoryTheory.BasedLift.cast h) g).hom = g.hom

@[simp]

theorem CategoryTheory.BasedLift.cast_symm_apply_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {f' : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (h : f = f') (g : CategoryTheory.BasedLift P f' x y) : ((CategoryTheory.BasedLift.cast h).symm g).hom = g.hom

def CategoryTheory.BasedLift.cast {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {f' : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (h : f = f') : CategoryTheory.BasedLift P f x y ≃ CategoryTheory.BasedLift P f' x y

Casting a based-lift along an equality of the base morphisms induces an equivalence of the based-lifts.

Equations

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

theorem CategoryTheory.BasedLift.cast_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {f' : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {g : CategoryTheory.BasedLift P f x y} {h : f = f'} : ((CategoryTheory.BasedLift.cast h) g).hom = g.hom

theorem CategoryTheory.BasedLift.eq_id_of_hom_eq_id {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {x : P ⁻¹ c} {g : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.id c) x x} : g.hom = CategoryTheory.CategoryStruct.id ↑x ↔ g = CategoryTheory.BasedLift.id x

def CategoryTheory.BasedLift.castIdComp {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) f) x y ≃ CategoryTheory.BasedLift P f x y

Casting equivalence along postcomposition with the identity morphism.

Equations

• CategoryTheory.BasedLift.castIdComp = CategoryTheory.BasedLift.cast ⋯

def CategoryTheory.BasedLift.castCompId {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.id d)) x y ≃ CategoryTheory.BasedLift P f x y

Casting equivalence along precomposition with the identity morphism.

Equations

• CategoryTheory.BasedLift.castCompId = CategoryTheory.BasedLift.cast ⋯

def CategoryTheory.BasedLift.castAssoc {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {d' : C} {u' : c' ⟶ c} {f : c ⟶ d} {u : d ⟶ d'} {x : P ⁻¹ c'} {y : P ⁻¹ d'} : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp u' f) u) x y ≃ CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u' (CategoryTheory.CategoryStruct.comp f u)) x y

Equations

• CategoryTheory.BasedLift.castAssoc = CategoryTheory.BasedLift.cast ⋯

@[simp]

theorem CategoryTheory.BasedLift.castOfeqToHom_symm_apply_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f) (Fiber.tauto ↑x) y) : (CategoryTheory.BasedLift.castOfeqToHom.symm g).hom = g.hom

@[simp]

theorem CategoryTheory.BasedLift.castOfeqToHom_apply_hom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P f x y) : (CategoryTheory.BasedLift.castOfeqToHom g).hom = g.hom

def CategoryTheory.BasedLift.castOfeqToHom {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} : CategoryTheory.BasedLift P f x y ≃ CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f) (Fiber.tauto ↑x) y

Equations

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

@[simp]

theorem CategoryTheory.BasedLift.assoc {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {d' : C} {f₁ : c' ⟶ c} {f₂ : c ⟶ d} {f₃ : d ⟶ d'} {w : P ⁻¹ c'} {x : P ⁻¹ c} {y : P ⁻¹ d} {z : P ⁻¹ d'} (g₁ : CategoryTheory.BasedLift P f₁ w x) (g₂ : CategoryTheory.BasedLift P f₂ x y) (g₃ : CategoryTheory.BasedLift P f₃ y z) : ((g₁ ≫[l] g₂) ≫[l] g₃) = CategoryTheory.BasedLift.castAssoc.invFun (g₁ ≫[l] g₂ ≫[l] g₃)

The composition of based-lifts is associative up to casting along equalities of the base morphisms.

@[simp]

theorem CategoryTheory.BasedLift.assoc_inv {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {d' : C} {f₁ : c' ⟶ c} {f₂ : c ⟶ d} {f₃ : d ⟶ d'} {w : P ⁻¹ c'} {x : P ⁻¹ c} {y : P ⁻¹ d} {z : P ⁻¹ d'} (g₁ : CategoryTheory.BasedLift P f₁ w x) (g₂ : CategoryTheory.BasedLift P f₂ x y) (g₃ : CategoryTheory.BasedLift P f₃ y z) : CategoryTheory.BasedLift.castAssoc.toFun ((g₁ ≫[l] g₂) ≫[l] g₃) = g₁ ≫[l] g₂ ≫[l] g₃

theorem CategoryTheory.BasedLift.tauto_comp_cast {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {e : E} {e' : E} {e'' : E} {g : e ⟶ e'} {g' : e' ⟶ e''} : CategoryTheory.BasedLift.tauto (CategoryTheory.CategoryStruct.comp g g') = (CategoryTheory.BasedLift.cast ⋯) (CategoryTheory.BasedLift.tauto g ≫[l] CategoryTheory.BasedLift.tauto g')

instance CategoryTheory.Lift.instCoeOutSigmaHomValEqObj {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} : {a a_1 : C} → {f : a ⟶ a_1} → {y : P ⁻¹ a_1} → CoeOut (CategoryTheory.Lift P f y) ((x : E) × (x ⟶ ↑y))

Equations

• CategoryTheory.Lift.instCoeOutSigmaHomValEqObj = { coe := fun (l : CategoryTheory.Lift P f y) => ⟨↑l.src, l.based_lift.hom⟩ }

@[simp]

theorem CategoryTheory.Lift.over_base {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (y : P ⁻¹ d) (g : CategoryTheory.Lift P f y) : P.map g.based_lift.hom = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))

def CategoryTheory.Lift.homOf {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} : {a a_1 : C} → {f : a ⟶ a_1} → {y : P ⁻¹ a_1} → (g : CategoryTheory.Lift P f y) → ↑g.src ⟶ ↑y

Equations

• g.homOf = g.based_lift.hom

instance CategoryTheory.Lift.instCoeDepHomValEqObjSrc {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} : {a a_1 : C} → {f : a ⟶ a_1} → {y : P ⁻¹ a_1} → {g : CategoryTheory.Lift P f y} → CoeDep (CategoryTheory.Lift P f y) g (↑g.src ⟶ ↑y)

Regarding a morphism in Lift P f as a morphism in the total category E.

Equations

• CategoryTheory.Lift.instCoeDepHomValEqObjSrc = { coe := g.based_lift.hom }

def CategoryTheory.Lift.id {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} (x : P ⁻¹ c) : CategoryTheory.Lift P (CategoryTheory.CategoryStruct.id c) x

The identity lift.

Equations

• CategoryTheory.Lift.id x = { src := x, based_lift := CategoryTheory.BasedLift.id x }

class CategoryTheory.IsoBasedLift {C : Type u_3} {E : Type u_4} [CategoryTheory.Category.{u_5, u_3} C] [CategoryTheory.Category.{u_6, u_4} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) [CategoryTheory.IsIso f] (x : P ⁻¹ c) (y : P ⁻¹ d) extends CategoryTheory.BasedLift : Type u_6

The type of iso-based-lifts of an isomorphism in the base with fixed source and target.

• hom : ↑x ⟶ ↑y
• over : CategoryTheory.CategoryStruct.comp (P.map CategoryTheory.IsoBasedLift.toBasedLift.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
• is_iso_hom : CategoryTheory.IsIso CategoryTheory.IsoBasedLift.toBasedLift.hom

theorem CategoryTheory.IsoBasedLift.is_iso_hom {C : Type u_3} {E : Type u_4} [CategoryTheory.Category.{u_5, u_3} C] [CategoryTheory.Category.{u_6, u_4} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} [CategoryTheory.IsIso f] {x : P ⁻¹ c} {y : P ⁻¹ d} [self : CategoryTheory.IsoBasedLift f x y] : CategoryTheory.IsIso CategoryTheory.IsoBasedLift.toBasedLift.hom

def CategoryTheory.IsoBasedLift.«term_⟶[≅_]_» : Lean.TrailingParserDescr

Equations

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

instance CategoryTheory.IsoBasedLift.instIsoOfIsoBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} [CategoryTheory.IsIso f] {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.IsoBasedLift f x y) : CategoryTheory.IsIso CategoryTheory.IsoBasedLift.toBasedLift.hom

Any iso-based-lift is in particular an isomorphism.

Equations

• ⋯ = ⋯

instance CategoryTheory.IsoBasedLift.instCoeBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} [CategoryTheory.IsIso f] {x : P ⁻¹ c} {y : P ⁻¹ d} : Coe (CategoryTheory.IsoBasedLift f x y) (CategoryTheory.BasedLift P f x y)

Coercion from IsoBasedLift to BasedLift

Equations

• CategoryTheory.IsoBasedLift.instCoeBasedLift = { coe := fun (l : CategoryTheory.IsoBasedLift f x y) => { hom := CategoryTheory.IsoBasedLift.toBasedLift.hom, over := ⋯ } }

noncomputable def CategoryTheory.IsoBasedLift.Inv {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} [CategoryTheory.IsIso f] {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.IsoBasedLift f x y) : CategoryTheory.IsoBasedLift (CategoryTheory.inv f) y x

Equations

• g.Inv = { hom := CategoryTheory.inv CategoryTheory.IsoBasedLift.toBasedLift.hom, over := ⋯, is_iso_hom := ⋯ }

class CategoryTheory.CartesianBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P f x y) : Type (max (max (max u_1 u_2) u_3) u_4)

A lift g : x ⟶[f] y over a base morphism f is cartesian if for every morphism u in the base and every lift g' : x ⟶[u ≫ f] z over the composite u ≫ f, there is a unique morphism l : y ⟶[u] z over u such that l ≫ g = g'.

• uniq_lift : ⦃c' : C⦄ → ⦃z : P ⁻¹ c'⦄ → (u : c' ⟶ c) → (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u f) z y) → Unique { l : CategoryTheory.BasedLift P u z x // (l ≫[l] g) = g' }

class CategoryTheory.CoCartesianBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P f x y) : Type (max (max (max u_1 u_2) u_3) u_4)

A morphism g : x ⟶[f] y over f is cocartesian if for all morphisms u in the base and g' : x ⟶[f ≫ u] z over the composite f ≫ u, there is a unique morphism l : y ⟶[u] z over u such that g ≫ l = g'.

• uniq_colift : ⦃d' : C⦄ → ⦃z : P ⁻¹ d'⦄ → (u : d ⟶ d') → (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp f u) x z) → Unique { l : CategoryTheory.BasedLift P u y z // (g ≫[l] l) = g' }

def CategoryTheory.CartesianBasedLift.gaplift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] (u : c' ⟶ c) (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u f) x' y) : CategoryTheory.BasedLift P u x' x

gaplift g u g' is the canonical map from a lift g' : x' ⟶[u ≫ f] y to a cartesian lift g of f.

Equations

• CategoryTheory.CartesianBasedLift.gaplift g u g' = ↑default

def CategoryTheory.CartesianBasedLift.gaplift' {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] (u : c' ⟶ c) {f' : c' ⟶ d} (g' : CategoryTheory.BasedLift P f' x' y) (h : f' = CategoryTheory.CategoryStruct.comp u f) : CategoryTheory.BasedLift P u x' x

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

Equations

• CategoryTheory.CartesianBasedLift.gaplift' g u g' h = ↑default

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift_cast {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] (u : c' ⟶ c) {f' : c' ⟶ d} (g' : CategoryTheory.BasedLift P f' x' y) (h : f' = CategoryTheory.CategoryStruct.comp u f) : CategoryTheory.CartesianBasedLift.gaplift' g u g' h = CategoryTheory.CartesianBasedLift.gaplift g u ((CategoryTheory.BasedLift.cast h) g')

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift_property {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] (u : c' ⟶ c) (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u f) x' y) : (CategoryTheory.CartesianBasedLift.gaplift g u g' ≫[l] g) = g'

The composition of the gap lift and the cartesian lift is the given lift

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift_hom_property {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] (u : c' ⟶ c) (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u f) x' y) : CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianBasedLift.gaplift g u g').hom g.hom = g'.hom

A variant of the gaplift property for equality of the underlying morphisms.

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift_uniq {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] {u : c' ⟶ c} (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u f) x' y) (v : CategoryTheory.BasedLift P u x' x) (hv : (v ≫[l] g) = g') : v = CategoryTheory.CartesianBasedLift.gaplift g u g'

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

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift_uniq' {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c' : C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} {x' : P ⁻¹ c'} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] {u : c' ⟶ c} (v : CategoryTheory.BasedLift P u x' x) (v' : CategoryTheory.BasedLift P u x' x) (hv : (v ≫[l] g) = v' ≫[l] g) : v = v'

A variant of the uniqueness lemma.

@[simp]

theorem CategoryTheory.CartesianBasedLift.gaplift'_self {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {x : P ⁻¹ c} {y : P ⁻¹ d} (g : CategoryTheory.BasedLift P f x y) [CategoryTheory.CartesianBasedLift g] : CategoryTheory.CartesianBasedLift.gaplift' g (CategoryTheory.CategoryStruct.id c) g ⋯ = CategoryTheory.BasedLift.id x

The gaplift of any cartesian based-lift with respect to itself is the identity.

def CategoryTheory.isCartesianMorphism {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} (g : x ⟶ y) : Prop

A morphism is cartesian if the gap map is unique.

Equations

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

def CategoryTheory.CartMor {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) : CategoryTheory.MorphismProperty E

The class of cartesian morphisms

Equations

• CategoryTheory.CartMor P g = CategoryTheory.isCartesianMorphism g

noncomputable def CategoryTheory.gapmap {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} (g : x ⟶ y) (gcart : CategoryTheory.CartMor P g) {z : E} (u : P.obj z ⟶ P.obj x) (g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u (P.map g)) (Fiber.tauto z) (Fiber.tauto y)) : z ⟶ x

gapmap g gcart u g' is a unique morphism l over u such that l ≫ g = g'.

Equations

• CategoryTheory.gapmap g gcart u g' = (Classical.choose ⋯).hom

@[simp]

theorem CategoryTheory.gapmap_over {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} {g : x ⟶ y} {gcart : CategoryTheory.CartMor P g} {z : E} {u : P.obj z ⟶ P.obj x} {g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u (P.map g)) (Fiber.tauto z) (Fiber.tauto y)} : P.map (CategoryTheory.gapmap g gcart u g') = u

@[simp]

theorem CategoryTheory.gapmap_property {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_4, u_1} C] [CategoryTheory.Category.{u_3, u_2} E] {P : CategoryTheory.Functor E C} {x : E} {y : E} {g : x ⟶ y} {gcart : CategoryTheory.CartMor P g} {z : E} {u : P.obj z ⟶ P.obj x} {g' : CategoryTheory.BasedLift P (CategoryTheory.CategoryStruct.comp u (P.map g)) (Fiber.tauto z) (Fiber.tauto y)} : CategoryTheory.CategoryStruct.comp (CategoryTheory.gapmap g gcart u g') g = g'.hom

The composition of the gap map of a map g' and the cartesian lift g is the given map g'.

theorem CategoryTheory.cart_id {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} (e : E) : CategoryTheory.CartMor P (CategoryTheory.CategoryStruct.id e)

cart_id e says that the identity morphism 𝟙 e is cartesian.

class CategoryTheory.CartBasedLifts {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] (P : CategoryTheory.Functor E C) {c : C} {d : C} (f : c ⟶ d) (src : P ⁻¹ c) (tgt : P ⁻¹ d) extends CategoryTheory.BasedLift : Type (max (max (max u_1 u_2) u_3) u_4)

Given a morphism f in the base category C, the type CartLifts P f src tgt consists of the based-lifts of f with the source src and the target tgt which are cartesian with respect to P.

• hom : ↑src ⟶ ↑tgt
• over : CategoryTheory.CategoryStruct.comp (P.map CategoryTheory.CartBasedLifts.toBasedLift.hom) (CategoryTheory.eqToHom ⋯) = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) f
• is_cart : CategoryTheory.CartesianBasedLift CategoryTheory.CartBasedLifts.toBasedLift

instance CategoryTheory.instCoeHomOfCartBasedLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (src : P ⁻¹ c) (tgt : P ⁻¹ d) : CoeOut (CategoryTheory.CartBasedLifts P f src tgt) (↑src ⟶ ↑tgt)

Equations

• CategoryTheory.instCoeHomOfCartBasedLift f src tgt = { coe := fun (l : CategoryTheory.CartBasedLifts P f src tgt) => CategoryTheory.CartBasedLifts.toBasedLift.hom }

class CategoryTheory.CartLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (y : P ⁻¹ d) extends CategoryTheory.Lift : Type (max (max (max u_1 u_2) u_3) u_4)

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

• src : P ⁻¹ c
• based_lift : CategoryTheory.BasedLift P f CategoryTheory.CartLift.toLift.src y
• is_cart : {x x_1 : C} → {x_2 : x ⟶ x_1} → {x_3 : P ⁻¹ x} → {x_4 : P ⁻¹ x_1} → {lift : CategoryTheory.BasedLift P x_2 x_3 x_4} → CategoryTheory.CartesianBasedLift lift

def CategoryTheory.CartLift.homOf {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {y : P ⁻¹ d} (g : CategoryTheory.CartLift f y) : ↑CategoryTheory.CartLift.toLift.src ⟶ ↑y

Equations

• g.homOf = CategoryTheory.CartLift.toLift.based_lift.hom

instance CategoryTheory.instCoeLiftOfCartLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} {f : c ⟶ d} {y : P ⁻¹ d} : Coe (CategoryTheory.CartLift f y) (CategoryTheory.Lift P f y)

Equations

• CategoryTheory.instCoeLiftOfCartLift = { coe := fun (l : CategoryTheory.CartLift f y) => CategoryTheory.CartLift.toLift }

class CategoryTheory.CoCartLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (x : P ⁻¹ c) extends CategoryTheory.CoLift : Type (max (max (max u_1 u_2) u_3) u_4)

• tgt : P ⁻¹ d
• based_colift : CategoryTheory.BasedLift P f x CategoryTheory.CoCartLift.toCoLift.tgt
• is_cart : {x x_1 : C} → {x_2 : x ⟶ x_1} → {x_3 : P ⁻¹ x} → {x_4 : P ⁻¹ x_1} → {colift : CategoryTheory.BasedLift P x_2 x_3 x_4} → CategoryTheory.CoCartesianBasedLift colift

def CategoryTheory.HasCartLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (y : P ⁻¹ d) : Prop

Mere existence of a cartesian lift with fixed target.

Equations

• CategoryTheory.HasCartLift f y = Nonempty (CategoryTheory.CartLift f y)

def CategoryTheory.HasCoCartLift {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} {c : C} {d : C} (f : c ⟶ d) (x : P ⁻¹ c) : Prop

Equations

• CategoryTheory.HasCoCartLift f x = Nonempty (CategoryTheory.CoCartLift f x)

@[reducible, inline]

abbrev CategoryTheory.Cart {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] : CategoryTheory.Functor E C → Type u_2

Equations

• CategoryTheory.Cart x = E

instance CategoryTheory.instCategoryCart {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} : CategoryTheory.Category.{u_4, u_2} (CategoryTheory.Cart P)

The subcategory of cartesian morphisms.

Equations

• CategoryTheory.instCategoryCart = CategoryTheory.Category.mk ⋯ ⋯ ⋯

def CategoryTheory.Cart.forget {C : Type u_1} {E : Type u_2} [CategoryTheory.Category.{u_3, u_1} C] [CategoryTheory.Category.{u_4, u_2} E] {P : CategoryTheory.Functor E C} : CategoryTheory.Functor (CategoryTheory.Cart P) E

The forgetful functor from the category of cartesian morphisms to the domain category.

Equations

• CategoryTheory.Cart.forget = { obj := fun (x : CategoryTheory.Cart P) => x, map := fun (x y : CategoryTheory.Cart P) (f : x ⟶ y) => f, map_id := ⋯, map_comp := ⋯ }