CorollaryStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck pass

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.

Euclidean Spin is the universal cover of SO(n) for n at least three

Statement

Assume the Axiom of Choice. For every integer $n \geq 3$ , the connected double cover ${Spin}_{f u l l} (n) \to S O (n)$ from Pin and full-even Spin are topological double covers has simply connected total space and is the universal covering group of $S O (n)$ . The proof uses the explicit locally trivial sphere bundle

$Spin (n - 1) ⟶ Spin (n) \overset{x \mapsto ρ_{x} (e_{n})}{\to} S^{n - 1}$

from Euclidean Spin sphere bundle and explicit rotor sections. No universal-cover assertion is made for $n = 1$ or $n = 2$ .

Facts & Assumptions

Given: Euclidean $V = R^{n}$ with its positive Clifford convention, the Axiom of Choice, and the group maps above.

[F1]

$Spin (n) \to S O (n)$ is a two-sheeted covering, and $S O (n)$ is connected (Pin and full-even Spin are topological double covers, The even Clifford norm detects the identity component in mixed signature).

[F2]

The sphere projection has explicit local product charts and a finite partition of unity subordinate to those charts (Euclidean Spin sphere bundle and explicit rotor sections).

[F3]

Under AC, a numerable fiber bundle is a Hurewicz fibration (Numerable fiber bundles are hurewicz fibrations). The AC hypothesis in this supplier is used to well-order finite chart words in its lifting construction.

[F4]

For a based Serre fibration, the homotopy groups of the fiber, total space, and base form an exact sequence (Long exact sequence of homotopy groups of a fibration).

[F5]

$S^{m}$ is simply connected for every $m \geq 2$ ( $S^{n}$ is simply connected for every $n \geq 2$ ).

[F6]

Full-even Spin elements are even products of unit vectors, with $- 1$ included (Normalized Pin products and Clifford norm).

[F7]

The orthogonal square-free monomials form a basis of the Clifford algebra (PBW basis and exterior associated graded for a Clifford algebra).

[A1]

Assume AC; it is used only in step 3.1 through the numerable-bundle-to-fibration supplier [F3] (The Axiom of Choice).

Proof

technique · induction

1.1givenF6construct

For every $n \geq 2$ , $Spin (n)$ is path connected. By [F6], each element is a product of an even number of unit vectors, possibly multiplied by $- 1$ . The unit sphere $S^{n - 1}$ is path connected: non-antipodal points join by a great-circle arc, and antipodal points join by two such arcs through a third point. For each pair of unit factors choose paths from a fixed unit vector $e_{1}$ to the two factors and multiply the two paths; at the initial endpoint their product is $e_{1}^{2} = 1$ . Concatenating these paths joins $1$ to the product. The remaining scalar $- 1$ joins to $1$ along $t \mapsto \cos (π t) + e_{1} e_{2} \sin (π t)$ . It lies in full-even Spin because $\cos (π t) + e_{1} e_{2} \sin (π t) = e_{1} (\cos (π t) e_{1} + \sin (π t) e_{2}),$ and both factors are unit vectors; the path starts at $1$ and ends at $- 1$ .

2.1F5F6F7step 1.1constructbase

In dimension $3$ , [F7] gives basis $1, e_{1} e_{2}, e_{2} e_{3}, e_{3} e_{1}$ for ${C l}_{3, 0}^{0}$ . Direct multiplication gives the quaternion relations, Clifford conjugation negates each bivector, and hence $N (a + b_{1} e_{1} e_{2} + b_{2} e_{2} e_{3} + b_{3} e_{3} e_{1}) = a^{2} + b_{1}^{2} + b_{2}^{2} + b_{3}^{2}$ . A bivector $b = b_{1} e_{2} e_{3} + b_{2} e_{3} e_{1} + b_{3} e_{1} e_{2}$ corresponds to the vector $b_{1} e_{1} + b_{2} e_{2} + b_{3} e_{3}$ under the three-dimensional Hodge star; choosing an oriented orthonormal basis in its perpendicular plane gives $b = β u w$ with $u, w$ orthonormal and $β = \sqrt{b_{1}^{2} + b_{2}^{2} + b_{3}^{2}}$ . If $a^{2} + β^{2} = 1$ , the vector $v = a u + β w$ is unit and $u v = a + b$ . For $b = 0$ , the elements $\pm 1$ are the empty product and a product $u (- u)$ . Thus every unit quaternion is in Spin, and every Spin element has norm one, so $Spin (3) = S^{3}$ . By [F5], this group is simply connected.

3.1A1F2F3F4F5step 1.1step 2.1ih

For $n \geq 4$ , the sphere bundle in [F2] has a finite subordinate partition of unity, so it is numerable; [F3] and [A1] make it a Hurewicz, hence Serre, fibration. Its fiber is $Spin (n - 1)$ and its base is $S^{n - 1}$ . By the induction hypothesis the fiber is simply connected, and [F5] makes the base simply connected. The exact segment $π_{1} (Spin (n - 1)) \to π_{1} (Spin (n)) \to π_{1} (S^{n - 1})$ from [F4] therefore forces $π_{1} (Spin (n)) = 0$ . Step 1.1 gives path connectedness, so Spin $(n)$ is simply connected for all $n \geq 3$ .

4.1A1F1step 1.1step 2.1step 3.1discharge-induction∎

By [F1], Spin $(n) \to S O (n)$ is a connected covering with connected simply connected total space. By definition this is the universal covering space; since the map is a group homomorphism, it is the universal covering group. The induction begins at $n = 3$ in step 2.1 and proceeds by step 3.1, with the exact choice use recorded in [A1].

Remarks

The proof carries AC because it uses the published general theorem that numerable bundles are Hurewicz fibrations. The group-theoretic factorization and the explicit finite partition of unity use no choice axiom. Spin $(2) ≅ S^{1}$ is a nontrivial double cover of $S O (2) ≅ S^{1}$ , not a universal cover; its direct calculation is on the B page.

Depends on

Used by

Spin structures exist exactly when w2 vanishes and then form an H1 torsor Lemma

Dependency tree · two levels

41 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

Jean Gallier, Clifford Algebras, Clifford Groups, and a Generalization of the Quaternions: The Pin and Spin Groups, §1.8 (standard reference, not scraped)
Konstantin Wernli, Lecture Notes on Spin Geometry, §1.5.3, pp. 29–31 (standard reference, not scraped)