English
If c is a limit cone for F ⋙ toLightProfinite and G.mapCone c is a limit cone, and each projection c.π.app i is epi, then cone G c.pt is a limit cone.
Русский
Если c является пределом конуса для F ⋙ toLightProfinite и G.mapCone c является пределом конуса, причём все проекции c.π.app i — эпиморфизмы, тогда конус cone G c.pt является пределом конуса.
LaTeX
$$$\bigl(\mathrm{IsLimit}(c)\bigr) \wedge \bigl(\forall i, \operatorname{Epi}(c.\pi. app i)\bigr) \wedge \mathrm{IsLimit}(G.mapCone c) \Rightarrow \mathrm{IsLimit}(\mathrm{cone} \, G\, c.pt).$$$
Lean4
/-- If `c` and `G.mapCone c` are limit cones and the projection maps in `c` are epimorphic,
then `cone G c.pt` is a limit cone.
-/
noncomputable def isLimitCone (hc : IsLimit c) [∀ i, Epi (c.π.app i)] (hc' : IsLimit <| G.mapCone c) :
IsLimit (cone G c.pt) :=
(functor_initial c hc).isLimitWhiskerEquiv _ _ hc'
