English
The composition of Ext groups is bilinear: for X,Y,Z objects and natural numbers a,b,c with h: a+b=c, there is a bilinear map Ext X Y a →+ Ext Y Z b →+ Ext X Z c; this map is given by the Yoneda product α ∘ β when a,b,c match with h.
Русский
Произведение Ext-объектов по трём фигурам даёт билинейную операцию: существует билинеарная карта Ext^a(X,Y) × Ext^b(Y,Z) → Ext^c(X,Z) при a+b=c, заданная композиціей Яноды.
LaTeX
$$$\text{bilinearComp}(X,Y,Z;a,b,c,h):\ Ext^a(X,Y) \to^+ Ext^b(Y,Z) \to^+ Ext^c(X,Z)$ с $h:\ a+b=c$ и $\big(\alpha,\beta\big) \mapsto \alpha \circ \beta$.$$
Lean4
/-- The composition of `Ext`, as a bilinear map. -/
@[simps!]
noncomputable def bilinearComp (a b c : ℕ) (h : a + b = c) : Ext X Y a →+ Ext Y Z b →+ Ext X Z c :=
AddMonoidHom.mk' (fun α ↦ AddMonoidHom.mk' (fun β ↦ α.comp β h) (by simp)) (by aesop)
