Ext — Mathlib

English

The Ext groups compose: given α ∈ Ext(X,Y,a) and β ∈ Ext(Y,Z,b) with a+b=c, we get an element in Ext(X,Z,c) defined by the sum shift.

Русский

Объединение Ext: из α ∈ Ext(X,Y,a) и β ∈ Ext(Y,Z,b) при a+b=c получаем элемент Ext(X,Z,c).

LaTeX

$$$\alpha \in Ext(X,Y,a),\ \beta \in Ext(Y,Z,b)\Rightarrow \alpha\comp\beta(h) \in Ext(X,Z,a+b)$$$

Lean4

/-- A Ext-group in an abelian category `C`, defined as a `Type w` when `[HasExt.{w} C]`. -/
def Ext (X Y : C) (n : ℕ) : Type w :=
  SmallShiftedHom.{w} (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ((CochainComplex.singleFunctor C 0).obj X)
    ((CochainComplex.singleFunctor C 0).obj Y) (n : ℤ)

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