Skip to content

Group rings

Reusable Lean algebra equivalences from group algebras equipped with explicit free-abelian coordinates to multivariable Laurent polynomial algebras, with canonical FreeAbelianGroup specialization and forward/inverse basis and free-generator laws. Laurent monomials are finitely supported integer exponent vectors; no finite-variable or decidable-equality premise is added. Separately, field-valued finite-abelian characters give evaluation bases when enough roots exist; right convolution has positive-character eigenvalues, diagonalization and a Nat.card rank formula. Monoid-algebra augmentation sums coefficients over any semiring and monoid. For a right-cancellative monoid M, any nonzero R[M]-linear map from R with its left augmentation action into the left regular R[M] forces M finite. Such maps vanish for infinite M, including infinite groups, without coefficient commutativity, nontriviality or a domain condition. Over any ring, the augmentation kernel is the left ideal generated by single m 1 - 1. A monoid generating set, or a subgroup generating set for groups, suffices for these left-ideal generators. Generic difference-membership lemmas propagate through monoid and subgroup closure in any ring's left ideals. As a left coefficient-ring module it also has a basis indexed by nonidentity monoid elements, with those vectors and the original coefficients as coordinates. A generic pointed Finsupp sum-kernel equivalence underlies this basis. Single-term units over nontrivial semirings are exactly the terms whose coefficient and monoid index are both units. Coefficient-unit reflection holds over every semiring, including the trivial one. For an arbitrary subgroup of a group, its left ideal of basis differences consists of exactly the elements with zero coefficient sums on left cosets. Over a nontrivial ring these ideals reflect subgroup membership and inclusion, and two-sidedness is equivalent to subgroup normality. No group or coefficient commutativity or finiteness is needed. The coset map itself is semiring-general. Subgroup finite generation implies finite generation of its left group-ring ideal over any ring; over a nontrivial ring the converse holds. For the whole group this characterizes finite generation of the augmentation kernel. Left-Noetherian group algebras over nontrivial rings have every subgroup finitely generated. Surjective augmentation combines with the generic surjective-homomorphism Noetherianity theorem for coefficient descent over arbitrary semirings and monoids. For a finitely generated commutative monoid, its monoid algebra over any left-Noetherian ring is left-Noetherian, in independent universes and without coefficient commutativity. Augmentation gives the reverse implication; the exponent monoid need not be finite. For any monoid homomorphism over any ring, its monoid-algebra kernel is the left ideal spanned by all equal-image unit-basis differences. A finitely generated commutative source admits one finite pair family that works over every coefficient ring, without coefficient Noetherianity or target commutativity, finite generation or surjectivity. More generally, finite generation of the integer kernel is an explicit sufficient premise. For any injective homomorphism from a group to a monoid, left-Noetherianity of the monoid algebra descends to the group algebra over every semiring, with three independent universes. Every subgroup algebra is therefore left-Noetherian, without finite index or normality. The generic criterion uses an additive right retraction and ideal extension-contraction; no target cancellation or freeness is assumed. For any semiring and subgroup, right cosets index a basis of the group algebra as a left subgroup-algebra module, with explicit coefficient, reconstruction and scalar compatibility laws. Finite index makes this module finite over any semiring. For ring coefficients, finite-index subgroup algebras and group algebras are left-Noetherian simultaneously. Over every ring, the infinite cyclic group algebra is left-Noetherian iff its coefficient ring is. Group equivalences and finite-index infinite cyclic subgroups transport this criterion, including finite-group products. Every left ideal of an arbitrary semiring extends along monoid-algebra constants to exactly the elements whose coefficients lie in that ideal. Coefficient-change kernels are therefore extended coefficient kernels. Their powers vanish at exactly the same exponents as the coefficient kernel, including degree zero, for arbitrary semiring homomorphisms and monoids. With ring source and semiring target coefficients, surjectivity identifies the quotient with the target monoid algebra; otherwise it is the range subsemiring. Polynomial transport preserves constants, every coefficient, ideal extension and coefficient-change kernels. For a group-to-monoid map, simultaneous coefficient/index change over a ring source has kernel the sum of the subgroup-relation ideal and the extended coefficient kernel. Surjective coefficients give the algebra of the index range; if the index map is also surjective the full target is available. No nontriviality or commutativity is imposed, and the target coefficients need only be a semiring. No sufficient-condition converse for arbitrary groups is asserted. Over a nontrivial possibly noncommutative ring with prime p equal to zero, nilpotence of the augmentation kernel implies one common p-power exponent for an arbitrary group, hence IsPGroup p G, without finiteness. Uniform vanishing of mixed ordered products gives the same conclusion. A generic left-ideal power API over any semiring identifies zero powers with vanishing of every ordered product of that length, including degree zero. For finite p-groups over any ring with p=0, including the zero ring, the augmentation kernel has zero Nat.card G-th power. Every ordered mixed product of that length therefore vanishes. Over nontrivial rings, finite-group augmentation nilpotence is equivalent to IsPGroup p G. The proof uses central subgroups of order p, canonical cyclic quotient kernels, ideal extension bounds and multiplication of power degrees. For locally finite p-groups over any ring with prime p=0, each augmentation-zero element is nilpotent, with an element-dependent exponent. Under these same hypotheses, the Jacobson radical is the augmentation preimage of the coefficient radical. Radical membership is detected by augmentation, and a basis term is radical exactly when its coefficient is. If the coefficient radical is zero, the group-algebra radical equals the augmentation kernel. No uniform kernel exponent or vanishing kernel power is asserted; noncommutative and zero coefficient rings are allowed. Uniform nilpotence of an ordinary left-ideal action over any semiring yields a nonzero common annihilated vector in every nontrivial semimodule. Two-sided ideals have a canonical common-annihilator submodule, agreeing with commutative set torsion. For any ring and monoid, augmentation-kernel annihilation is equivalent to being fixed by every canonical monoid symbol. Every nontrivial unital module of a finite p-group algebra over a ring with prime p=0 therefore has a nonzero canonical fixed vector, without finite generation, finite dimension or finiteness of the module. Simple modules of these finite p-group algebras have trivial group action on every vector, hence augmentation action. Simplicity over the group algebra is equivalent to simplicity under canonical restriction along singleOneRingHom, including noncommutative and zero coefficient rings. The augmentation-action/trivial-monoid-action characterization is valid for semirings and semimodules. For any map of modules over a finite p-group algebra with prime p=0 in any ring, canonical fixed vectors detect injectivity and canonical augmentation coinvariants detect surjectivity, without finite generation or coupled module universes. The generic injection theorem concerns nilpotent two-sided ideals over semirings acting on additive groups; quotient surjectivity detection allows nilpotent left ideals over rings. Nilpotent Nakayama itself holds for arbitrary semimodules. For arbitrary rings S and A, any ring homomorphism phi, a given A-module V, and a two-sided ideal I with one power contained in the annihilator of V, surjectivity of the canonical S-to-A/I map implies separate Noetherian and Artinian equivalences and equality of composition lengths in ENat under exact restriction along phi. This includes nilpotent ideals, infinite length, noncentral scalar images and zero rings, without finite generation. For any ring R with prime p=0 and finite p-group G, these three invariants of every given R[G]-module agree with canonical coefficient restriction. For a finite group whose order is a unit in any semiring, projectivity under canonical coefficient restriction implies projectivity of the original group-algebra module. Noncommutative and zero semirings, additive commutative monoids and independent coefficient, group and module universes are allowed. Monoid algebras commute canonically with finite square matrix semirings, preserving every coefficient entry. The equivalence requires a semiring, a monoid and a finite decidable matrix index type in independent universes; empty indices and zero or noncommutative coefficients are allowed. Group-algebra centrality over any semiring is equivalent to central coefficients and conjugation invariance. A nonzero coefficient of a central element has a finite conjugation orbit, even when the group is infinite. At any one fixed group index, coefficients of all right products determine a group-algebra element; left-product tests independently do so. Either family detects zero, over any possibly zero or noncommutative semiring and any group, without finiteness. Identity evaluation is the index-one case, not augmentation. No group-algebra/convolution bridge is asserted.

Quoted from the project description in formalization.yaml of FormalFrontier/group-rings at commit 8e90e656, Apache-2.0.

1 article: 1 for headline results in its README whose declaration link names a declaration the scan finds in the linked file. Its other headline results are quoted where they stand.

Facts

From the repository and its formalization.yaml; the review and automation statements are quoted as written.

  • Repository: FormalFrontier/group-rings, read at commit 8e90e656 (2026-11-05).
  • Lean toolchain v4.34.0-rc2, Mathlib at 83abb3e7.
  • License: Apache-2.0.
  • Authors: Formal Frontier Agents.
  • Review status: “other”.
  • Review notes: “Agent mathematical review is revision-specific, not human review or source-author endorsement. Metadata and historical API signature hashes do not certify proofs, current native analysis, source coverage or rights.”
  • Automation: agent; framework “AI agents using Lean and Lake”; tool setup “Agents wrote and adapted proofs, interfaces, clients and documentation using Lean v4.34.0-rc2, Lake and mathlib 83abb3e776bdefcbc447a1e44d0debe4010039e5.”; prompting notes “Supplied coordinates, coefficient/universe hypotheses, basis laws, Fourier sign, augmentation coefficient laws, single-term unit criteria and boundary clients guide the reusable interfaces.”
  • Automation notes: “Code, proofs, documentation and metadata include AI-agent contributions; expression origins and contributor credit are recorded in CREDITS.md. No human mathematical review or source-author endorsement is claimed. AI generation does not establish correctness, originality, copyright ownership or redistribution clearance.”

Literature

The sources its formalization.yaml names, with their relationship to it.

Builds on

Used by

Headline results

Quoted from the headline results in README.md of FormalFrontier/group-rings at commit 8e90e656, Apache-2.0.

The families below summarize the library. The complete catalogue retains the detailed statements, qualifiers and source links; the usage guide provides the module and declaration inventories.

Single terms and augmentation. Over a nontrivial semiring and any monoid, IsUnit (single m r) ↔ IsUnit r ∧ IsUnit m; coefficient-unit reflection also allows the zero semiring. Over any semiring and an index type with only multiplication, a single term is left-regular iff its coefficient is left-regular and either the coefficients are subsingleton or its index is left-regular; the right-hand criterion is analogous. Augmentation is the coefficient-sum ring homomorphism over any semiring. For a right-cancellative monoid M, a nonzero R[M]-linear map from R with its left augmentation action into the left regular R[M] forces M finite; all such maps vanish when M is infinite, including infinite groups. No coefficient nontriviality or domain condition is needed. See the augmentation Hom theorems. Over a ring its kernel is the left span of single m 1 - 1, with monoid or subgroup generating-set refinements. MonoidAlgebra.augmentationKerBasis is a basis over the coefficient ring R, not over R[M], indexed by nonidentity monoid elements. Statements and modules. Over a nontrivial semiring and any group G, projectivity of R over R[G] for the canonical left augmentation action forces G to be finite and (Nat.card G : R) to be a unit; coefficients need not commute. See the augmentation-projectivity theorem.

Units with two unique products. Over a no-zero-divisor semiring R and a monoid M with TwoUniqueProds M, an arbitrary f : R[M] is a unit iff f = single m.val r.val for some m : Units M and r : Units R. Both kinds of units are multiplicative; R may be the zero semiring. For an additive monoid A with TwoUniqueSums A, the companion theorem uses a : AddUnits A; coefficient and algebra units remain multiplicative. See the unit theorem and precise scope and zero-semiring boundary.

TheoremConvolution support#

Over a no-zero-divisor semiring and a magma with two unique products, a product of input support cardinalities greater than one forces the convolution support cardinality to be greater than one. Coefficients need not commute, and no monoid or nontriviality assumption is imposed. See MonoidAlgebra.one_lt_card_support_coeff_mul and the precise support bound.

Quoted from the headline results in README.md of FormalFrontier/group-rings at commit 8e90e656, Apache-2.0.

Lean

Read from the source at commit 8e90e656, without running Lean.

Sources
LeanMonoidAlgebra.one_lt_card_support_coeff_mul

Coefficient tests, centers and finite matrices. Over any possibly zero or noncommutative semiring, a group-algebra element is determined by one chosen coefficient after all right multiplications, and independently after all left multiplications. Centrality means central coefficients invariant under conjugation; coefficients vanish on infinite conjugacy orbits. For any monoid, finite decidable matrix indices give the ring equivalence MonoidAlgebra (Matrix n n R) M ≃+* Matrix n n (R[M]), preserving both multiplication orders, including empty indices. Precise statements.

Crossed maps and averaging. Over any ring and monoid, linear maps from the full augmentation ideal to a given left R[M]-module correspond additively to normalized crossed maps z(mn) = z(m) + single m 1 • z(n) for its canonical action. For a finite group of unit order in the coefficient ring, every crossed map is principal, with negative inverse-order sum witness, natural for additive maps. See the universal property and averaging.

Augmentation cotangents. For any unital ring and monoid, coefficient-linear maps from I/I² to a left R-module V correspond as a set to M →* Multiplicative V. For a group, I/I² ≃ₗ[R] R ⊗[ℤ] Additive (Abelianization G), where I is the augmentation ideal and I² its ordinary ideal square. Coefficient covariance is semilinear; monoid products split by projections and sums of inclusions. No commutativity or freeness is required. Statements · cotangent guide.

Finite p-groups and fixed vectors. For prime p, any ring with (p : R) = 0 and finite p-group G, the augmentation ideal has zero Nat.card G-th power. Every nontrivial unital R[G]-module has a nonzero canonical fixed vector; simplicity is equivalent to simplicity under canonical coefficient restriction, and simple modules have trivial group action. For any group over any ring, augmentation nilpotence forces Subsingleton R ∨ Finite G, without a characteristic assumption. If (p : R) = 0, nilpotence is equivalent to Subsingleton R ∨ (Finite G ∧ IsPGroup p G); over nontrivial R it also forces one common p-power exponent. For locally finite p-groups over any ring with (p : R) = 0, every augmentation-zero element is nilpotent, with an element-dependent exponent; no uniform kernel power is asserted. Under these same locally finite hypotheses, the Jacobson radical is the augmentation preimage of the coefficient radical. In particular, a single term is radical exactly when its coefficient is, and a zero coefficient radical gives the augmentation kernel. See the radical guide and statements and guides.

Given modules and scalar restriction. Over any semiring and monoid, canonical representations and an additive Hom/intertwiner correspondence retain the given carriers and coefficient actions. For finite groups of unit order in the coefficient semiring, coefficient projectivity implies group-algebra projectivity. The normalized norm is natural for R[G]-linear maps and is the unique R[G]-linear retraction onto the fixed vectors' span. For rings S, A, a map φ : S →+* A surjective modulo a two-sided ideal I, and an A-module V with ∃ n, I^n ≤ Module.annihilator A V, the exact restriction Module.compHom V φ preserves and reflects both chain conditions and preserves length in ℕ∞, including infinity. Semisimplicity is equivalent to annihilation by I and semisimplicity of that restriction. For finite p-groups over rings with prime p = 0, this gives the canonical coefficient comparisons: semisimplicity requires coefficient semisimplicity and trivial group action. Fixed vectors detect injectivity of module maps; coinvariants detect surjectivity, without finite generation. Statements and modules.

Finiteness of modules. For rings S, A, compatible scalar towers, and a two-sided ideal I, a Noetherian A-module with uniformly nilpotent I-action is finite over S whenever A ⧸ I is finite over S; no surjective scalar map or nilpotence of I itself is needed. Separately, a simple algebra over a commutative ring admitting a nontrivial compatible module Noetherian over that base is itself Noetherian, hence finite, over the base; the base ring need not be Noetherian. A Noetherian A-semimodule also has a greatest A-submodule finite over compatible scalars S, preserved by every A-linear endomorphism. For the regular module this is a two-sided ideal. Both scalar semirings may be noncommutative, and S need not be Noetherian. Greatest finite submodules · other statements and hypotheses.

Subgroup ideals and coset bases. Over any ring, a subgroup's left difference ideal consists of elements whose coefficient sums vanish on left cosets gH. Over nontrivial rings these ideals reflect subgroup membership, inclusion, finite generation and normality via two-sidedness. Separately, over any semiring, R[G] has a left R[H]-basis indexed by right cosets H * g; finite index gives module finiteness. No normality is required for these coset constructions. Statements · subgroup guide.

Coefficient and index quotients. Over semirings, extension of any left coefficient ideal is characterized coefficientwise. For any semiring homomorphism and monoid, coefficient change preserves and reflects zero kernel powers at each fixed exponent, including zero, without surjectivity. For Ring R, Semiring S, Group G, Monoid M, and maps f : R →+* S, φ : G →* M, the mixed kernel is the sum of the extended coefficient kernel and the kernel-subgroup difference ideal. For arbitrary maps the quotient is the composite's range subsemiring; surjective f gives S[MonoidHom.mrange φ], and surjectivity of both gives S[M]. Normal-subgroup quotients and unchanged coefficient kernel/range quotients have full basis and factorization laws. Statements and guides.

Commuting scalar actions and central idempotents. Commuting ring actions on a module remain commuting after quotienting both rings by annihilating ideals; two-sidedness is needed for quotient rings, not just their scalar actions. For any ring A and two-sided ideal I, the first ideal-square quotient I/I² has commuting left and right A ⧸ I-actions. In any ring, an idempotent central modulo a nilpotent two-sided ideal I is central if both off-diagonal corner maps send I into I²; quotient centrality alone is insufficient. Actions · centrality criterion.

Central summands detected by characters. For a commutative ring R and an R-algebra A Artinian on both sides, every χ : A →ₐ[R] R is one on a central idempotent whose principal left ideal is finite over R with its inherited action. Zero and nonreduced base rings are allowed; the whole algebra need not be finite over R. Statement and proof strategy.

Uniform binomial kernels. For any monoid homomorphism and any ring, its monoid-algebra kernel is the left span of equal-image unit-basis differences. If the source is finitely generated and commutative, one finite family of index pairs works over every coefficient ring. Neither the target monoid nor the coefficients need commute; no coefficient-Noetherian hypothesis is needed. Statements and modules.

Relative module finiteness. For any semiring R and homomorphism f : M →* N of arbitrary monoids, R[N] is finite as a left R[M]-module for its regular action restricted along mapDomainRingHom R f iff there is a finite set T with every n expressible as f m * t, t ∈ T, or R is subsingleton. The source image is on the left; coefficients may be noncommutative, and neither cancellation nor finite generation is assumed. Monomial subalgebra inclusions over nontrivial commutative coefficients satisfy the corresponding finite-cover criterion with their inclusion-induced action. Statements and boundaries · imports and API.

Finite type. For any commutative semiring R and any monoid M, Algebra.FiniteType R (MonoidAlgebra R M) is equivalent to Monoid.FG M ∨ Subsingleton R. Nontrivial coefficients give simply finite generation of M; neither commutativity nor cancellation of M is needed. The additive-monoid counterpart uses the same criterion. Module · statements and use.

Finite presentation. For any commutative ring R and finitely generated commutative monoid M, the canonical R-algebra R[M] is finitely presented. The additive-monoid version is also an instance. Coefficients need not be Noetherian, and exponents need not be cancellative or finite. Module · statements and use.

Chain conditions and regularity. For any ring R and finitely generated commutative monoid M, R[M] is left-Noetherian iff R is. For a commutative group G, the exact criterion is left-Noetherianity of R and Subsingleton R ∨ Group.FG G. A finite-index finitely generated commutative subgroup gives the coefficient-ring criterion even when the ambient group is noncommutative and the subgroup is not normal. For a cancellative monoid over any semiring, a nonzero left ideal finite over the coefficients forces the monoid to be finite. Additive right-compatible coefficient retractions give left-Artinian descent without multiplicativity. Such a retraction exists for every homomorphism from a division ring to a nontrivial semiring, without centrality or finite-dimensionality assumptions. Left-Noetherianity descends to embedded group algebras over any semiring; finite-index subgroup algebras over rings share it with the whole algebra. Over nontrivial rings it forces every subgroup to be finitely generated, without a general converse. The infinite cyclic and finite-index cyclic criteria reduce to the coefficient ring; import GroupRings.MonoidAlgebra.CyclicNoetherian directly for these. Over any ring, infinite-order elements of cancellative monoids give regular monic basis differences, forcing torsion in left-Artinian monoid algebras with nontrivial coefficients. For any ring R and either a left-cancellative or a right-cancellative monoid G, MonoidAlgebra.isArtinianRing_iff_of_isLeftCancelMul and MonoidAlgebra.isArtinianRing_iff give that R[G] is left-Artinian iff R is left-Artinian and Subsingleton R ∨ Finite G. The corresponding finite_of_isArtinianRing theorems give monoid finiteness directly over any nontrivial ring, specializing to the classical group criterion. Locally, over a nontrivial semiring and any monoid, left Artinianity makes every right-regular index a unit; over a nontrivial ring, it also makes every left-regular index a unit, without global cancellation. The global criteria require ring coefficients. All these conditions use the original left regular action. The zero ring is allowed in the criterion, the universes are independent, and no commutativity or right-Artinian hypothesis is imposed. Separately, LaurentPolynomial R is left-Artinian iff R is subsingleton, even for noncommutative or zero rings. Statements and modules.

Laurent coordinates. Supplied coordinates G ≃+ (σ →₀ ℤ) identify an additive commutative group's algebra over a commutative semiring with MvLaurentPolynomial σ A. Free abelian groups have canonical coordinates, with arbitrary, empty or infinite variable types. Statements and module.

Characters and right convolution. Character evaluations on an additive commutative group G are linearly independent over any field K, even for infinite groups without enough roots. For finite G, enough roots of unity of exponent Monoid.exponent (Multiplicative G) give a character basis; with [Fintype G] they give diagonalization and rank for right convolution, whose entry is f (-sigma + tau) and eigenvalue is ∑ x, f x * psi x with positive sign. The eigenvector law needs no enough-roots assumption. Statements · Fourier guide.

Main results

Its formalization.yaml lists 125 main results, and the scan finds 117 of them declared in the file the yaml gives; they are on their own page, not made articles. The scan does not find LinearMap.injective_iff_annihilatorSubmoduleMap (GroupRings/RingTheory/Ideal/ModuleDetection.lean), LinearMap.surjective_iff_mapQ_smul_top (GroupRings/RingTheory/Ideal/ModuleDetection.lean), Submodule.eq_bot_of_isNilpotent_of_smul_eq_self (GroupRings/RingTheory/Ideal/ModuleDetection.lean), Ideal.exists_ne_zero_le_torsionOf_of_pow_le_annihilator (GroupRings/RingTheory/Ideal/Annihilator.lean), Ideal.annihilatorSubmodule (GroupRings/RingTheory/Ideal/Annihilator.lean), Ideal.pow_le_iff_forall_list_prod_mem (GroupRings/RingTheory/Ideal/Powers.lean), RingHom.isNoetherianRing_of_additive_retraction (GroupRings/RingTheory/Noetherian.lean), RingHom.comap_map_eq_of_additive_retraction (GroupRings/RingTheory/Noetherian.lean).

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.