PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-22

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.

Regularity of a moment map is equivalent to local freeness

Statement

Assume ${A C}_{ω}$ . For a Hamiltonian $G$ -space with moment map $μ$ and a point $p \in M$ , the differential $d μ_{p} : T_{p} M \to g^{*}$ is surjective if and only if the infinitesimal stabilizer $g_{p}$ is zero. Consequently a covector $α \in g^{*}$ is a regular value of $μ$ if and only if $g_{p} = 0$ for every $p \in μ^{- 1} (α)$ , that is, if and only if the action is locally free along the level $μ^{- 1} (α)$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , a Hamiltonian $G$ -space with moment map $μ$ , and a point $p \in M$ .

[A1]

${A C}_{ω}$ is countable choice; it is used only through the fundamental-field interface cited in [F1] and [F2].

[F1]

$im d μ_{p} = ann (g_{p})$ . The differential of the moment map and the orbit-orthogonal identity.

[F2]

The infinitesimal orbit map has kernel exactly the stabilizer Lie algebra $g_{p} = T_{e} G_{p}$ , and $G_{p}$ is a closed embedded Lie subgroup. Kernel of the infinitesimal orbit map, Stabilizers are closed embedded Lie subgroups.

[F3]

A subgroup of a finite-dimensional real Lie group is discrete in the subspace topology if and only if it is a closed embedded zero-dimensional Lie subgroup; a Lie group is zero-dimensional exactly when its Lie algebra is zero. Discrete subgroups are closed embedded zero-dimensional Lie subgroups.

[F4]

A value of a smooth map is regular when the differential is surjective at every point of its fibre. Regular and critical points and values.

Proof

technique · direct

1.1

By [F1], surjectivity of $d μ_{p}$ is equivalent to $ann (g_{p}) = g^{*}$ , which holds if and only if $g_{p} = 0$ : if $g_{p}$ contained a nonzero vector then some linear functional would not vanish on it, and conversely $ann (0) = g^{*}$ .

F1given

1.2

By [F2] and [F3], $g_{p} = 0$ is equivalent to the stabilizer $G_{p}$ being discrete: $g_{p}$ is the Lie algebra of $G_{p}$ , so it vanishes exactly when $G_{p}$ is zero-dimensional, and by [F3] that is equivalent to discreteness of $G_{p}$ .

F2F3

2.1

Combining steps 1.1 and 1.2, $d μ_{p}$ is surjective exactly when the stabilizer $G_{p}$ is discrete, i.e. when the action is locally free at $p$ . Applying this at every point of the fibre of a covector $α$ and using [F4], $α$ is a regular value of $μ$ exactly when the stabilizers along $μ^{- 1} (α)$ are discrete, i.e. when the action is locally free along the level.

step 1.1step 1.2F4A1∎

Depends on

Used by

The zero angular-momentum level has nonfree points and no regular reduction Counterexample
Complex projective space as a circle symplectic reduction Example
Grassmannians from unitary symplectic reduction Example
Weighted circle actions and weighted projective singular quotients Example
Every value of a moment map gives a smooth symplectic quotient False statement
The general reduced dimension is dim M minus two dim G False statement
The dimension of a regular reduced space at a nonzero value Proposition
The shifting trick identifies reduction at a value with a zero reduction Proposition
Nonregular or nonfree symplectic quotients need not be manifolds Remark

Dependency tree · two levels

25 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

Eckhard Meinrenken, Symplectic Geometry (standard reference, not scraped)
Ana Cannas da Silva, Lectures on Symplectic Geometry (standard reference, not scraped)