noncomputable def ExtClassifiesExtensions.splitting_of_ext1_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (hExt : ∀ (e : CategoryTheory.Abelian.Ext S.X₃ S.X₁ 1), e = 0) : S.Splitting

Splitting criterion: a short exact sequence 0 → X₁ → X₂ → X₃ → 0 splits when Ext¹(X₃, X₁) = 0, recovering the classification of extensions by Ext¹.

noncomputable def ExtClassifiesExtensions.covariantConnecting {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) (X : C) {n₀ n₁ : ℕ} (h : n₀ + 1 = n₁) : CategoryTheory.Abelian.Ext X S.X₃ n₀ →+ CategoryTheory.Abelian.Ext X S.X₁ n₁

The covariant connecting homomorphism Ext^{n₀}(X, X₃) → Ext^{n₁}(X, X₁) associated to a short exact sequence, given by post-composition with the extension class.