Alphabeta MathHow 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.
An elementary abelian -group has a canonical -vector-space structure
Statement
The rule gives every elementary abelian -group its canonical -vector-space structure, with the group operation as vector addition and the identity as zero.
Facts & Assumptions
Given: An elementary abelian -group , a residue class , and , with integer powers as in Powers : natural exponents in a monoid and integer exponents in a group, with .
An elementary abelian -group is a finite abelian -group in which every nonidentity element has order ; the trivial group is permitted (Elementary abelian -groups).
For every prime , addition and multiplication make a field (For every prime , the two operations on make it a field).
The additive structure of is an abelian group and multiplication distributes over addition (For every natural , is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold).
For integers , one has and ; if , then (Exponent laws in a group: and for all , and when and commute).
Proof
If , then for an integer . Since by [F1], the power laws in [L3] give . Thus is independent of the representative.
The power laws in [L3] and commutativity give , , , , and . Together with [L1] and [L2], these are the vector-space axioms.
The scalar structure uses the existing abelian group law and does not change its elements. In particular its additive group remains finite, abelian, and of exponent , including the zero-dimensional trivial case.
Depends on
- Elementary abelian $p$-groups
- For every prime $p$, the two operations on $\mathbb{Z}/p$ make it a field
- For every natural $n$, $(\mathbb{Z}/n,+)$ is an abelian group, multiplication is a commutative monoid operation, and both distributive laws hold
- Powers $g^{n}$: natural exponents in a monoid and integer exponents in a group, with $g^{0} = e$
- Exponent laws in a group: $g^{m+n} = g^{m}g^{n}$ and $(g^{m})^{n} = g^{mn}$ for all $m, n \in \mathbb{Z}$, and $(gh)^{n} = g^{n}h^{n}$ **when $g$ and $h$ commute**
Used by
- An extraspecial p-group of order p¹⁺²ⁿ has generator rank 2n Corollary
- Fₚ-spanning sets, independence, and bases in an elementary abelian p-group Definition
- The commutator pairing of an extraspecial p-group relative to a chosen generator of its centre Definition
- The square map of an extraspecial 2-group relative to a chosen generator of its centre Definition
- A subgroup of the central quotient and its orthogonal complement have orders multiplying to the order of the quotient Lemma
- The commutator pairing is well defined on the central quotient, is bilinear over Fₚ, and is alternating Lemma
- The square map is well defined on the central quotient and satisfies q(x̄ȳ)=q(x̄)+q(ȳ)+b(x̄,ȳ) Lemma
- Two elements of an extraspecial p-group with nontrivial commutator generate an extraspecial subgroup of order p³ Lemma
- A unique abelian minimal normal subgroup gives affine type Proposition
- Automorphisms act linearly on the Frattini quotient Theorem
- The Frattini quotient is the largest elementary abelian quotient of a finite p-group Theorem
Dependency tree · two levels
32 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
- K. Conrad, Generating Sets, §6 (standard reference, not scraped)