isoFinYonedaComponents_hom_apply — Mathlib

English

For y in F(X) and x in X, the hom action of isoFinYonedaComponents on y and x is given by F.map of the constant map at x applied to y.

Русский

Для элемента y в F(X) и элемента x из X, действие гомоморфизма isoFinYonedaComponents на y и x задаётся как F.map константной функции на x applied к y.

LaTeX

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

Lean4

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

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