English
Let c be a limit cone for F ⋙ toLightProfinite and suppose [∀ i, Epi (c.π.app i)]. Then Initial (LightProfinite.Extend.functor c).
Русский
Пусть c является пределом конуса для F ⋙ toLightProfinite и выполняется условие, что ∀ i, Epi (c.π.app i). Тогда LightProfinite.Extend.functor c является начальствующим функтором.
LaTeX
$$$\mathrm{Initial}(\mathrm{LightProfinite.Extend.functor}(c))$$$
Lean4
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`LightProfinite.Extend.functor` is initial.
-/
theorem functor_initial (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Initial (functor c) :=
by
rw [initial_iff_comp_equivalence _ (StructuredArrow.post _ _ lightToProfinite)]
have : ∀ i, Epi ((lightToProfinite.mapCone c).π.app i) := fun i ↦
inferInstanceAs (Epi (lightToProfinite.map (c.π.app i)))
exact Profinite.Extend.functor_initial _ (isLimitOfPreserves lightToProfinite hc)
