ι_fromFreeYonedaCoproduct_apply — Mathlib

English

For m in M.Elements and X in C^op, the application of M.fromFreeYonedaCoproduct to the coproduct element matches m.fromFreeYoneda applied to the corresponding freeYoneda element.

Русский

Для m ∈ M.Elements и X в C^op, применение M.fromFreeYonedaCoproduct к элементу копродукта совпадает с m.fromFreeYoneda, примененным к соответствующему элементу freeYoneda.

LaTeX

$$$M.fromFreeYonedaCoproduct.app X ((M.ιFreeYonedaCoproduct m).app X x) = m.fromFreeYoneda.app X x$$$

Lean4

theorem ι_fromFreeYonedaCoproduct_apply (m : M.Elements) (X : Cᵒᵖ) (x : m.freeYoneda.obj X) :
    M.fromFreeYonedaCoproduct.app X ((M.ιFreeYonedaCoproduct m).app X x) = m.fromFreeYoneda.app X x :=
  congr_fun ((evaluation R X ⋙ forget _).congr_map (M.ι_fromFreeYonedaCoproduct m)) x

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