English
Given a short exact S in an abelian category C, the covariant long exact sequence in Ext obtained by X and the shifted Ext groups is exact at all terms when n varies. In particular, the construction Ext X S.X₂ n → Ext X S.X₁ n → Ext X S.X₃ n is exact for all n.
Русский
Для заданной короткой точной последовательности S в абелевой категории C выписывается ковариантная длинная точная последовательность в Ext, получаемая из X и смещённых групп Ext; последовательность \nExt^n(X,S.X₂) → Ext^n(X,S.X₁) → Ext^n(X,S.X₃) — точная для всех n.
LaTeX
$$$\\big(\\mathrm{covariantSequence}(X,hS,n,n',h)\\big).Exact$$$
Lean4
/-- Alternative formulation of `covariant_sequence_exact₃` -/
theorem covariant_sequence_exact₃' :
(ShortComplex.mk (AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X (add_zero n₀)))
(AddCommGrpCat.ofHom (hS.extClass.postcomp X h))
(by
ext x
dsimp
simp only [comp_assoc_of_second_deg_zero, ShortComplex.ShortExact.comp_extClass, comp_zero])).Exact :=
by
letI := HasDerivedCategory.standard C
have :=
(preadditiveCoyoneda.obj (op ((singleFunctor C 0).obj X))).homologySequence_exact₃ _
(hS.singleTriangle_distinguished) n₀ n₁ (by cutsat)
rw [ShortComplex.ab_exact_iff_function_exact] at this ⊢
apply
Function.Exact.of_ladder_addEquiv_of_exact' (e₁ := Ext.homAddEquiv) (e₂ := Ext.homAddEquiv) (e₃ := Ext.homAddEquiv)
(H := this)
· ext x; apply hom_comp_singleFunctor_map_shift (C := C)
· ext x
exact preadditiveCoyoneda_homologySequenceδ_singleTriangle_apply hS x h
