English
Under an equivalence of cone categories, the image of a lift under the equivalence equals an explicit composition described by unit and inverse quasi-inverses; i.e., (ofConeEquiv h P).lift s equals a certain composite built from unit, P, and h.
Русский
При эквивалентности категорий конусов образ подъёма через эквивариантность равен определённому Композиции, записанному через модуль единицы и обратной связи; т. е. (ofConeEquiv h P).lift s равно заданной композиции.
LaTeX
$$$ (ofConeEquiv\, h\, P).lift\, s = ((h.unitIso.hom.app s).hom \\circ (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) \\circ (h.unitIso.inv.app c).hom $$$
Lean4
@[simp]
theorem ofConeEquiv_apply_desc {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G}
(P : IsLimit (h.functor.obj c)) (s) :
(ofConeEquiv h P).lift s =
((h.unitIso.hom.app s).hom ≫ (h.inverse.map (P.liftConeMorphism (h.functor.obj s))).hom) ≫
(h.unitIso.inv.app c).hom :=
rfl
