yonedaEquiv_symm_naturality_right

English

Right naturality for yonedaEquiv_symm: yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app X x).

Русский

Правая естественность yonedaEquiv_symm: yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app X x).

LaTeX

$$$ yonedaEquiv.symm x \\; \\gg \\; f = yonedaEquiv.symm (f.app { \\operatorname{unop} X \\} x) $$$

Lean4

theorem yonedaEquiv_symm_naturality_right (X : C) {F F' : Cᵒᵖ ⥤ Type v₁} (f : F ⟶ F') (x : F.obj ⟨X⟩) :
    yonedaEquiv.symm x ≫ f = yonedaEquiv.symm (f.app ⟨X⟩ x) :=
  by
  apply yonedaEquiv.injective
  simp [yonedaEquiv_comp]

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