Alphabeta Math
TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)
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.

Every complex affine algebraic action has a finite-dimensional equivariant closed embedding

Statement

Assume AC through the published affine Nullstellensatz and morphism dictionary. Let G be a complex affine algebraic group and X any affine algebraic set with an algebraic G-action. There is a finite-dimensional rational G-module W⊆C[X] generating C[X] as an algebra, such that evaluation ev:X⟶W∗,ev(x)(w)=w(x) is an equivariant isomorphism onto a closed invariant algebraic subset. The target has the dual action (gλ)(w)=λ(g−1w). Neither connectedness, irreducibility, nor reductivity is required; this is an embedding of the action, not merely a faithful representation of G.

Facts & Assumptions

Given: G,X and the algebraic action, and AC (The Axiom of Choice).

[F1]

Coordinates finitely generate A=C[X] (The coordinate ring of a classical affine algebraic set).

[F2]

A finite set of functions lies in a finite-dimensional rational stable subspace (The coordinate ring of an affine algebraic action is a locally finite rational module).

Proof

1.1F1F2givenalgebra

Choose finitely many algebra generators of A by F1 and put them in a finite-dimensional rational submodule W by F2. Then W generates A. Choose a finite basis w1,…,wN of W. Its action has regular matrix entries; the dual action has transpose-inverse matrix, whose entries are regular because inversion g↦g−1 is a morphism. Thus W∗ is a finite-dimensional rational module.

2.1F3F4step 1.1algebra

The coordinate map π:C[z1,…,zN]→A, zi↦wi, is surjective. Its kernel I is radical since A is reduced. F4 identifies C[V(I)] with C[z1,…,zN]/I, and π identifies that quotient with A. F3 gives mutually inverse morphisms X↔V(I) from this algebra isomorphism. The morphism to W∗≅AN is precisely evaluation because its coordinates are wi(x); hence evaluation is an isomorphism onto the closed set V(I). If X is empty, A=0, and I is the unit ideal so the conclusion still holds.

3.1F2step 1.1step 2.1givenalgebra∎

For g∈G, x∈X and w∈W, (g ev(x))(w)=ev(x)(g−1w)=(g−1w)(x)=w(gx)=ev(gx)(w) by the inverse-pullback action on functions. This proves equivariance and invariance of the image. The only choice beyond finite-dimensional selection is the AC inherited by F3 and F4 in step 2.1; local finiteness itself needs no infinite basis.

Depends on

Used by

Dependency tree · two levels

27 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