The dual numbers: Ext-finite but not Ext-bounded

Let k be a field, let A = k[ε] be the dual numbers k[ε]/(ε²), and let S = A/(ε) be the residue field of A, viewed as an A-module. Every Ext group of the pair (S, S) is a one-dimensional k-vector space (TauCeti.extDualNumberResidueEquiv), so TauCeti.IsExtFinite holds while none of the groups vanishes and TauCeti.IsExtBounded fails: the alternating sum ∑ n, (-1)ⁿ dim_k Extⁿ(S, S) is not a finite sum. This is the example that separates the two halves of TauCeti.IsEulerAdmissible. Since TauCeti.extEuler takes a proof of TauCeti.IsEulerAdmissible as an argument, it cannot be instantiated for this pair and exposes no totalised fallback value.

Main results

• TauCeti.not_isExtBounded_dualNumberResidue: no degree bounds the Ext-support of (S, S). This half needs only a nontrivial commutative ring of coefficients.
• TauCeti.isExtFinite_dualNumberResidue: every Extⁿ(S, S) is a finite-dimensional k-vector space.
• TauCeti.not_isEulerAdmissible_dualNumberResidue: the pair (S, S) is not Euler-admissible.

References

• Charles A. Weibel, An Introduction to Homological Algebra, Cambridge Studies in Advanced Mathematics 38, Cambridge University Press (1994), Section 2.5 and Chapter 4.

theorem TauCeti.not_isExtBoundedBy_dualNumberResidue (k : Type u) [CommRing k] [Nontrivial k] (N : ℕ) : ¬IsExtBoundedBy (dualNumberResidue k) (dualNumberResidue k) N

No degree is a vanishing bound for the Ext groups of k[ε]/(ε) against itself, because none of them vanishes.

theorem TauCeti.not_isExtBounded_dualNumberResidue (k : Type u) [CommRing k] [Nontrivial k] : ¬IsExtBounded (dualNumberResidue k) (dualNumberResidue k)

The dual-numbers rejection. Extⁿ(S, S) never vanishes, so the pair (S, S) is not Ext-bounded.

theorem TauCeti.isExtFinite_dualNumberResidue (k : Type u) [Field k] : IsExtFinite k (dualNumberResidue k) (dualNumberResidue k)

Every Ext group of k[ε]/(ε) against itself is a finite-dimensional k-vector space.

theorem TauCeti.not_isEulerAdmissible_dualNumberResidue (k : Type u) [Field k] : ¬IsEulerAdmissible k (dualNumberResidue k) (dualNumberResidue k)

The dual-numbers rejection. The residue field S of k[ε] is not Euler-admissible against itself: its Ext groups are all one-dimensional, so Ext-finiteness holds (TauCeti.isExtFinite_dualNumberResidue), but none of them vanishes, so the alternating sum ∑ n, (-1)ⁿ dim_k Extⁿ(S, S) is not a finite sum. Because TauCeti.extEuler consumes a proof of TauCeti.IsEulerAdmissible, it cannot be instantiated for this pair and exposes no totalised fallback value.