English
There is a natural isomorphism between F evaluated at a finite X and the product of X-indexed copies of F at a unit profinite, i.e., Fin Yoneda components give an isomorphism F(X) ≅ X → F(Profinite.of PUnit).
Русский
Существует естественная изоморфность между F( X ) и X-ий копий F( Profinite.of PUnit ), то есть компоненты Fin Yoneda дают изоморфность F(X) ≅ X → F(Profinite.of PUnit).
LaTeX
$$$F([X]) \\cong (X \\to F([\\mathrm{Profinite.of}(PUnit)])).$$$
Lean4
/-- Auxiliary definition for `isoFinYoneda`. -/
def isoFinYonedaComponents (X : Profinite.{u}) [Finite X] : F.obj ⟨X⟩ ≅ (X → F.obj ⟨Profinite.of PUnit.{u + 1}⟩) :=
(isLimitFanMkObjOfIsLimit F _ _ (Cofan.IsColimit.op (fintypeCatAsCofanIsColimit X))).conePointUniqueUpToIso
(Types.productLimitCone.{u, u + 1} fun _ ↦ F.obj ⟨Profinite.of PUnit.{u + 1}⟩).2
