Realizing Ext¹ by short exact sequences

Given a short exact sequence with projective middle term, every class in Ext¹ out of its final term is represented by a short exact sequence with the prescribed endpoints. The middle term is obtained by pushing out the given presentation.

A pair of maps on the endpoints of two short exact sequences extends to a map of sequences exactly when it respects their extension classes. In particular, equal extension classes give isomorphic sequences with the identity on both endpoints.

This uses TauCeti.homBoundary_surjective to express a class as a boundary, and ShortComplex.ShortExact.extClass_naturality to identify the pushout class. In particular, the result can turn extension classes with annihilation properties into sequences with lifting properties.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Section 3.4.

theorem CategoryTheory.ShortComplex.ShortExact.exists_extClass_eq {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S : ShortComplex C} (hS : S.ShortExact) [Projective S.X₂] (Y : C) (α : Abelian.Ext S.X₃ Y 1) : ∃ (E : C) (i : Y ⟶ E) (p : E ⟶ S.X₃) (h : CategoryStruct.comp i p = 0) (hT : { X₁ := Y, X₂ := E, X₃ := S.X₃, f := i, g := p, zero := h }.ShortExact), hT.extClass = α

Every degree-one extension class out of the last term of a projective presentation has a short exact representative with exactly the specified endpoints.

theorem CategoryTheory.ShortComplex.ShortExact.exists_hom_iff_extClass_comp_eq {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S T : ShortComplex C} (hS : S.ShortExact) (hT : T.ShortExact) (a : S.X₁ ⟶ T.X₁) (c : S.X₃ ⟶ T.X₃) : (∃ (φ : S ⟶ T), φ.τ₁ = a ∧ φ.τ₃ = c) ↔ hS.extClass.comp (Abelian.Ext.mk₀ a) ⋯ = (Abelian.Ext.mk₀ c).comp hT.extClass ⋯

Maps on the endpoints extend to a morphism of short exact sequences if and only if they respect the associated degree-one extension classes.

theorem CategoryTheory.ShortComplex.ShortExact.exists_iso_iff_extClass_comp_eq {C : Type u} [Category.{v, u} C] [Abelian C] [HasExt C] {S T : ShortComplex C} (hS : S.ShortExact) (hT : T.ShortExact) (a : S.X₁ ≅ T.X₁) (c : S.X₃ ≅ T.X₃) : (∃ (e : S ≅ T), e.hom.τ₁ = a.hom ∧ e.hom.τ₃ = c.hom) ↔ hS.extClass.comp (Abelian.Ext.mk₀ a.hom) ⋯ = (Abelian.Ext.mk₀ c.hom).comp hT.extClass ⋯

Isomorphisms on the endpoints extend to an isomorphism of short exact sequences if and only if they respect the associated degree-one extension classes.