English
The constructed covariant long exact Ext sequence is exact as a sequence of composable arrows.
Русский
Построенная ковариантная длинная точная последовательность в Ext является точной последовательностью композиционных стрелок.
LaTeX
$$$\\big(\\mathrm{covariantSequence}(X,hS,n_0,n_1,h)\\big).\\mathrm{Exact}$$$
Lean4
/-- Given a short exact short complex `S` in an abelian category `C` and an object `X : C`,
this is the long exact sequence
`Ext X S.X₁ n₀ → Ext X S.X₂ n₀ → Ext X S.X₃ n₀ → Ext X S.X₁ n₁ → Ext X S.X₂ n₁ → Ext X S.X₃ n₁`
when `n₀ + 1 = n₁` -/
noncomputable def covariantSequence : ComposableArrows AddCommGrpCat.{w} 5 :=
mk₅ (AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X (add_zero n₀)))
(AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X (add_zero n₀))) (AddCommGrpCat.ofHom (hS.extClass.postcomp X h))
(AddCommGrpCat.ofHom ((mk₀ S.f).postcomp X (add_zero n₁)))
(AddCommGrpCat.ofHom ((mk₀ S.g).postcomp X (add_zero n₁)))
