hom — Mathlib

English

The canonical map from morphisms X → Y to Ext X Y 0 is given by mk₀.

Русский

Каноническое отображение из (X → Y) в Ext X Y 0 задаётся как mk₀.

LaTeX

$$$mk_0\ (f:X\to Y) : Ext\ X\ Y\ 0$$$

Lean4

/-- The morphism in the derived category which corresponds to an element in `Ext X Y a`. -/
noncomputable abbrev hom {a : ℕ} (α : Ext X Y a) :
    ShiftedHom ((singleFunctor C 0).obj X) ((singleFunctor C 0).obj Y) (a : ℤ) :=
  homEquiv α

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