LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge 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.

Invariants separate a stable point from a disjoint closed invariant subset

Statement

Assume the Axiom of Choice inherited from the named suppliers. Let $G$ be a complex reductive affine algebraic group acting algebraically on an affine algebraic set $X$ , with categorical quotient $π : X \to X / ⁣ / G$ (Finite generation of invariants and the affine categorical quotient). Let $Z \subseteq X$ be closed and $G$ -stable, and let $x \in X$ with $π (x) \notin π (Z)$ . Then there exists $f \in C [X]^{G}$ with $f (x) \neq 0$ and $f ∣_{Z} = 0$ .

Facts & Assumptions

Given: AC; a complex reductive affine algebraic group $G$ acting on an affine algebraic set $X$ ; the categorical quotient $π : X \to X / ⁣ / G$ ; a closed $G$ -stable subset $Z \subseteq X$ and a point $x \in X$ with $π (x) \notin π (Z)$ .

[F1]

Closed images of closed invariant subsets. For every closed $G$ -stable subset $Y \subseteq X$ the morphism $Y / ⁣ / G \to X / ⁣ / G$ is a closed immersion, and for closed $G$ -stable $Y, Y^{'} \subseteq X$ one has $π (Y \cap Y^{'}) = π (Y) \cap π (Y^{'})$ (Finite generation of invariants and the affine categorical quotient, clause (iv)).

[F2]

Separation by regular functions. In an affine algebraic set, a point outside a closed subset is separated from it by a regular function: if $q$ is a maximal ideal of a coordinate ring $A$ and $C \subseteq Spec A$ is the closed set of a radical ideal $a \subseteq̸ q$ , then there is $g \in a$ with $g (q) \neq 0$ (Classical affine algebraic sets correspond to radical ideals, and irreducible sets to prime ideals).

Proof

technique · direct

1.1F1

The image $π (Z)$ is closed in $X / ⁣ / G$ : since $Z$ is closed and $G$ -stable, [F1] makes $Z / ⁣ / G \to X / ⁣ / G$ a closed immersion; its image is $π (Z)$ , because $π ∣_{Z}$ is surjective onto $Z / ⁣ / G$ by the quotient theorem and the underlying set of the closed immersion is that image.

2.1F2step 1.1

By hypothesis $π (x) \notin π (Z)$ , so in the affine algebraic set $X / ⁣ / G$ the point $π (x)$ , viewed as the maximal ideal $m_{π (x)}$ of $C [X / ⁣ / G] = C [X]^{G}$ , does not contain the radical ideal $a$ of the closed set $π (Z)$ ; by [F2] there is $\overset{ˉ}{f} \in a \subseteq C [X]^{G}$ with $\overset{ˉ}{f} (π (x)) \neq 0$ and $\overset{ˉ}{f} ∣_{π (Z)} = 0$ .

3.1step 2.1∎

Put $f = π^{*} (\overset{ˉ}{f}) = \overset{ˉ}{f} \circ π \in C [X]^{G}$ . Then $f (x) = \overset{ˉ}{f} (π (x)) \neq 0$ , and for $z \in Z$ one has $f (z) = \overset{ˉ}{f} (π (z)) = 0$ because $π (z) \in π (Z)$ ; hence $f ∣_{Z} = 0$ . This is the required invariant.

Remarks

This is the first step of Brion's proof of Proposition 1.26 (printed pp. 9-10): the closedness of $π (Z)$ is clause (iv) of the affine quotient theorem, and the separating function is produced on the quotient and pulled back along $π$ .
AC is inherited from the quotient and Nullstellensatz suppliers; the pullback construction itself is choice-free.

Depends on

Used by

Projective GIT quotient for a linear action Theorem
The stable locus has a geometric quotient Theorem

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

Michel Brion, Introduction to actions of algebraic groups, Les cours du CIRM 1 (2010), no. 1, 1-22 (standard reference, not scraped)