Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedprecheck passaudited 2026-08-26
How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

  • Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
  • AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
  • AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

When the group order is invertible the Reynolds operator retracts a ring onto its invariants

Example

Let G be a finite group of order N≥1 acting by ring automorphisms on a commutative ring S (A group acting on a ring by automorphisms and its invariant subring), and suppose the element u:=N⋅1S, the N-fold sum of 1S with itself, is invertible in S. Define the Reynolds operator

ρ ⁣:S⟶SG,ρ(s):=u−1∑g∈Gg⋅s.

Then ρ takes values in SG, is SG-linear, and satisfies ρ(a)=a for every a∈SG. So ρ is a retraction of the inclusion SG⊆S as a map of SG-modules, and A subring that admits a module retraction from a Noetherian ring is Noetherian gives: if S is Noetherian then SG is Noetherian.

This neither contains nor is contained in Noether's finiteness theorem: the invariants of a finite group acting on a finite-type algebra over a Noetherian ring form an algebra of finite type. Noether's theorem needs a Noetherian subring A⊆S, the finite-type hypothesis over A, and an action by A-algebra automorphisms; this example drops the finite-type and fixed-base-ring hypotheses, adds the hypothesis that N be invertible, and concludes only that SG is Noetherian rather than of finite type over a specified base ring.

Facts & Assumptions

Given: A finite group G of order N≥1 acting by ring automorphisms on a commutative ring S in which u=N⋅1S is invertible.

[L1]

For an action of a group G on a commutative ring C by ring automorphisms, CG={c∈C:g⋅c=c for every g∈G} is a subring of C, and each g acts as a ring automorphism, so g⋅1C=1C (A group acting on a ring by automorphisms and its invariant subring).

[L2]

A left action satisfies e⋅c=c and (gh)⋅c=g⋅(h⋅c) (Left group actions, transitive actions, and faithful actions).

[L3]

In a group every element has a two-sided inverse and the operation is associative (Group and abelian group).

[L4]

In a ring, addition is associative and commutative, multiplication is associative, 1 is a two-sided multiplicative identity, and multiplication distributes over addition on both sides (Ring: an abelian group under addition and a monoid under multiplication, with multiplication distributing over addition on both sides).

[L5]

A subset S of a ring is a subring when 1∈S and S is closed under addition, additive inverses and multiplication (Subring: a subset containing 1R and closed under addition, additive inverses and multiplication).

[L6]

A function f ⁣:M→N between R-modules is an R-module homomorphism when f(m+m′)=f(m)+f(m′) and f(rm)=rf(m) for all m,m′∈M and r∈R (Module homomorphism and isomorphism, kernel, image and cokernel).

[L7]

If R′ is a Noetherian commutative ring, R⊆R′ a subring, and ρ ⁣:R′→R is R-linear with ρ(x)=x for every x∈R, then R is Noetherian (A subring that admits a module retraction from a Noetherian ring is Noetherian).

[L8]

For A Noetherian, C a commutative A-algebra of finite type with A a subring of C, and G a finite group acting on C by A-algebra automorphisms, CG is of finite type over A (Noether's finiteness theorem: the invariants of a finite group acting on a finite-type algebra over a Noetherian ring form an algebra of finite type).

Verification

technique · direct
1.1L1L4given

The element u=N⋅1S is fixed by the action, and so is its inverse. Each h∈G acts as a ring homomorphism, so it is additive and sends 1S to 1S; applying it to the N-fold sum 1S+⋯+1S gives h⋅u=u. Applying h to uu−1=1S gives u (h⋅u−1)=1S; left-multiplying by u−1 and using associativity, u−1u=1S, and 1Sx=x yields h⋅u−1=u−1. The formula ρ(s)=u−1∑g∈Gg⋅s therefore defines a function S→S, the sum being over the finite set G.

2.1L1L2L3step 1.1

ρ takes values in SG. For h∈G, additivity of the action of h and step 1.1 give h⋅ρ(s)=u−1∑g∈Gh⋅(g⋅s)=u−1∑g∈G(hg)⋅s; and g↦hg is a bijection of G onto itself, with inverse g↦h−1g, so it merely reindexes the sum and h⋅ρ(s)=ρ(s).

2.2L1L4L6step 1.1

ρ is SG-linear. Additivity is additivity of each g together with associativity and commutativity of addition. For a∈SG and s∈S, each g is multiplicative and fixes a, so g⋅(as)=(g⋅a)(g⋅s)=a (g⋅s); summing and using distributivity gives ρ(as)=u−1 a∑g(g⋅s)=a ρ(s), where a and u−1 commute because S is commutative.

2.3L1L4step 1.1

ρ fixes SG pointwise. For a∈SG every term of the sum is a, so ∑g∈Gg⋅a is the N-fold sum of a, which by distributivity is ua; hence ρ(a)=u−1(ua)=a.

3.1L1L5L7step 2.1step 2.2step 2.3

So SG is a subring of S and ρ ⁣:S→SG is SG-linear with ρ(a)=a for every a∈SG: it is a retraction of the inclusion as a map of SG-modules. If S is Noetherian, the retraction lemma applies with R′=S and R=SG and gives that SG is Noetherian.

4.1L8step 3.1algebra∎

The comparison with Noether's theorem, and the caveat. Noether's theorem needs a Noetherian subring A⊆C, the finite-type hypothesis over A, and an action by A-algebra automorphisms, and it concludes that CG is of finite type over A. The argument here uses none of the finite-type or fixed-base-ring hypotheses and concludes only that SG is Noetherian, at the cost of the invertibility of u. That cost is real: in S=F2[x], the substitution x↦x+1 defines an automorphism of order 2, but for the resulting action of the order-two group one has u=2⋅1S=0, so ρ is not defined.

Remarks

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

28 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources