comp — Mathlib

English

The hom component of the composite Ext corresponds to the composite of hom components.

Русский

Гом-компонента композиции Ext равна композиции гомоморфизмов.

LaTeX

$$$(\alpha.comp\beta\; h).hom = \alpha.hom \circ \beta.hom (\; h \;)$$$

Lean4

/-- The composition of `Ext`. -/
noncomputable def comp {a b : ℕ} (α : Ext X Y a) (β : Ext Y Z b) {c : ℕ} (h : a + b = c) : Ext X Z c :=
  SmallShiftedHom.comp α β (by cutsat)

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