PropositionStatement: Literature-sourcedProof: AI-adaptedSession-authored (Fable 5 assisted)precheck passaudited 2026-08-26

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.

In an extraspecial $p$ -group of order $p^{1 + 2 n}$ every maximal abelian subgroup has order $p^{1 + n}$

Statement

Let $P$ be an extraspecial $p$ -group of order $p^{1 + 2 n}$ . Call an abelian subgroup of $P$ maximal abelian when it is not properly contained in any abelian subgroup of $P$ . Then maximal abelian subgroups exist, every one of them contains $Z (P)$ , and every one of them has order $p^{1 + n}$ . Under the correspondence $A \mapsto A / Z (P)$ they are exactly the subgroups $A$ with $Z (P) \leq A \leq P$ whose image $U = A / Z (P)$ in $V = P / Z (P)$ satisfies $U = U^{⊥}$ .

Facts & Assumptions

Given: An extraspecial $p$ -group $P$ of order $p^{1 + 2 n}$ , the quotient $V = P / Z (P)$ with its commutator pairing $b_{z}$ , and for $U \leq V$ the subgroup $U^{⊥} = {v \in V : b_{z} (v, u) = 0 for all u \in U}$ .

[F1]

The commutator pairing of $P$ relative to $z$ is the map $b_{z} : V \times V \to F_{p}$ determined by $[x, y] = z^{b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})}$ (The commutator pairing of an extraspecial $p$ -group relative to a chosen generator of its centre).

[F2]

$Z (G) : = {z \in G : z g = g z for every g \in G}$ (The center $Z (G)$ of a group).

[F3]

$⟨ S ⟩$ is the smallest subgroup of $G$ containing $S$ (The subgroup $⟨ S ⟩$ generated by a subset, the cyclic subgroup $⟨ g ⟩$ , and cyclic groups).

[L1]

The commutator pairing is well defined, $F_{p}$ -bilinear and alternating, with $b_{z} (\overset{ˉ}{y}, \overset{ˉ}{x}) = - b_{z} (\overset{ˉ}{x}, \overset{ˉ}{y})$ (The commutator pairing is well defined on the central quotient, is bilinear over $F_{p}$ , and is alternating).

[L2]

An extraspecial $p$ -group has $∣ P ∣ = p^{1 + 2 n}$ with $n \geq 1$ and $∣ P / Z (P) ∣ = p^{2 n}$ (An extraspecial $p$ -group has order $p^{1 + 2 n}$ for some $n \geq 1$ ).

[L3]

For a subgroup $U$ of $V$ , $∣ U ∣ ∣ U^{⊥} ∣ = ∣ V ∣ = p^{2 n}$ (A subgroup of the central quotient and its orthogonal complement have orders multiplying to the order of the quotient).

[L4]

For $N ⊴ G$ the maps $H \mapsto H / N$ and $K \mapsto π^{- 1} (K)$ are inverse inclusion-preserving bijections between subgroups $H$ with $N \leq H \leq G$ and subgroups $K \leq G / N$ (Correspondence theorem: subgroups of $G / N$ correspond to subgroups of $G$ containing $N$ , with normality preserved).

[L5]

For a finite group $G$ and $H \leq G$ , $∣ G ∣ = [G : H] ∣ H ∣$ (Lagrange's theorem: $∣ G ∣ = [G : H] ∣ H ∣$ for every subgroup $H$ of a finite group $G$ ).

[L6]

For a finite $p$ -group $P$ the following are equivalent: $P$ is extraspecial; $P$ is nonabelian, $∣ Z (P) ∣ = p$ and $P / Z (P)$ is elementary abelian; $P$ is nonabelian and $Z (P) = P^{'} = Φ (P)$ has order $p$ (Three equivalent descriptions of an extraspecial $p$ -group).

Proof

technique · direct

1.1

If $B \leq P$ is abelian then $B Z (P)$ is a subgroup, because $Z (P)$ is normal, and it is abelian, because $(b u) (b^{'} u^{'}) = b b^{'} u u^{'} = (b^{'} u^{'}) (b u)$ for $u, u^{'} \in Z (P)$ ; it contains $B$ . So a maximal abelian subgroup equals $B Z (P)$ and contains $Z (P)$ .

F2algebra

1.2

For $Z (P) \leq A \leq P$ with image $U = A / Z (P)$ : two elements $a, a^{'}$ of $A$ commute exactly when $[a, a^{'}] = e$ , that is exactly when $b_{z} (\overset{ˉ}{a}, {\overset{ˉ}{a}}^{'}) = 0$ ; so $A$ is abelian exactly when $U \leq U^{⊥}$ .

F1L1

1.3

The correspondence $A \mapsto A / Z (P)$ is an inclusion-preserving bijection between the subgroups of $P$ containing $Z (P)$ and the subgroups of $V$ , and $∣ A ∣ = p ∣ A / Z (P) ∣$ by Lagrange.

F2L4L5L6

1.4

If $U \leq U^{⊥}$ then $∣ U ∣^{2} \leq ∣ U ∣ ∣ U^{⊥} ∣ = p^{2 n}$ , so $∣ U ∣ \leq p^{n}$ .

L2L3

1.5

The trivial subgroup satisfies $U \leq U^{⊥}$ , and $V$ is finite, so among the subgroups with $U \leq U^{⊥}$ there is one of largest order, and it is maximal with that property.

2.1

Combining the previous three observations, $A \mapsto A / Z (P)$ carries the maximal abelian subgroups of $P$ bijectively onto the subgroups $U$ of $V$ that are maximal subject to $U \leq U^{⊥}$ .

step 1.1step 1.2step 1.3

2.2

Let $U$ be maximal subject to $U \leq U^{⊥}$ and suppose $U \neq U^{⊥}$ . Pick $v \in U^{⊥}$ with $v \notin U$ and set $U^{'} = ⟨ U, v ⟩$ , whose elements are the products $u v^{a}$ . For such elements, $b_{z} (u v^{a}, u^{'} v^{a^{'}}) = b_{z} (u, u^{'}) + a^{'} b_{z} (u, v) + a b_{z} (v, u^{'}) + a a^{'} b_{z} (v, v) = 0$ , using $U \leq U^{⊥}$ , the choice of $v$ , skew symmetry and alternation. So $U^{'} \leq U^{' ⊥}$ and $U^{'}$ properly contains $U$ , contradicting maximality. Hence $U = U^{⊥}$ and $∣ U ∣^{2} = p^{2 n}$ , so $∣ U ∣ = p^{n}$ .

F1F3L1L3step 1.4

3.1

Therefore maximal abelian subgroups exist, each contains $Z (P)$ , each corresponds to a subgroup $U$ with $U = U^{⊥}$ of order $p^{n}$ , and each has order $p \cdot p^{n} = p^{1 + n}$ .

step 1.5step 2.1step 2.2∎

Remarks

Maximality is under inclusion, not merely maximality of order, and the two agree here only because step 2.2 shows every maximal self-orthogonal subgroup has the same order. That is what makes the conclusion a statement about every maximal abelian subgroup rather than about a largest one.

Depends on

Used by

Dependency tree · two levels

52 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

M. van Beek, Topics in Finite p-Groups, Proposition 2.41(iii) and Theorem 2.40(v) (standard reference, not scraped)
D. A. Craven, The Theory of p-Groups, Lemma 3.12 (standard reference, not scraped)

In an extraspecial pp-group of order p1+2np1+2n every maximal abelian subgroup has order p1+np1+n