English
There is an equivalence of IsLimit between mapped cones and mapped fans: IsLimit(G.mapCone(Fan.mk P g)) ≃ IsLimit(Fan.mk (G P) (G.map ∘ g)).
Русский
Существует эквиваленция IsLimit между отображёнными конусами и объединенными конусами: IsLimit(G.mapCone(Fan.mk P g)) ≃ IsLimit(Fan.mk (G P) (G.map ∘ g)).
LaTeX
$$$\text{IsLimit}(\mathrm{mapCone}\ G\ (\mathrm{Fan.mk}\ P\ g)) \simeq \text{IsLimit}(\mathrm{Fan.mk}\ (G\cdot P)\ (\lambda j. G.map( g\, j )))$$$
Lean4
/-- The map of a fan is a limit iff the fan consisting of the mapped morphisms is a limit. This
essentially lets us commute `Fan.mk` with `Functor.mapCone`.
-/
def isLimitMapConeFanMkEquiv {P : C} (g : ∀ j, P ⟶ f j) :
IsLimit (Functor.mapCone G (Fan.mk P g)) ≃ IsLimit (Fan.mk _ fun j => G.map (g j) : Fan fun j => G.obj (f j)) :=
by
refine (IsLimit.postcomposeHomEquiv ?_ _).symm.trans (IsLimit.equivIsoLimit ?_)
· refine Discrete.natIso fun j => Iso.refl (G.obj (f j.as))
refine Cones.ext (Iso.refl _) fun j => by dsimp; cases j; simp
