CorollaryStatement: AI-adaptedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 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.

The centre of an extraspecial $p$ -group has no complement

Statement

Let $P$ be an extraspecial $p$ -group. Then $Z (P)$ has no complement in $P$ : there is no subgroup $H \leq P$ with $P = Z (P) H$ and $Z (P) \cap H = 1$ .

Facts & Assumptions

Given: An extraspecial $p$ -group $P$ (Special and extraspecial $p$ -groups).

[F1]

For subgroups $N, H$ of $G$ with $N ⊴ G$ , $G = N H$ and $N \cap H = {1}$ , the group $G$ is the internal semidirect product of $N$ by $H$ , and $H$ is called a complement to $N$ in $G$ (An internal semidirect product and a complement to a normal subgroup).

[F2]

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

[L1]

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

[L2]

For every homomorphism $f : G \to H$ , the rule $g \ker f \mapsto f (g)$ is an isomorphism from $G / \ker f$ onto $im f$ (First isomorphism theorem for groups: $G / \ker f ≅ im f$ ).

[L3]

An elementary abelian $p$ -group is a finite abelian $p$ -group in which every nonidentity element has order $p$ (Elementary abelian $p$ -groups).

Proof

technique · contradiction

1.1F1L1assume-contra

Suppose $H \leq P$ is a complement to $Z (P)$ , so that $P = Z (P) H$ and $Z (P) \cap H = 1$ ; the centre is normal, so the quotient $P / Z (P)$ is defined.

2.1L2step 1.1

Let $π : P \to P / Z (P)$ be the quotient map and restrict it to $H$ . Its kernel is $H \cap Z (P) = 1$ , and its image is all of $P / Z (P)$ because every $g \in P$ is $z h$ with $z \in Z (P)$ and $h \in H$ , whence $π (g) = π (h)$ ; so $H ≅ P / Z (P)$ .

3.1L1L3step 2.1

The quotient $P / Z (P)$ is elementary abelian, hence abelian, so $H$ is abelian.

4.1F2step 1.1step 3.1discharge-contradiction∎

Every element of $P$ is $z h$ with $z$ central and $h \in H$ , and $(z_{1} h_{1}) (z_{2} h_{2}) = z_{1} z_{2} h_{1} h_{2} = z_{2} z_{1} h_{2} h_{1} = (z_{2} h_{2}) (z_{1} h_{1})$ , so $P$ is abelian; this contradicts the nonabelianness of an extraspecial group.

Remarks

The argument uses no bound on the order of $P$ , so the conclusion holds for every extraspecial group and not only for those of order $p^{3}$ . What fails is not that a complement is hard to find but that its existence would make the group abelian, which the definition forbids.

Depends on

Used by

FALSE: the centre of an extraspecial p-group has a complement False statement

Dependency tree · two levels

28 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.32(ii) (standard reference, not scraped)

The centre of an extraspecial pp-group has no complement