extClass_comp — Mathlib

English

In an abelian category, for a short exact sequence S, the Ext-class attached to S vanishes after precomposing with the canonical map Ext.mk₀(S.f) and then shifting by 1.

Русский

В абелевой категории для короткой точной последовательности S соответствующий Ext‑класс обнуляется после предварного композиционного применения канонической маппинга Ext.mk₀(S.f) и сдвига на единицу.

LaTeX

$$$h_S^{\\text{ext}} \\circ \\mathrm{Ext.mk}_0(S.f) \\circ (\\text{add\_zero } 1) = 0$$$

Lean4

@[simp]
theorem extClass_comp : hS.extClass.comp (Ext.mk₀ S.f) (add_zero 1) = 0 :=
  by
  letI := HasDerivedCategory.standard C
  ext
  simp only [Ext.comp_hom, Ext.mk₀_hom, extClass_hom, Ext.zero_hom, ShiftedHom.comp_mk₀]
  exact comp_distTriang_mor_zero₃₁ _ hS.singleTriangle_distinguished

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