homAddEquiv_apply — Mathlib

English

For any objects X, Y in an abelian category and any natural number n, the canonical bilinear identification (homAddEquiv) on Ext X Y n selects the underlying morphism of the extension α; i.e., the equivalence sends α to its defining morphism α.hom.

Русский

Для любых объектов X, Y в абелевой категории и натурального числа n существует каноническое билинейное соответствие, инициализируемое как homAddEquiv, которое переводит экстенсионный класс α в отображение-основание α.hom.

LaTeX

$$$\operatorname{homAddEquiv}(\alpha) = \alpha_{\mathrm{hom}}$$$

Lean4

@[simp]
theorem homAddEquiv_apply (α : Ext X Y n) : homAddEquiv α = α.hom :=
  rfl

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