whiskering_linearYoneda — Mathlib

English

Composing linear Yoneda with whiskering on the right by forgetful functor yields the standard Yoneda, i.e., linearYoneda ⋙ whiskeringRight ... forget = yoneda.

Русский

Сочетание линейного Yoneda с правым whiskering даёт обычный Yoneda: линейный Yoneda ⋙ whiskeringRight ... forget = yoneda.

LaTeX

$$$\\text{whiskering\_linearYoneda} : \\text{linearYoneda}\\_R(C) \\circ (\\text{whiskeringRight} (\\mathrm{Opposite}\\,C) \\dots ) = \\text{yoneda}$$$

Lean4

@[simp]
theorem whiskering_linearYoneda : linearYoneda R C ⋙ (whiskeringRight _ _ _).obj (forget (ModuleCat.{v} R)) = yoneda :=
  rfl

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