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 be a complex affine algebraic group and any affine algebraic set with an algebraic -action. There is a finite-dimensional rational -module generating as an algebra, such that evaluation is an equivariant isomorphism onto a closed invariant algebraic subset. The target has the dual action . Neither connectedness, irreducibility, nor reductivity is required; this is an embedding of the action, not merely a faithful representation of .
Facts & Assumptions
Given: and the algebraic action, and AC (The Axiom of Choice).
Coordinates finitely generate (The coordinate ring of a classical affine algebraic set).
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).
Affine algebra maps reconstruct morphisms (Classical affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms).
A radical ideal is exactly (Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals).
Proof
Choose finitely many algebra generators of by F1 and put them in a finite-dimensional rational submodule by F2. Then generates . Choose a finite basis of . Its action has regular matrix entries; the dual action has transpose-inverse matrix, whose entries are regular because inversion is a morphism. Thus is a finite-dimensional rational module.
The coordinate map , , is surjective. Its kernel is radical since is reduced. F4 identifies with , and identifies that quotient with . F3 gives mutually inverse morphisms from this algebra isomorphism. The morphism to is precisely evaluation because its coordinates are ; hence evaluation is an isomorphism onto the closed set . If is empty, , and is the unit ideal so the conclusion still holds.
For , and , 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
- Classical complex affine algebraic actions and rational modules
- The coordinate ring of an affine algebraic action is a locally finite rational module
- The coordinate ring of a classical affine algebraic set
- Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals
- Classical affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms
- The Axiom of Choice
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
- Michel Brion, Introduction to actions of algebraic groups (2010) (standard reference, not scraped)
- Philippe Gille, Introduction to reductive group schemes over rings, full notes retrieved 2026-10-02 (standard reference, not scraped)
- J. S. Milne, Algebraic Groups (2022) (standard reference, not scraped)