English
The inverse of the Fin Yoneda components respects precomposition via the map g, mirroring the hom-formula forisoFinYonedaComponents_inv_comp.
Русский
Обратная компонента Fin Yoneda сохраняет предсоставление через отображение g (inv_comp).
LaTeX
$$$\\big(\\text{isoFinYonedaComponents } F X\\big).inv (f \\circ g) = F.map g^{op} ((\\text{isoFinYonedaComponents } F Y).inv f)$$$
Lean4
/-- A presheaf, which takes a light profinite set written as a sequential limit to the corresponding
colimit, agrees with the left Kan extension of its restriction.
-/
def lanPresheafIso (hF : IsColimit <| F.mapCocone (coconeRightOpOfCone S.asLimitCone)) :
(lanPresheaf F).obj ⟨S⟩ ≅ F.obj ⟨S⟩ :=
(Functor.Final.colimitIso (LightProfinite.Extend.functorOp S.asLimitCone) _).symm ≪≫
(colimit.isColimit _).coconePointUniqueUpToIso hF
