freeYonedaHomEquiv_symm_comp — Mathlib

English

The symmetric version of the above: freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)).

Русский

Симметричная версия: freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)).

LaTeX

$$$\mathrm{freeYonedaHomEquiv\_symm}(\alpha) \;\gggg\; f = \mathrm{freeYonedaHomEquiv\_symm}(\alpha \ggg f.app(op X))$$$

Lean4

@[reassoc]
theorem freeYonedaHomEquiv_symm_comp {X : C} {M : A} {F G : Cᵒᵖ ⥤ A} (α : M ⟶ F.obj (op X)) (f : F ⟶ G) :
    freeYonedaHomEquiv.symm α ≫ f = freeYonedaHomEquiv.symm (α ≫ f.app (op X)) :=
  by
  obtain ⟨β, rfl⟩ := freeYonedaHomEquiv.surjective α
  apply freeYonedaHomEquiv.injective
  simp only [Equiv.symm_apply_apply, freeYonedaHomEquiv_comp, Equiv.apply_symm_apply]

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