extClass_comp_assoc — Mathlib

English

For every γ in Ext S.X₂ Y n and Y, n', h satisfying the stated equation, the extClass composed with Ext.mk₀ S.f and γ again yields zero.

Русский

Для любого элемента γ из Ext(S.X₂, Y, n) и подходящих нулевых индикаторов, композиция extClass с Ext.mk₀(S.f) и γ снова равна нулю.

LaTeX

$$$h_S^{\\text{ext}} \\circ \\big( \\mathrm{Ext.mk}_0(S.f) \\circ \\gamma \\circ (0 + n) \\big) \\circ h = 0$$$

Lean4

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

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