freeYonedaHomEquiv_comp — Mathlib

English

The bijection freeYonedaHomEquiv commutes with composition: freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X).

Русский

Связь freeYonedaHomEquiv совместима с композициями: freeYonedaHomEquiv(α ≫ f) = freeYonedaHomEquiv(α) ≫ f.app(op X).

LaTeX

$$$\mathrm{freeYonedaHomEquiv}(\alpha \ggg f) = \mathrm{freeYonedaHomEquiv}(\alpha) \ggg f.{op X}$$$

Lean4

@[reassoc]
theorem freeYonedaHomEquiv_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : freeYoneda X M ⟶ F) (f : F ⟶ G) :
    freeYonedaHomEquiv (α ≫ f) = freeYonedaHomEquiv α ≫ f.app (op X) := by simp [freeYonedaHomEquiv]

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