English
If X is a CondensedSet and, for all Profinite S, IsColimit holds for (profiniteToCompHaus.op.comp X.val).mapCocone S.asLimitCone.op, then X lies in the essential image of LocallyConstant functor.
Русский
Если X — CondensedSet и для всякого Profinite S тождественно выполняется свойство IsColimit для соответствующего отображения, то X принадлежит к м),( EssImage) локально постоянного функторa.
LaTeX
$$$\\forall S:\\ Profinite,\\ IsColimit\\bigl((profiniteToCompHaus.op \\circ X.val) . mapCocone S.asLimitCone.op\\bigr) \\Rightarrow X \\\\in\\mathrm{essImage}(\\mathrm{LocallyConstant.functor})$$$
Lean4
theorem mem_locallyConstant_essImage_of_isColimit_mapCocone (X : CondensedSet.{u})
(h : ∀ S : Profinite.{u}, IsColimit <| (profiniteToCompHaus.op ⋙ X.val).mapCocone S.asLimitCone.op) :
CondensedSet.LocallyConstant.functor.essImage X :=
by
let e : CondensedSet.{u} ≌ Sheaf (coherentTopology Profinite) _ :=
(Condensed.ProfiniteCompHaus.equivalence (Type (u + 1))).symm
let i : (e.functor.obj X).val ≅ (e.functor.obj (LocallyConstant.functor.obj _)).val :=
Condensed.isoLocallyConstantOfIsColimit _ h
exact ⟨_, ⟨e.functor.preimageIso ((sheafToPresheaf _ _).preimageIso i.symm)⟩⟩
