Alphabeta Math
DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-generated
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 Heisenberg group of a finite-dimensional symplectic vector space

Definition

Let (V,ω) be a finite-dimensional real symplectic vector space, so V is a finite-dimensional real vector space and ω:V×V→R is an alternating, nondegenerate bilinear form (Symplectic vector space). Define H(V,ω):=V×Rwith the product topology and multiplication$$ (v,t)(w,s)=\left(v+w,\ t+s-\frac12\omega(v,w)\right).

The proposed identity is $(0,0)$, and the central coordinate is the subgroup $j(\mathbb R)=\{(0,t):t\in\mathbb R\}$. The lemma [Heisenberg group polarization and the fixed-central-character orbit](/item/lem-heisenberg-group-lagrangian-splitting-and-dual-orbit "forward-reference") verifies that this is a second-countable locally compact topological group and that $j(\mathbb R)$ is its center. The maps $j(t)=(0,t)$ and $\operatorname{pr}_V(v,t)=v$ form the central extension shown below. The diagram records the maps; exactness is established by the explicit kernel computation in the cited lemma.
diagram failed to render:
1 \arrow[r] & \mathbb R \arrow[r, hook, "j"] & H(V,\omega) \arrow[r, two heads, "\operatorname{pr}_V"] & V \arrow[r] & 1

Depends on

Used by

Dependency tree · two levels

6 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