English
For a functor F : (Opposite LightProfinite) ⥤ Type that preserves finite products, and a finite X, there is a natural isomorphism F(X) ≅ X → F( LightProfinite.of PUnit ).
Русский
Пусть F : (противоположное LightProfinite) ⥤ Type сохраняет конечные произведения, и X — конечное множество; существует естественное изоморфизм F(X) ≅ X → F( LightProfinite.of PUnit ).
LaTeX
$$$F(X) \cong X \to F(\mathrm{LightProfinite.of\,PUnit})$$$
Lean4
/-- Auxiliary definition for `isoFinYoneda`. -/
def isoFinYonedaComponents (X : LightProfinite.{u}) [Finite X] :
F.obj ⟨X⟩ ≅ (X → F.obj ⟨LightProfinite.of PUnit.{u + 1}⟩) :=
(isLimitFanMkObjOfIsLimit F _ _ (Cofan.IsColimit.op (fintypeCatAsCofanIsColimit X))).conePointUniqueUpToIso
(Types.productLimitCone.{u, u} fun _ ↦ F.obj ⟨LightProfinite.of PUnit.{u + 1}⟩).2
