English
There is a canonical isomorphism between the LanPresheaf along a S and the original F mapped to S via an IsColimit and a cocone-based isomorphism; equivalently, the presheaf agrees with its left Kan extension along the extension functor on S.
Русский
Существует каноническое изоморфизм между LanPresheaf и исходным F на S через изоморфизм IsColimit и кокон; тождественность прешефа и левого вычисления канонического расширения на S.
LaTeX
$$$\\mathrm{lanPresheafIso}\\; hF : (\\mathrm{lanPresheaf F}).obj\\langle S\\rangle \\cong F.\\mathrm{obj}\\langle S\\rangle$$$
Lean4
/-- A presheaf, which takes a profinite set written as a cofiltered limit to the corresponding
colimit, agrees with the left Kan extension of its restriction.
-/
def lanPresheafIso (hF : IsColimit <| F.mapCocone S.asLimitCone.op) : (lanPresheaf F).obj ⟨S⟩ ≅ F.obj ⟨S⟩ :=
(Functor.Final.colimitIso (Profinite.Extend.functorOp S.asLimitCone) _).symm ≪≫
(colimit.isColimit _).coconePointUniqueUpToIso hF
