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.
Categorical and geometric quotients of classical varieties
Definition
Let be a complex affine algebraic group acting algebraically on a classical variety (Classical algebraic prevarieties, regular maps, and varieties, Classical complex affine algebraic actions and rational modules). A -invariant morphism is a categorical quotient if every -invariant morphism of classical varieties factors uniquely as with a morphism.
It is a geometric quotient (Brion Definition 1.18) if
(i) is surjective and its fibres are exactly the -orbits,
(ii) a subset is open if and only if is open in , and
(iii) for every open the pullback of regular functions is an isomorphism onto the -invariant regular functions on the preimage.
A geometric quotient is a categorical quotient and is unique up to unique isomorphism; when it exists its underlying topological space is the orbit space with the quotient topology. For an affine -variety whose invariant algebra is finitely generated, the affine model is the morphism induced by the inclusion . For a reductive , the theorem below proves this finite generation and makes the model a categorical quotient with one closed orbit in each fibre (Finite generation of invariants and the affine categorical quotient ↗).
Why a geometric quotient is categorical. Let satisfy (i)–(iii) and let be a -invariant morphism to a classical variety . By (i) two points of a fibre of lie in one orbit, on which is constant, so factors through a unique set map . For open, is open in by continuity of , so is open in by (ii): is continuous. If is an affine chart of with coordinates and , then is a -invariant regular function on , hence by (iii) is the pullback along of a unique regular function on ; that function is . Since this holds for every coordinate of an affine chart, is a morphism (A morphism from an open subset of a classical affine variety to an affine variety, Classical algebraic prevarieties, regular maps, and varieties), and local agreement of the resulting morphisms on overlapping charts gives a morphism . Surjectivity in (i) makes the factorisation unique. If also is a categorical quotient, the universal property applied to and to yields morphisms with and with ; then and , so uniqueness of the factorisation of through and of through forces and . Thus categorical and geometric quotients are unique up to unique isomorphism, and for a geometric quotient (i)–(ii) say exactly that the underlying map is the quotient map of the orbit equivalence relation with the quotient topology.
Conventions. This is the classical notion of Brion Definition 1.18 and the paragraph after Theorem 1.24. The scheme-theoretic fppf quotient sheaf on the AG-ACT-1 page is a different object and is not identified with this classical notion here. In the classical register, of a finitely generated reduced complex algebra denotes its associated affine variety of complex closed points with the classical regular-function sheaf; no identification with the space of every scheme prime is used. For empty the coordinate algebra is zero and its quotient is empty; finite generation and the universal properties below are then immediate and fibre assertions are vacuous. The definition itself uses no Axiom of Choice; the finite-generation theorem referred to above inherits AC from its own named suppliers, so consumers of that theorem carry AC, while nothing in this definition does.