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.

Semicontinuity of stabilizer and orbit dimension

Statement

Assume the Axiom of Choice inherited from the local fibre-dimension supplier. Let $G$ be a complex affine algebraic group acting algebraically on a classical variety $X$ (Classical complex affine algebraic actions and rational modules). For every integer $n$ the set ${x \in X : \dim G_{x} \geq n}$ is closed in $X$ ; equivalently $x \mapsto \dim G_{x}$ is upper semicontinuous and $x \mapsto \dim G x$ is lower semicontinuous (Global and local dimension of classical varieties). In particular the set of points with infinite stabilizer is closed, and if $X$ is nonempty, the points with stabilizer of minimal dimension form a non-empty open subset.

Facts & Assumptions

Given: AC; a complex affine algebraic group $G$ acting algebraically on a classical variety $X$ , with stabilizers $G_{x}$ for $x \in X$ and the orbit map $β : G \times X \to X \times X$ , $β (g, x) = (x, g x)$ .

[F1]

Local fibre-dimension bound. Let $A \to B$ be a finite-type ring map and let the scheme fibre at $q$ have local dimension $n$ at the corresponding point; then there is an open neighbourhood $V$ of $q$ in $Spec B$ such that every fibre over $V$ has local dimension at most $n$ at the corresponding point (Local fibre-dimension bound from polynomial quasi-finiteness, clause 2). This is the affine-local form of openness of the locus where the fibre local dimension is at most $n$ for a morphism locally of finite type.

[F2]

Local dimension convention. The local dimension $\dim_{y} Y$ is the infimum of the Krull dimensions of open neighbourhoods of $y$ , and for a scheme locally of finite type over a field it equals the largest dimension of an irreducible component through $y$ (Relative dimension of a smooth morphism at a point).

[F3]

Fibres of the orbit map. For a finite-type group scheme acting on a separated finite-type scheme, the fibre of the orbit map over a closed point $y = g_{0} x$ is the translate $g_{0} G_{x}$ , and $G_{g x} = g G_{x} g^{- 1}$ (Fibres of the orbit map and the scheme-theoretic stabilizer as a closed subgroup scheme, clauses (b) and (c), the target factors swapped to match $β (g, x) = (x, g x)$ ). Read classically, the fibres of $β$ over closed points are translates of closed subgroups.

[F4]

Pure dimension of closed subgroups. A classical closed subgroup $H$ is itself a complex affine algebraic group, so it has pure dimension $\dim H$ (Complex affine algebraic groups are smooth). By [F2] its local dimension at every closed point is $\dim H$ . Reduction does not change components or dimensions, so the same holds for the underlying stabilizer scheme.

[F5]

Orbit dimension. For every $x$ in a classical variety with a complex affine algebraic group action, $\dim G = \dim G_{x} + \dim G x$ (Orbit dimension and closed orbits for complex group actions, (a)).

Proof

technique · direct

1.1F3

The map $β : G \times X \to X \times X$ , $β (g, x) = (x, g x)$ , is a morphism of finite-type schemes over $C$ : its components are the second projection and the action morphism. For a closed point $(g, x)$ of the source, the scheme fibre $β^{- 1} (x, g x)$ is the translate $g G_{x}$ of the stabilizer, a closed subgroup translate; this is the supplier statement read with the two target factors in the order used by $β$ .

2.1F2F4step 1.1

Fix a closed point $(g, x)$ and let $H = G_{x}$ . By [F4] the reduction of $H$ has pure dimension $\dim H$ , so [F2] makes its local dimension at every closed point equal to $\dim H = \dim G_{x}$ . The underlying components and dimensions are unchanged by reduction or translation, so the same holds for $g H$ . Hence the local dimension of the fibre of $β$ at $(g, x)$ equals $\dim G_{x}$ .

3.1F1F2step 2.1

Let $n$ be an integer. Apply [F1] affine-locally to $β$ at every source point whose fibre has local dimension $d \leq n$ . Each such point has an open neighbourhood on which the fibre local dimension is at most $d \leq n$ , so this locus is open in $G \times X$ . On complex closed points, step 2.1 identifies the condition with $\dim G_{x} \leq n$ .

4.1F3step 3.1

The identity section $s : X \to G \times X$ , $x \mapsto (e, x)$ , is a morphism; pulling back the open set of step 3.1 along $s$ gives that ${x \in X : \dim G_{x} \leq n}$ is open in $X$ . Taking the complement at level $n - 1$ shows that ${x \in X : \dim G_{x} \geq n}$ is closed, so $x \mapsto \dim G_{x}$ is upper semicontinuous.

5.1F5step 4.1∎

By the orbit dimension formula, $\dim G x = \dim G - \dim G_{x}$ ; since a constant minus an upper semicontinuous function is lower semicontinuous, $x \mapsto \dim G x$ is lower semicontinuous. A closed subgroup of the finite-type complex group $G$ is finite exactly when its dimension is zero, so the locus of points with infinite stabilizer is ${x : \dim G_{x} \geq 1}$ , closed by step 4.1. If $X$ is nonempty, the set of attained values ${\dim G_{x} : x \in X}$ is a nonempty subset of ${0, 1, \dots, \dim G}$ and has a minimum $m$ ; then ${x : \dim G_{x} \leq m}$ is nonempty, open by step 4.1, and is exactly the locus of stabilizers of minimal dimension. This proves all assertions.

Remarks

This is Brion's Lemma 1.14 with the general local-fibre-dimension supplier of Stacks Morphisms, Lemma 29.29.4 (tag 02FZ), whose proof reduces to Stacks Algebra, Lemma 10.125.6; neither properness nor projectivity of the orbit map is used. The dimension used is the local dimension of the fibre in the component sense, not the dimension of a possibly nonreduced stabilizer scheme's local ring.
All Axiom of Choice content is inherited from the published local fibre-dimension bound and from the orbit-dimension lemma.

Depends on

Used by

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

Dependency tree · two levels

70 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)
The Stacks Project, Morphisms of Schemes, Lemma 29.29.4 (tag 02FZ) (standard reference, not scraped)