freeYonedaEquiv_comp — Mathlib

English

The bijection given by the free Yoneda equivalence is compatible with post-composition by presheaf morphisms: applying the equivalence after composing with a morphism φ: M → N is the same as applying φ to the result of the equivalence on m.

Русский

Биекция, заданная свободной Yoneda-эквивалентностью, сохраняет композицию: применение эквивалентности после композиции с морфизмом φ: M → N равно применению φ к результату эквивалентности на m.

LaTeX

$$$\\mathrm{freeYonedaEquiv}(m \\circ φ) = φ_X(\\mathrm{freeYonedaEquiv}(m))$$$

Lean4

theorem freeYonedaEquiv_comp {M N : PresheafOfModules.{v} R} {X : C} (m : ((free R).obj (yoneda.obj X) ⟶ M))
    (φ : M ⟶ N) : freeYonedaEquiv (m ≫ φ) = φ.app _ (freeYonedaEquiv m) :=
  rfl

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