homAddEquiv_add — Mathlib

English

The additive Yoneda-like isomorphism maps hom-sets to Yoneda-constructed objects respecting addition.

Русский

Аддитивное подобие yoneda отображает множество гомоморфизмов в yoneda-объекты с сохранением сложения.

LaTeX

$$$\text{compPreadditiveYonedaIso.hom.app}$$$

Lean4

@[simp]
theorem homAddEquiv_add (X : C) (Y : D) (f f' : F.obj X ⟶ Y) :
    adj.homEquiv X Y (f + f') = adj.homEquiv X Y f + adj.homEquiv X Y f' :=
  map_add (adj.homAddEquiv X Y) _ _

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