Euler-admissible pairs and the Ext-Euler characteristic

Let C be a k-linear abelian category with Ext groups. The Ext-Euler characteristic of a pair of objects is the alternating sum

χ(X, Y) = ∑ n, (-1)ⁿ dim_k Extⁿ(X, Y).

This is a number only under two genuinely separate finiteness hypotheses: every Extⁿ(X, Y) must be a finite-dimensional k-vector space, and Extⁿ(X, Y) must vanish for all large n. Neither implies the other — over the dual numbers k[ε]/(ε²) the simple module S has Extⁿ(S, S) ≅ k for every n, so the first holds and the second fails, while an infinite-dimensional vector space is Ext-bounded but not Ext-finite against itself — and a definition that totalizes the sum would return a junk value in exactly the first situation. This file therefore keeps the two conditions apart, as IsExtFinite and IsExtBounded, packages them as IsEulerAdmissible, and defines the Euler characteristic only from a witness of both.

The value is defined by truncating the sum to the degrees below an explicit bound (truncatedExtEuler); the whole content of extEuler_eq is that every bound beyond which the Ext groups vanish gives the same answer.

Main definitions

• TauCeti.IsExtFinite: every Extⁿ(X, Y) is a finite-dimensional k-vector space.
• TauCeti.IsExtBoundedBy and TauCeti.IsExtBounded: Extⁿ(X, Y) vanishes for n at least a given bound, resp. for all large n.
• TauCeti.IsEulerAdmissible: the conjunction of the two, the hypothesis under which the Ext-Euler characteristic of the pair (X, Y) exists.
• TauCeti.IsExtBoundedOn and TauCeti.IsEulerAdmissibleOn: respectively, uniform boundedness and pointwise Euler-admissibility for a pair of object properties; the latter is the hypothesis Layer 5's descent to Grothendieck groups will consume.
• TauCeti.truncatedExtEuler and TauCeti.extEuler: the truncated alternating sum, and the Ext-Euler characteristic of an Euler-admissible pair.

Main results

• TauCeti.extEuler_eq: the Ext-Euler characteristic is the alternating sum truncated at any bound beyond which the Ext groups vanish.
• TauCeti.IsEulerAdmissible.congr and TauCeti.extEuler_congr: degreewise linear equivalences of Ext preserve the hypothesis and the value.
• TauCeti.IsEulerAdmissible.of_iso and TauCeti.extEuler_of_iso: isomorphism invariance of the hypothesis and of the value.
• TauCeti.IsEulerAdmissible.of_shortExact₂ and TauCeti.IsEulerAdmissible.of_shortExact₂': Euler-admissibility is closed under extensions in either variable, and TauCeti.IsEulerAdmissible.biprod, TauCeti.IsEulerAdmissible.biprod' under binary direct sums; the empty direct sum is covered by TauCeti.IsEulerAdmissible.of_isZero_left and TauCeti.IsEulerAdmissible.of_isZero_right.
• TauCeti.IsExtFinite.of_shortExact₃': Ext-finiteness also passes from the subobject and the middle object of a short exact sequence to its quotient, in the first variable.
• TauCeti.IsExtFinite.finiteDimensional_hom: Hom-finiteness is the degree-zero consequence of Ext-finiteness, and is kept as a separate predicate.
• TauCeti.extEuler_projective: projective evaluation, χ(P, Y) = dim_k Hom(P, Y).

The remaining Layer 5 targets — the long exact sequences cut off by the vanishing bound, the resulting additivity of χ in both variables, and the descent of χ to a biadditive pairing on Grothendieck groups — are not proved here; this file supplies the finiteness interface they are stated over.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Sections 2.4--2.7 and Chapter 4, for Ext, its long exact sequences, and projective dimension.
• Ibrahim Assem, Daniel Simson, and Andrzej Skowroński, Elements of the Representation Theory of Associative Algebras, Volume 1, LMS Student Texts 65, Cambridge University Press (2006), Chapter III, Section 3, Proposition 3.13, for the Euler form of an algebra of finite global dimension.
• The Tau Ceti Grothendieck groups, Cartan maps, and Euler forms roadmap, Layer 5, whose "Ext-finite pairs" bullet and the first half of its "Ext-Euler value" bullet are the targets proved here.

The two finiteness conditions

structure TauCeti.IsExtFinite {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X Y : C) : Prop

Every Extⁿ(X, Y) is a finite-dimensional k-vector space. This is one of the two independent halves of TauCeti.IsEulerAdmissible; on its own it does not make the alternating sum of the dimensions a finite sum.

• finiteDimensional (n : ℕ) : FiniteDimensional k (CategoryTheory.Abelian.Ext X Y n)

  Each Ext group of the pair is finite-dimensional.

structure TauCeti.IsExtBoundedBy {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X Y : C) (N : ℕ) : Prop

Extⁿ(X, Y) vanishes in every degree n ≥ N.

• subsingleton ⦃n : ℕ⦄ (hn : N ≤ n) : Subsingleton (CategoryTheory.Abelian.Ext X Y n)

  The Ext groups of the pair vanish from degree N on.

structure TauCeti.IsExtBounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (X Y : C) : Prop

Extⁿ(X, Y) vanishes for all large n. This is the other half of TauCeti.IsEulerAdmissible, and the one that makes the Ext-Euler characteristic a finite sum.

• exists_bound : ∃ (N : ℕ), IsExtBoundedBy X Y N

  Some degree bounds the Ext-support of the pair.

structure TauCeti.IsEulerAdmissible {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X Y : C) : Prop

A pair (X, Y) is Euler-admissible when all of its Ext groups are finite-dimensional and all but finitely many of them vanish. This is exactly the hypothesis under which the alternating sum ∑ n, (-1)ⁿ dim_k Extⁿ(X, Y) is a well-defined integer.

• isExtFinite : IsExtFinite k X Y

  All Ext groups of the pair are finite-dimensional.

• isExtBounded : IsExtBounded X Y

  All but finitely many Ext groups of the pair vanish.

Elementary consequences and monotonicity

theorem TauCeti.IsExtBoundedBy.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X Y : C} {N M : ℕ} (h : IsExtBoundedBy X Y N) (hNM : N ≤ M) : IsExtBoundedBy X Y M

A vanishing bound may always be raised.

theorem TauCeti.IsExtBoundedBy.isExtBounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X Y : C} {N : ℕ} (h : IsExtBoundedBy X Y N) : IsExtBounded X Y

An explicit vanishing bound witnesses eventual Ext-vanishing.

theorem TauCeti.IsExtFinite.finiteDimensional_hom {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (h : IsExtFinite k X Y) : FiniteDimensional k (X ⟶ Y)

Hom-finiteness is the degree-zero part of Ext-finiteness, and is kept as a separate, weaker predicate: it says nothing about the higher Ext groups.

Versions for a pair of object properties

structure TauCeti.IsExtBoundedOn {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (P Q : CategoryTheory.ObjectProperty C) (N : ℕ) : Prop

A uniform Ext-vanishing bound for a pair of object properties: Extⁿ(X, Y) = 0 in every degree n ≥ N, for all X satisfying P and all Y satisfying Q. For a category of modules over a k-algebra of finite global dimension this is the bound supplied by that dimension, and it is a strictly stronger hypothesis than pointwise Ext-boundedness.

• isExtBoundedBy ⦃X Y : C⦄ (hX : P X) (hY : Q Y) : IsExtBoundedBy X Y N

  The bound N works for every pair of objects drawn from P and Q.

structure TauCeti.IsEulerAdmissibleOn {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (P Q : CategoryTheory.ObjectProperty C) : Prop

Every pair of objects drawn from P and Q is Euler-admissible, with a bound that may depend on the pair. This is the hypothesis under which the Ext-Euler characteristic descends to a pairing between the Grothendieck groups of the two subcategories. A shared bound is the separate, stronger predicate TauCeti.IsExtBoundedOn.

• isEulerAdmissible ⦃X Y : C⦄ (hX : P X) (hY : Q Y) : IsEulerAdmissible k X Y

  Each pair of objects drawn from P and Q is Euler-admissible.

theorem TauCeti.IsExtBoundedOn.isExtBounded {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} {N : ℕ} (h : IsExtBoundedOn P Q N) {X Y : C} (hX : P X) (hY : Q Y) : IsExtBounded X Y

A uniform bound is in particular a pointwise one.

theorem TauCeti.IsExtBoundedOn.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P P' Q Q' : CategoryTheory.ObjectProperty C} {N M : ℕ} (h : IsExtBoundedOn P Q N) (hP : P' ≤ P) (hQ : Q' ≤ Q) (hNM : N ≤ M) : IsExtBoundedOn P' Q' M

A uniform vanishing bound passes to smaller object properties and may always be raised, in particular it restricts to full subcategories of the ones considered.

theorem TauCeti.IsEulerAdmissibleOn.mono {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P P' Q Q' : CategoryTheory.ObjectProperty C} (h : IsEulerAdmissibleOn k P Q) (hP : P' ≤ P) (hQ : Q' ≤ Q) : IsEulerAdmissibleOn k P' Q'

Euler-admissibility on a pair of object properties passes to smaller properties, in particular to full subcategories of the ones considered.

theorem TauCeti.IsExtBoundedOn.isEulerAdmissibleOn {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} {N : ℕ} (h : IsExtBoundedOn P Q N) (hfin : ∀ ⦃X Y : C⦄, P X → Q Y → IsExtFinite k X Y) : IsEulerAdmissibleOn k P Q

A uniform bound and pointwise Ext-finiteness give Euler-admissibility on the pair.

The Ext-Euler characteristic

noncomputable def TauCeti.truncatedExtEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X Y : C) (N : ℕ) : ℤ

The raw alternating sum ∑_{n < N} (-1)ⁿ * Module.finrank k Extⁿ(X, Y) over the cohomological degrees below N. This definition takes no admissibility witness: a summand is the dimension of the corresponding Ext group only where that group is finite-dimensional, Module.finrank returning its 0 fallback elsewhere. Truncating at an explicit bound is what keeps the sum finite; TauCeti.extEuler is the version that supplies both a TauCeti.IsExtFinite witness, making every summand a genuine dimension, and a vanishing bound for N.

Equations

• TauCeti.truncatedExtEuler k X Y N = ∑ n ∈ Finset.range N, (-1) ^ n * ↑(Module.finrank k (CategoryTheory.Abelian.Ext X Y n))

@[simp]

theorem TauCeti.truncatedExtEuler_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X Y : C) : truncatedExtEuler k X Y 0 = 0

The empty truncation of the alternating sum is zero.

theorem TauCeti.truncatedExtEuler_succ {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (X Y : C) (N : ℕ) : truncatedExtEuler k X Y (N + 1) = truncatedExtEuler k X Y N + (-1) ^ N * ↑(Module.finrank k (CategoryTheory.Abelian.Ext X Y N))

Raising the truncation bound by one adds the signed dimension of the next Ext group.

theorem TauCeti.truncatedExtEuler_eq_of_le {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} {N M : ℕ} (h : IsExtBoundedBy X Y N) (hNM : N ≤ M) : truncatedExtEuler k X Y M = truncatedExtEuler k X Y N

Raising the truncation bound past a degree from which the Ext groups vanish does not change the alternating sum.

noncomputable def TauCeti.extEuler {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (h : IsEulerAdmissible k X Y) : ℤ

The Ext-Euler characteristic χ(X, Y) = ∑ n, (-1)ⁿ dim_k Extⁿ(X, Y) of an Euler-admissible pair. The choice of vanishing bound made here is removed at once by TauCeti.extEuler_eq, so no result depends on it.

Equations

• TauCeti.extEuler k h = TauCeti.truncatedExtEuler k X Y ⋯.choose

theorem TauCeti.extEuler_eq {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (h : IsEulerAdmissible k X Y) {N : ℕ} (hN : IsExtBoundedBy X Y N) : extEuler k h = truncatedExtEuler k X Y N

Every degree from which the Ext groups of the pair vanish computes its Ext-Euler characteristic.

theorem TauCeti.extEuler_eq_zero_of_isExtBoundedBy_zero {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (h : IsEulerAdmissible k X Y) (h₀ : IsExtBoundedBy X Y 0) : extEuler k h = 0

The Ext-Euler characteristic of a pair with no Ext at all is zero.

Invariance under linear equivalences and isomorphisms

theorem TauCeti.IsExtFinite.congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.Linear k D] [CategoryTheory.HasExt D] {X Y : C} {X' Y' : D} (h : IsExtFinite k X Y) (e : (n : ℕ) → CategoryTheory.Abelian.Ext X Y n ≃ₗ[k] CategoryTheory.Abelian.Ext X' Y' n) : IsExtFinite k X' Y'

Ext-finiteness transports along degreewise linear equivalences of Ext groups, including between pairs in different categories.

theorem TauCeti.IsExtBoundedBy.congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt D] {X Y : C} {X' Y' : D} {N : ℕ} (h : IsExtBoundedBy X Y N) (e : ⦃n : ℕ⦄ → N ≤ n → CategoryTheory.Abelian.Ext X Y n ≃ CategoryTheory.Abelian.Ext X' Y' n) : IsExtBoundedBy X' Y' N

A vanishing bound transports along bijections of the Ext groups from that degree on, including between pairs in different categories.

theorem TauCeti.IsExtBounded.congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.HasExt D] {X Y : C} {X' Y' : D} (h : IsExtBounded X Y) (e : ∀ᶠ (n : ℕ) in Filter.atTop, Nonempty (CategoryTheory.Abelian.Ext X Y n ≃ CategoryTheory.Abelian.Ext X' Y' n)) : IsExtBounded X' Y'

Eventual Ext-vanishing transports along bijections of Ext groups in all large degrees, including between pairs in different categories.

theorem TauCeti.IsEulerAdmissible.congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.Linear k D] [CategoryTheory.HasExt D] {X Y : C} {X' Y' : D} (h : IsEulerAdmissible k X Y) (e : (n : ℕ) → CategoryTheory.Abelian.Ext X Y n ≃ₗ[k] CategoryTheory.Abelian.Ext X' Y' n) : IsEulerAdmissible k X' Y'

Euler-admissibility transports along degreewise linear equivalences of Ext groups, including between pairs in different categories.

theorem TauCeti.extEuler_congr {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {D : Type u'} [CategoryTheory.Category.{v', u'} D] [CategoryTheory.Abelian D] [CategoryTheory.Linear k D] [CategoryTheory.HasExt D] {X Y : C} {X' Y' : D} (e : (n : ℕ) → CategoryTheory.Abelian.Ext X Y n ≃ₗ[k] CategoryTheory.Abelian.Ext X' Y' n) (h : IsEulerAdmissible k X Y) : extEuler k ⋯ = extEuler k h

Degreewise linear equivalences of Ext groups preserve the Ext-Euler characteristic, including when the pairs lie in different categories.

theorem TauCeti.IsExtFinite.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (h : IsExtFinite k X Y) (e : X ≅ X') (f : Y ≅ Y') : IsExtFinite k X' Y'

Ext-finiteness only depends on the isomorphism classes of the two objects.

theorem TauCeti.IsExtBoundedBy.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} {N : ℕ} (h : IsExtBoundedBy X Y N) (e : X ≅ X') (f : Y ≅ Y') : IsExtBoundedBy X' Y' N

A vanishing bound transports along isomorphisms of the two objects.

theorem TauCeti.IsExtBounded.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (h : IsExtBounded X Y) (e : X ≅ X') (f : Y ≅ Y') : IsExtBounded X' Y'

Eventual Ext-vanishing only depends on the isomorphism classes of the two objects.

theorem TauCeti.IsEulerAdmissible.of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (h : IsEulerAdmissible k X Y) (e : X ≅ X') (f : Y ≅ Y') : IsEulerAdmissible k X' Y'

Euler-admissibility only depends on the isomorphism classes of the two objects.

theorem TauCeti.extEuler_of_iso {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X X' Y Y' : C} (h : IsEulerAdmissible k X Y) (h' : IsEulerAdmissible k X' Y') (e : X ≅ X') (f : Y ≅ Y') : extEuler k h = extEuler k h'

The Ext-Euler characteristic only depends on the isomorphism classes of the two objects.

Closure under extensions and finite direct sums

theorem TauCeti.IsExtFinite.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] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X : C} (h₁ : IsExtFinite k X S.X₁) (h₃ : IsExtFinite k X S.X₃) : IsExtFinite k X S.X₂

Extension closure in the second variable for Ext-finiteness.

theorem TauCeti.IsExtFinite.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] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} (h₁ : IsExtFinite k S.X₁ Y) (h₃ : IsExtFinite k S.X₃ Y) : IsExtFinite k S.X₂ Y

Extension closure in the first variable for Ext-finiteness.

theorem TauCeti.IsExtFinite.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] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} (h₁ : IsExtFinite k S.X₁ Y) (h₂ : IsExtFinite k S.X₂ Y) : IsExtFinite k S.X₃ Y

Ext-finiteness passes to the quotient term of a short exact sequence, along the first variable: the long exact sequence exhibits Extⁿ⁺¹(S.X₃, Y) between Extⁿ(S.X₁, Y) and Extⁿ⁺¹(S.X₂, Y), and its degree-zero group is a subspace of Hom(S.X₂, Y).

theorem TauCeti.IsExtBoundedBy.of_shortExact₂ {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₁ : IsExtBoundedBy X S.X₁ N₁) (h₃ : IsExtBoundedBy X S.X₃ N₃) : IsExtBoundedBy X S.X₂ (max N₁ N₃)

Extension closure in the second variable for eventual Ext-vanishing: the middle term of a short exact sequence inherits the larger of the two outer bounds.

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

Extension closure in the first variable for eventual Ext-vanishing.

theorem TauCeti.IsEulerAdmissible.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] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {X : C} (h₁ : IsEulerAdmissible k X S.X₁) (h₃ : IsEulerAdmissible k X S.X₃) : IsEulerAdmissible k X S.X₂

Euler-admissibility is closed under extensions in the second variable.

theorem TauCeti.IsEulerAdmissible.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] {S : CategoryTheory.ShortComplex C} (hS : S.ShortExact) {Y : C} (h₁ : IsEulerAdmissible k S.X₁ Y) (h₃ : IsEulerAdmissible k S.X₃ Y) : IsEulerAdmissible k S.X₂ Y

Euler-admissibility is closed under extensions in the first variable.

theorem TauCeti.IsEulerAdmissible.biprod {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y₁ Y₂ : C} (h₁ : IsEulerAdmissible k X Y₁) (h₂ : IsEulerAdmissible k X Y₂) : IsEulerAdmissible k X (Y₁ ⊞ Y₂)

Euler-admissibility is closed under binary direct sums in the second variable, because Y₁ ⟶ Y₁ ⊞ Y₂ ⟶ Y₂ is short exact.

theorem TauCeti.IsEulerAdmissible.biprod' {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] {k : Type t} [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X₁ X₂ Y : C} (h₁ : IsEulerAdmissible k X₁ Y) (h₂ : IsEulerAdmissible k X₂ Y) : IsEulerAdmissible k (X₁ ⊞ X₂) Y

Euler-admissibility is closed under binary direct sums in the first variable.

theorem TauCeti.IsEulerAdmissible.of_isZero_left {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (hX : CategoryTheory.Limits.IsZero X) : IsEulerAdmissible k X Y

A zero object is Euler-admissible against every object: all of its Ext groups vanish. This is the empty case of TauCeti.IsEulerAdmissible.biprod', the direct sum of no objects being a zero object.

theorem TauCeti.IsEulerAdmissible.of_isZero_right {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {X Y : C} (hY : CategoryTheory.Limits.IsZero Y) : IsEulerAdmissible k X Y

Every object is Euler-admissible against a zero object. This is the empty case of TauCeti.IsEulerAdmissible.biprod.

Projective evaluation

theorem TauCeti.isExtBoundedBy_one_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] (P Y : C) [CategoryTheory.Projective P] : IsExtBoundedBy P Y 1

All Ext groups of positive degree out of a projective object vanish, so a pair with projective first entry is Ext-bounded by 1.

theorem TauCeti.isExtBoundedOn_one_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] [CategoryTheory.HasExt C] {P : CategoryTheory.ObjectProperty C} (hP : ∀ (X : C), P X → CategoryTheory.Projective X) (Q : CategoryTheory.ObjectProperty C) : IsExtBoundedOn P Q 1

If every object satisfying P is projective, then 1 is a uniform Ext-vanishing bound for P against an arbitrary Q. This is the degenerate case of a uniform global-dimension bound, and the one Layer 4's Cartan comparison uses on the subcategory of projectives.

theorem TauCeti.isExtFinite_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (P Y : C) [CategoryTheory.Projective P] [FiniteDimensional k (P ⟶ Y)] : IsExtFinite k P Y

A Hom-finite pair with projective first entry is Ext-finite: apart from the degree-zero group, which is the Hom space, all of its Ext groups vanish.

theorem TauCeti.isEulerAdmissible_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] (P Y : C) [CategoryTheory.Projective P] [FiniteDimensional k (P ⟶ Y)] : IsEulerAdmissible k P Y

A Hom-finite pair with projective first entry is Euler-admissible.

theorem TauCeti.extEuler_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Y : C} [CategoryTheory.Projective P] (h : IsEulerAdmissible k P Y) : extEuler k h = ↑(Module.finrank k (P ⟶ Y))

Projective evaluation: the Ext-Euler characteristic of a pair with projective first entry is the dimension of its Hom space, χ(P, Y) = dim_k Hom(P, Y).

theorem TauCeti.isEulerAdmissibleOn_of_projective {C : Type u} [CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C] (k : Type t) [Field k] [CategoryTheory.Linear k C] [CategoryTheory.HasExt C] {P Q : CategoryTheory.ObjectProperty C} (hP : ∀ (X : C), P X → CategoryTheory.Projective X) (hHom : ∀ ⦃X Y : C⦄, P X → Q Y → FiniteDimensional k (X ⟶ Y)) : IsEulerAdmissibleOn k P Q

Hom-finite projectives are Euler-admissible against every object satisfying Q: this is the concrete source of Euler-admissibility on the projective side, and it is what makes TauCeti.IsEulerAdmissibleOn a nonempty hypothesis.