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 maximal elementary abelian subgroups of the two extraspecial groups of order have orders and
Statement
The maximal elementary abelian subgroups of the two extraspecial groups of order have orders and .
Facts & Assumptions
Given: The hypotheses of the Statement.
For an extraspecial -group of order with , the square map is the function determined by , with values in (The square map of an extraspecial -group relative to a chosen generator of its centre).
The square map is well defined on the central quotient and satisfies (The square map is well defined on the central quotient and satisfies ).
For each there are exactly two extraspecial groups of order up to isomorphism, with and solutions of (For each there are exactly two extraspecial groups of order ).
If and are extraspecial -groups with solutions of , then has such solutions (A product formula for the number of square roots of the identity in a central product of extraspecial -groups).
Every maximal abelian subgroup of an extraspecial -group of order has order (In an extraspecial -group of order every maximal abelian subgroup has order ).
An extraspecial -group has order for some (An extraspecial -group has order for some ).
The commutator pairing is independent of the coset representatives, is -bilinear on , and is alternating (The commutator pairing is well defined on the central quotient, is bilinear over , and is alternating).
The commutator pairing of an extraspecial -group has trivial radical (The commutator pairing of an extraspecial -group has trivial radical).
For an extraspecial -group with , the commutator pairing is the map determined by (The commutator pairing of an extraspecial -group relative to a chosen generator of its centre).
An elementary abelian -group is a finite abelian -group in which every nonidentity element has order ; the trivial group is permitted (,, ). (Elementary abelian -groups).
The set is independent when with finite support forces every . A basis of an elementary abelian -group is an independent spanning subset for its canonical -linear structure. (-spanning sets, independence, and bases in an elementary abelian -group).
Every finite elementary abelian -group has a basis; every independent subset extends to a basis, every spanning subset contains a basis, and all bases have the same finite size. (Finite elementary abelian -groups have bases, basis extension, and a well-defined dimension).
An extraspecial -group of order is of plus type when it has solutions of and of minus type when it has such solutions; for odd , plus and minus mean exponent and respectively (Plus and minus type of an extraspecial -group).
A central product of extraspecial -groups identified along their centres is extraspecial (A central product of extraspecial -groups identified along their centres is extraspecial).
Every extraspecial -group is an internal central product of nonabelian subgroups of order pairwise intersecting in its centre (Every extraspecial -group is an internal central product of nonabelian subgroups of order ).
Proof
A maximal elementary abelian subgroup contains , so has order with , and vanishes on .
On a coset with the map is a nonzero -linear functional on , so its kernel has index two and exactly of the coset's classes have .
Maximality of says no orthogonal to has : the polar identity would make vanish on , whose preimage is a strictly larger elementary abelian subgroup.
On the coset itself vanishes identically, contributing classes.
On a coset with the correction term vanishes, so is constantly by step 2.1 and the coset contributes no class.
With there are cosets inside the complement and outside, so the classes with number , and the elements with number twice that.
The classification counts those elements as in the plus case and in the minus case, so .
The left side is strictly increasing in , so in the plus case and in the minus case are the only solutions; both are attained, giving and for EVERY maximal elementary abelian subgroup.
Independently, is abelian, so the maximal-abelian bound gives and hence without the monotonicity argument; this is the free half of the plus case.
Depends on
- A central product of extraspecial $p$-groups identified along their centres is extraspecial
- Every extraspecial $p$-group is an internal central product of nonabelian subgroups of order $p^3$
- The square map of an extraspecial $2$-group relative to a chosen generator of its centre
- The square map is well defined on the central quotient and satisfies $q(\bar x\bar y)=q(\bar x)+q(\bar y)+b(\bar x,\bar y)$
- The commutator pairing of an extraspecial $p$-group relative to a chosen generator of its centre
- The commutator pairing is well defined on the central quotient, is bilinear over $\mathbb F_p$, and is alternating
- The commutator pairing of an extraspecial $p$-group has trivial radical
- A subgroup of the central quotient and its orthogonal complement have orders multiplying to the order of the quotient
- In an extraspecial $p$-group of order $p^{1+2n}$ every maximal abelian subgroup has order $p^{1+n}$
- An extraspecial $p$-group has order $p^{1+2n}$ for some $n\ge1$
- A product formula for the number of square roots of the identity in a central product of extraspecial $2$-groups
- For each $n\ge1$ there are exactly two extraspecial groups of order $2^{1+2n}$
- Plus and minus type of an extraspecial $p$-group
- Elementary abelian $p$-groups
- $\mathbb F_p$-spanning sets, independence, and bases in an elementary abelian $p$-group
- Finite elementary abelian $p$-groups have bases, basis extension, and a well-defined dimension
- Lagrange's theorem: $|G|=[G:H]|H|$ for every subgroup $H$ of a finite group $G$
- The subgroup $\langle S \rangle$ generated by a subset, the cyclic subgroup $\langle g \rangle$, and cyclic groups
- The center $Z(G)$ of a group
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
69 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
- D. A. Craven, The Theory of p-Groups, Proposition 3.14(ii) (standard reference, not scraped)
- M. van Beek, Topics in Finite p-Groups, Proposition 2.39(ii) (standard reference, not scraped)