Realization of degree-one Ext classes

In an abelian category with enough projectives, every degree-one Ext class is represented by a short exact sequence. The construction pushes the kernel of a projective presentation out along a degree-zero representative supplied by the long exact Ext sequence.

noncomputable def MagnitudeConjecture.ExtOneRealization.PushoutExtension.projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) : CategoryTheory.Limits.pushout (CategoryTheory.Limits.kernel.ι p) f ⟶ X

The map from the pushout middle object to the presented endpoint.

@[simp]

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.inl_projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.kernel.ι p) f) (projection p f) = p

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.inl_projection_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inl (CategoryTheory.Limits.kernel.ι p) f) (CategoryTheory.CategoryStruct.comp (projection p f) h) = CategoryTheory.CategoryStruct.comp p h

@[simp]

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.inr_projection {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.kernel.ι p) f) (projection p f) = 0

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.inr_projection_assoc {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) {Z : D} (h : X ⟶ Z) : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.kernel.ι p) f) (CategoryTheory.CategoryStruct.comp (projection p f) h) = CategoryTheory.CategoryStruct.comp 0 h

noncomputable def MagnitudeConjecture.ExtOneRealization.PushoutExtension.shortComplex {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) : CategoryTheory.ShortComplex D

The pushout short complex.

instance MagnitudeConjecture.ExtOneRealization.PushoutExtension.projection_epi {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) [CategoryTheory.Epi p] : CategoryTheory.Epi (projection p f)

noncomputable def MagnitudeConjecture.ExtOneRealization.PushoutExtension.projectionIsCokernel {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) [CategoryTheory.Epi p] : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ (projection p f) ⋯)

The pushout projection is a cokernel of the pushed kernel inclusion.

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.shortExact {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) [CategoryTheory.Epi p] : (shortComplex p f).ShortExact

The pushout complex is short exact.

noncomputable def MagnitudeConjecture.ExtOneRealization.PushoutExtension.fromPresentation {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) : { X₁ := CategoryTheory.Limits.kernel p, X₂ := P, X₃ := X, f := CategoryTheory.Limits.kernel.ι p, g := p, zero := ⋯ } ⟶ shortComplex p f

The comparison from the kernel presentation to its pushout.

theorem MagnitudeConjecture.ExtOneRealization.PushoutExtension.extClass_eq_precomp {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] {P X T : D} (p : P ⟶ X) (f : CategoryTheory.Limits.kernel p ⟶ T) [CategoryTheory.Epi p] [CategoryTheory.HasExt D] : ⋯.extClass = ⋯.extClass.comp (CategoryTheory.Abelian.Ext.mk₀ f) ⋯

The pushout realizes the connecting image of f.

theorem MagnitudeConjecture.ExtOneRealization.exists_shortExact_with_extClass_eq {D : Type u} [CategoryTheory.Category.{v, u} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt D] [CategoryTheory.EnoughProjectives D] (X T : D) (xi : CategoryTheory.Abelian.Ext X T 1) : ∃ (E : D) (i : T ⟶ E) (q : E ⟶ X) (zero : CategoryTheory.CategoryStruct.comp i q = 0) (hS : { X₁ := T, X₂ := E, X₃ := X, f := i, g := q, zero := zero }.ShortExact), hS.extClass = xi

Every degree-one Ext class in an abelian category with enough projectives has a short exact realization.