English
If a sequential cone in LightProfinite consists of finite sets and the cone is limiting, the extended functor is initial.
Русский
Если последовательный конус в LightProfinite состоит из конечных множеств и конус ограничен, то расширенный функтор является начальным.
LaTeX
$$$\\text{FunctorInitial }(c)\\Rightarrow \\text{Initial}(\\text{LightProfiniteExtend.}c)$$$
Lean4
/-- If the projection maps in the cone are epimorphic and the cone is limiting, then
`LightProfinite.Extend.functorOp` is final.
-/
theorem functorOp_final (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Final (functorOp c) :=
by
have := functor_initial c hc
have : ((StructuredArrow.toCostructuredArrow toLightProfinite c.pt)).IsEquivalence :=
(inferInstance : (structuredArrowOpEquivalence _ _).functor.IsEquivalence)
have : (functor c).rightOp.Final := inferInstanceAs ((opOpEquivalence ℕ).inverse ⋙ (functor c).op).Final
exact Functor.final_comp (functor c).rightOp _
