English
The inverse side of isoLocallyConstantOfIsColimit equals the counit applied to X, i.e., the counit map from LocallyConstant to X yields the inverse of the isomorphism.
Русский
Обратная часть изоморфизма isoLocallyConstantOfIsColimit совпадает с counit, применённым к X.
LaTeX
$$$(\\text{isoLocallyConstantOfIsColimit } X hX).inv = (\\mathrm{CompHausLike.LocallyConstant.counitApp})_X$$$
Lean4
/-- A presheaf `F`, which takes a profinite set written as a cofiltered limit to the corresponding
colimit, is isomorphic to the presheaf `LocallyConstant - F(*)`.
-/
def isoLocallyConstantOfIsColimit (hF : ∀ S : Profinite, IsColimit <| F.mapCocone S.asLimitCone.op) :
F ≅ (locallyConstantPresheaf (F.obj (toProfinite.op.obj ⟨of PUnit.{u + 1}⟩))) :=
(lanPresheafNatIso hF).symm ≪≫
lanPresheafExt (isoFinYoneda F ≪≫ (locallyConstantIsoFinYoneda F).symm) ≪≫
lanPresheafNatIso fun _ ↦ isColimitLocallyConstantPresheafDiagram _ _
