English
If two functors F and G have equivalent cone categories, the limiting cones are transported across this equivalence: there is an equivalence IsLimit(h.functor.obj c) ≃ IsLimit c.
Русский
Если два функторы F и G имеют эквивалентные категории конусов, пределы переносятся через это эквивалентность: IsLimit(h.functor.obj c) ≃ IsLimit c.
LaTeX
$$$ IsLimit(h.functor.obj c) \\simeq IsLimit(c) $$$
Lean4
/-- Given two functors which have equivalent categories of cones, we can transport a limiting cone
across the equivalence.
-/
def ofConeEquiv {D : Type u₄} [Category.{v₄} D] {G : K ⥤ D} (h : Cone G ≌ Cone F) {c : Cone G} :
IsLimit (h.functor.obj c) ≃ IsLimit c
where
toFun P := ofIsoLimit (ofRightAdjoint h.toAdjunction P) (h.unitIso.symm.app c)
invFun := ofRightAdjoint h.symm.toAdjunction
left_inv := by cat_disch
right_inv := by cat_disch
