isoFinYonedaComponents_hom_apply — Mathlib

English

For y ∈ F(X) and x ∈ X, the hom component of isoFinYonedaComponents at X satisfies (isoFinYonedaComponents F X).hom y x = F.map ((LightProfinite.of PUnit).const x).op y.

Русский

Для y ∈ F(X) и x ∈ X компонент отображения (isoFinYonedaComponents F X).hom на y и x равен F.map (изображение константы, выбирающее x) от y.

LaTeX

$$$(\text{isoFinYonedaComponents } F X)\mathrm{hom}\; y\; x = F.map\big((\mathrm{LightProfinite.of\,PUnit}).\mathrm{const}\; x\)^{\mathrm{op}}\; y$$$

Lean4

theorem isoFinYonedaComponents_hom_apply (X : LightProfinite.{u}) [Finite X] (y : F.obj ⟨X⟩) (x : X) :
    (isoFinYonedaComponents F X).hom y x = F.map ((LightProfinite.of PUnit.{u + 1}).const x).op y :=
  rfl

Похожие утверждения