PropositionStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 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.

The dimension of a regular reduced space at a nonzero value

Statement

Assume ${A C}_{ω}$ . Let $(M, ω, G, μ)$ be a Hamiltonian $G$ -space, let $α \in g^{*}$ be a regular value with nonempty level, and suppose that $G_{α}$ acts freely and properly on $μ^{- 1} (α)$ . Then the reduced space $M_{α} = μ^{- 1} (α) / G_{α}$ has dimension

$\dim M_{α} = \dim M - \dim G - \dim G_{α} .$

In particular the value $α$ enters the formula only through the dimension of its coadjoint stabilizer, and at $α = 0$ , where $G_{α} = G$ , the formula specialises to $\dim M - 2 \dim G$ .

Facts & Assumptions

Given: ${A C}_{ω}$ , a Hamiltonian $G$ -space, a regular value $α$ with nonempty level, and a free proper $G_{α}$ -action on the level.

[A1]

${A C}_{ω}$ is countable choice; it is used only through the reduction and fundamental-field suppliers.

[F1]

$M_{α}$ is the quotient of $μ^{- 1} (α)$ by the free proper $G_{α}$ -action. Marsden--Weinstein--Meyer symplectic reduction.

[F2]

Regularity of $α$ means $d μ_{p}$ is surjective at every $p$ in the level, so $\dim μ^{- 1} (α) = \dim M - \dim g$ . Regularity of a moment map is equivalent to local freeness, The differential of the moment map and the orbit-orthogonal identity.

[F3]

Quotienting a manifold by a free proper $G_{α}$ -action lowers the dimension by $\dim G_{α}$ . Marsden--Weinstein--Meyer symplectic reduction.

[F4]

The coadjoint stabilizer of $0$ is $G$ , and $\dim G_{α} = \dim g_{α}$ . The coadjoint representation, action and orbits.

Proof

technique · direct

1.1

By [F2] the level has dimension $\dim M - \dim g$ .

F2given

2.1

By [F3] the quotient by the free proper $G_{α}$ -action subtracts $\dim G_{α}$ , so $\dim M_{α} = \dim M - \dim g - \dim G_{α} = \dim M - \dim G - \dim G_{α}$ , using that a Lie group and its Lie algebra have equal dimension.

step 1.1F1F3

3.1

For $α = 0$ the coadjoint action is linear, so every group element fixes $0$ and $G_{0} = G$ by [F4]; the formula then reads $\dim M_{0} = \dim M - 2 \dim G$ , consistent with the zero-level corollary.

step 2.1F4A1∎

Depends on

Used by

Grassmannians from unitary symplectic reduction Example
The shifting trick for a nonzero coadjoint orbit Example
The general reduced dimension is dim M minus two dim G False statement

Dependency tree · two levels

36 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)