comp_extClass_assoc — Mathlib

English

The composition of Ext.mk₀ S.g with hS.extClass is zero after composing with 1, reflecting associativity of the Ext-extension boundary.

Русский

Композиция Ext.mk₀ S.g с hS.extClass нулируется после композиции с 1, отражая ассоциативность границы расширения Ext.

LaTeX

$$$(\\mathrm{Ext.mk}_0 S.g)\\circ (hS.extClass)\\circ (\\mathrm{zero\\_add}\,1) = 0$$$

Lean4

@[simp]
theorem comp_extClass_assoc {Y : C} {n : ℕ} (γ : Ext S.X₁ Y n) {n' : ℕ} (h : 1 + n = n') :
    (Ext.mk₀ S.g).comp (hS.extClass.comp γ h) (zero_add n') = 0 := by
  rw [← Ext.comp_assoc (a₁₂ := 1) _ _ _ (by cutsat) (by cutsat) (by cutsat), comp_extClass, Ext.zero_comp]

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