Graded Ext finiteness for quotients

In a short exact sequence 0 ⟶ X₁ ⟶ X₂ ⟶ X₃ ⟶ 0, finite internal support of Ext(X₁,Y) and Ext(X₂,Y) implies finite internal support of Ext(X₃,Y). The long exact Ext sequence also bounds the cohomological support of X₃ one degree after the bound for X₁. This makes a finite projective presentation usable for graded Euler characteristics.

The argument uses the contravariant long exact Ext sequence of Mathlib, via the linear maps in TauCeti.Algebra.Homology.Ext.Basic.

theorem TauCeti.IsGradedExtInternallyFinite.of_shortExact₃' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {S : CategoryTheory.ShortComplex C} {Y : C} (hS : S.ShortExact) (h₁ : IsGradedExtInternallyFinite k e S.X₁ Y) (h₂ : IsGradedExtInternallyFinite k e S.X₂ Y) : IsGradedExtInternallyFinite k e S.X₃ Y

Finite internal support of graded Ext passes to the quotient term of a short exact sequence in the first variable.

theorem TauCeti.IsGradedExtBoundedBy.of_shortExact₃' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {e : C ≌ C} {S : CategoryTheory.ShortComplex C} {Y : C} (hS : S.ShortExact) {N₁ N₂ : ℕ} (h₁ : IsGradedExtBoundedBy e S.X₁ Y N₁) (h₂ : IsGradedExtBoundedBy e S.X₂ Y N₂) : IsGradedExtBoundedBy e S.X₃ Y (max (N₁ + 1) N₂)

If graded Ext from the subobject vanishes from degree N₁ and from the middle object from degree N₂, then graded Ext from the quotient vanishes from max (N₁ + 1) N₂.

theorem TauCeti.IsGradedEulerAdmissible.of_shortExact₃' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {e : C ≌ C} {S : CategoryTheory.ShortComplex C} {Y : C} (hS : S.ShortExact) (h₁ : IsGradedEulerAdmissible k e S.X₁ Y) (h₂ : IsGradedEulerAdmissible k e S.X₂ Y) : IsGradedEulerAdmissible k e S.X₃ Y

Graded Euler admissibility passes from the subobject and the middle object to the quotient of a short exact sequence.