LemmaStatement: Literature-sourcedProof: AI-adaptedprecheck 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.

$Q_{8} \circ Q_{8} ≅ Dih (C_{4}) \circ Dih (C_{4})$

Statement

Let $E = Q_{8} \circ Q_{8}$ be the central product of two copies of the quaternion group along the unique isomorphism between their centres. Then $E$ is also an internal central product of two subgroups isomorphic to $Dih (C_{4})$ meeting in $Z (E)$ , and therefore

$Q_{8} \circ Q_{8} ≅ Dih (C_{4}) \circ Dih (C_{4}) .$

Facts & Assumptions

Given: Two copies $E_{1}, E_{2}$ of $Q_{8}$ , the central product $E = E_{1} \circ_{α} E_{2}$ along the unique isomorphism $α$ of their centres, the canonical images $x_{1}, y_{1}$ of the generators $i, j$ of $E_{1}$ and $x_{2}, y_{2}$ of those of $E_{2}$ , and the common central image $z$ , so that $x_{i}^{2} = y_{i}^{2} = z$ , $z^{2} = 1$ and $y_{i} x_{i} y_{i}^{- 1} = x_{i}^{- 1}$ .

[F1]

For groups $G, H$ with central subgroups $Z_{1} \leq Z (G)$ , $Z_{2} \leq Z (H)$ and an isomorphism $α : Z_{1} \to Z_{2}$ , the central product $G \circ_{α} H$ is the quotient of $G \times H$ by $N = {(z, α (z)^{- 1}) : z \in Z_{1}}$ (The central product $G \circ_{α} H$ of two groups along an isomorphism of central subgroups).

[F2]

Subgroups $G_{1}, \dots, G_{r}$ of $G$ form an internal central product when they generate $G$ and $[G_{i}, G_{j}] = 1$ for $i \neq j$ (Internal central products of a finite family of subgroups).

[F3]

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

[F4]

$ord (g)$ is the least $k \geq 1$ with $g^{k} = e$ (The order $∣ G ∣$ of a finite group and the order $ord (g)$ of an element, with $ord (g) = \infty$ when no positive power of $g$ is the identity).

[L1]

$Q_{8} = {1, - 1, i, - i, j, - j, k, - k}$ with $i^{2} = j^{2} = - 1$ and $j i = - k = i^{- 1} j$ (The quaternion group $Q_{8} = {\pm 1, \pm i, \pm j, \pm k}$ inside the nonzero quaternions, The quaternions $H$ : real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$ ).

[L2]

$∣ Q_{8} ∣ = 8$ , the element $- 1$ is its only element of order two, and each of $\pm i, \pm j, \pm k$ has order four ( $Q_{8}$ is a subgroup of $H^{\times}$ with eight elements, and $- 1$ is its only element of order $2$ ).

[L3]

$Dih (C_{4})$ and $Q_{8}$ are extraspecial of order eight ( $Dih (C_{4})$ and $Q_{8}$ are extraspecial of order $8$ , with six and two solutions of $x^{2} = 1$ respectively).

[L4]

The canonical maps into a central product are injective homomorphisms whose images commute elementwise, generate the product, and meet in the image of the identified subgroup (The two canonical maps into a central product are injective homomorphisms whose images commute, generate it, and meet in the identified centre).

[L5]

A central product of two extraspecial $p$ -groups identified along their centres is extraspecial of order $∣ E_{1} ∣ ∣ E_{2} ∣ / p$ (A central product of extraspecial $p$ -groups identified along their centres is extraspecial).

[L6]

Subgroups form an internal central product of $G$ if and only if the multiplication map from their direct product is a surjective homomorphism; for two factors $G ≅ G_{1} \circ_{id} G_{2}$ along the identity of $G_{1} \cap G_{2}$ (Internal central products are the images of external ones).

[L7]

For $n \geq 1$ , $Dih (C_{n}) = C_{n} ⋊ C_{2}$ with $r^{n} = s^{2} = 1$ and $s r s^{- 1} = r^{- 1}$ , of order $2 n$ ( $Dih (C_{n}) = C_{n} ⋊ C_{2}$ with inversion action has order $2 n$ and the dihedral relations).

[L8]

The conditions $N ⊴ G$ , $G = N H$ , $N \cap H = {1}$ hold if and only if conjugation restricts to an action and $(n, h) \mapsto n h$ is an isomorphism $N ⋊_{α} H \to G$ ( Recognition theorem: $G = N H$ with $N ⊴ G$ , $N \cap H = 1$ exactly realises an external semidirect product).

[L9]

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

Proof

technique · direct

1.1F1L2L3L4L5

The two canonical images are isomorphic copies of $Q_{8}$ that commute elementwise, generate $E$ , and meet exactly in $⟨ z ⟩$ ; and $E$ is extraspecial of order $8 \cdot 8 / 2 = 32$ .

1.2F4L1L2

Each $x_{i}$ has order four, since $x_{i}^{2} = z$ and $z^{2} = 1$ with $z \neq 1$ ; likewise each $y_{i}$ .

2.1L1L4step 1.1step 1.2

Put $t_{1} = x_{2} y_{1}$ and $t_{2} = x_{1} y_{2}$ . Then $t_{1}^{2} = x_{2} y_{1} x_{2} y_{1} = x_{2}^{2} y_{1}^{2} = z \cdot z = 1$ , because $x_{2}$ commutes with $y_{1}$ ; likewise $t_{2}^{2} = 1$ .

2.2L1L4step 1.1

Also $t_{1} x_{1} t_{1}^{- 1} = x_{2} (y_{1} x_{1} y_{1}^{- 1}) x_{2}^{- 1} = y_{1} x_{1} y_{1}^{- 1} = x_{1}^{- 1}$ , because $x_{2}$ commutes with everything in the first image; likewise $t_{2} x_{2} t_{2}^{- 1} = x_{2}^{- 1}$ .

2.3F3L4step 1.1step 1.2

Neither $t_{1}$ lies in $⟨ x_{1} ⟩$ nor $t_{2}$ in $⟨ x_{2} ⟩$ : if $x_{2} y_{1}$ were a power of $x_{1}$ then $x_{2}$ would lie in the first canonical image, hence in $⟨ z ⟩$ , contradicting that $x_{2}$ has order four.

3.1F3L7L8L9step 2.1step 2.2step 2.3

Set $H_{1} = ⟨ x_{1}, t_{1} ⟩$ and $H_{2} = ⟨ x_{2}, t_{2} ⟩$ . In $H_{1}$ the cyclic subgroup $⟨ x_{1} ⟩$ of order four is normalised by $t_{1}$ and meets $⟨ t_{1} ⟩$ trivially, and $∣ ⟨ x_{1} ⟩ ∣ ∣ ⟨ t_{1} ⟩ ∣ = 8$ ; so $H_{1}$ is the internal semidirect product of a cyclic group of order four by a group of order two acting by inversion, that is $H_{1} ≅ Dih (C_{4})$ of order eight with $Z (H_{1}) = ⟨ x_{1}^{2} ⟩ = ⟨ z ⟩$ . The same holds for $H_{2}$ .

4.1F2F3L1L4step 1.1step 3.1

The four generators commute in pairs across the two subgroups: $x_{1}$ commutes with $x_{2}$ and with $t_{2} = x_{1} y_{2}$ ; $t_{1} = x_{2} y_{1}$ commutes with $x_{2}$ ; and $t_{1} t_{2} = x_{2} (y_{1} x_{1}) y_{2} = x_{1}^{- 1} x_{2} y_{1} y_{2}$ while $t_{2} t_{1} = x_{1} (y_{2} x_{2}) y_{1} = x_{2}^{- 1} x_{1} y_{1} y_{2}$ , and these agree because $x_{1}^{2} = z = x_{2}^{2}$ gives $x_{1}^{- 1} x_{2} = x_{2}^{- 1} x_{1}$ . Hence $[H_{1}, H_{2}] = 1$ .

4.2F3L4step 1.1step 3.1

The two subgroups generate $E$ : they contain $x_{1}, x_{2}, t_{1}, t_{2}$ , hence $y_{1} = x_{2}^{- 1} t_{1}$ and $y_{2} = x_{1}^{- 1} t_{2}$ , hence both canonical images, which generate $E$ .

5.1F2L6L9step 1.1step 3.1step 4.1step 4.2

So $H_{1}$ and $H_{2}$ form an internal central product of $E$ , and the recognition theorem gives $E ≅ H_{1} \circ_{id} H_{2}$ along the identity of $D = H_{1} \cap H_{2}$ . Comparing orders, $32 = ∣ E ∣ = 8 \cdot 8 / ∣ D ∣$ , so $∣ D ∣ = 2$ and $D = ⟨ z ⟩ = Z (H_{1}) = Z (H_{2})$ .

6.1F1L3step 3.1step 5.1∎

Since $H_{1}$ and $H_{2}$ are isomorphic to $Dih (C_{4})$ by isomorphisms carrying $D$ to the centre, $E$ is a central product of two copies of $Dih (C_{4})$ along the unique isomorphism of their centres, which is what was claimed.

Remarks

The identity $x_{1}^{2} = x_{2}^{2}$ is the whole of the computation in step 4.1, and it is where the quaternion hypothesis is spent: in a central product of two dihedral groups the corresponding squares are both trivial and the same computation succeeds for a different reason. What the statement records is that these two central products are the same group, so the number of quaternion factors in a decomposition is not an invariant of it.

Depends on

Used by

Dependency tree · two levels

70 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.13(i) (standard reference, not scraped)
M. van Beek, Topics in Finite p-Groups, Exercise 2.37 (standard reference, not scraped)

Q8∘Q8≅Dih⁡(C4)∘Dih⁡(C4)Q8​∘Q8​≅Dih(C4​)∘Dih(C4​)