English
If F sends every limit cocone over a profinite S to a colimit, then the left Kan extension of F is naturally isomorphic to F itself, i.e., there is a natural isomorphism between LanPresheaf F and F.
Русский
Если F переводит каждый предел-коаконию над профинитовым пространством S в колимит, то левое Кан-extension к F из F естественным образом изомерен с F, то есть существует естественная изоморфизм LanPresheaf F ≅ F.
LaTeX
$$$\\ LanPresheaf F \\cong F$, (natural in $S$) for which the components give isomorphisms $\\left(\\text{lanPresheafNatIso}\\,hF\\right)_S : (\\text{LanPresheaf} F)(S) \\cong F(S)$.$$
Lean4
/-- `lanPresheafIso` is natural in `S`. -/
def lanPresheafNatIso (hF : ∀ S : Profinite, IsColimit <| F.mapCocone S.asLimitCone.op) : lanPresheaf F ≅ F :=
NatIso.ofComponents (fun ⟨S⟩ ↦ (lanPresheafIso (hF S))) fun _ ↦ (by simpa using colimit.hom_ext fun _ ↦ (by simp))
