Infinite Source Augmentation Ideal

Abstract

The augmentation ideal of the infinite coordinatewise square-zero source algebra is not finitely generated.

Theorem 1.1 (No finite family generates every source coordinate).

$$\begin{array}{c}(\forall s:\mathrm{Finset}(InfiniteSourceAlgebra),s\subseteq augmentationIdeal\Rightarrow \exists h:\mathbb{Z},\neg \mathrm{sourceVariable}(h)\in \mathrm{IdealSpan}(s))\wedge \\ \neg \mathrm{FG}(augmentationIdeal)\wedge \\ \neg \mathrm{IsNoetherianRing}(InfiniteSourceAlgebra).\end{array}$$

Proof. Machine-checked in Lean as D5/S3/Observer/InfiniteSourceAugmentationIdeal.infinite_source_augmentation_ideal_not_finitely_generated (✓ std3). ∎

Source. Repository-derived.

Commentary.

The carrier is the complex multivariable polynomial ring indexed by the integers, quotiented by the ideal generated by the square of each coordinate. The augmentation ideal is generated by the images of all coordinate variables.

Choose polynomial representatives for a proposed finite family and then an integer outside the union of their finite variable sets. Evaluation at that coordinate descends to the dual numbers: it kills every proposed generator but sends the fresh coordinate to the nonzero dual unit.

This proves the finite-family escape clause, which rules out finite generation. The pinned characterization of Noetherian rings by finite generation of all ideals then gives the final clause.

Repository, pinned-Mathlib, and public Lean ecosystem searches found no exact owner for this infinite-index quotient theorem.

References

• Truth anchor: D5/S3/Observer/InfiniteSourceAugmentationIdeal.infinite_source_augmentation_ideal_not_finitely_generated