English
If a functor F takes a light profinite set S to a colimit diagram via Cocone RightOpOfCone, then F is isomorphic to the locally constant presheaf at F at the base point, i.e., F ≅ locallyConstantPresheaf (F.obj (toLightProfinite.op.obj ⟨of PUnit⟩)).
Русский
Если функктор F переводит световую профинетическую множество S к колимитному диаграмме через Cocone RightOpOfCone, то F изоморфен локально константному предsheaf-у на F(*).
LaTeX
$$There is an isomorphism $F \cong \mathrm{locallyConstantPresheaf}(F(\mathrm{toLightProfinite.op.obj} \langle \mathrm{of\,PUnit} \rangle))$$$
Lean4
/-- A presheaf `F`, which takes a light profinite set written as a sequential limit to the corresponding
colimit, is isomorphic to the presheaf `LocallyConstant - F(*)`.
-/
def isoLocallyConstantOfIsColimit
(hF : ∀ S : LightProfinite, IsColimit <| F.mapCocone (coconeRightOpOfCone S.asLimitCone)) :
F ≅ (locallyConstantPresheaf (F.obj (toLightProfinite.op.obj ⟨of PUnit.{u + 1}⟩))) :=
(lanPresheafNatIso hF).symm ≪≫
lanPresheafExt (isoFinYoneda F ≪≫ (locallyConstantIsoFinYoneda F).symm) ≪≫
lanPresheafNatIso fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _
