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.
SU(2) to SO(3) as a covering homomorphism
Example
Assume . Identifying with the unit quaternions, conjugation on the imaginary quaternions defines a surjective two-sheeted covering homomorphism
whose kernel is .
Facts & Assumptions
Given: the quaternion basis , with carrying its ordinary Euclidean inner product.
Quaternion multiplication is associative, every nonzero quaternion is invertible, and . The quaternions : real quadruples with componentwise addition and an explicit multiplication formula matching the table on , is a division ring that is not commutative, hence not a field: for , while and .
Regular level sets are embedded submanifolds, and a closed subgroup of a finite-dimensional Lie group has its unique embedded Lie-group structure. A regular level set is an embedded submanifold, Cartan closed subgroup theorem.
A smooth map with invertible differential has a smooth local inverse. The smooth inverse function theorem on manifolds.
Determinants, transposes, and the parametrization of the unit circle are available. For , the determinant over a commutative ring by the Leibniz formula, and for a real matrix, The transpose of a matrix, is a bijection from onto the real unit circle.
is used through the closed-subgroup theorem [F2] that constructs the embedded Lie-group structure on . The Axiom of Countable Choice ().
Verification
Proof technique: explicit quaternion calculation followed by explicit covering sheets.
Write . A coordinate check from [F1] gives and hence . Thus the unit sphere is a group, with inverse . It is a smooth three-manifold by [F2], because is regular: is nonzero on every unit . Multiplication and inversion are polynomial and linear respectively, so this is a Lie group.
The determinant-nonzero matrices form an open subset of the nine-dimensional matrix space. Matrix multiplication is polynomial and inversion is the smooth adjugate-over-determinant formula, so this open manifold is a Lie group. Inside it, the equations and define a closed subgroup; [F2] therefore gives it the embedded Lie-group structure denoted . This is the exact use of in the construction.
For a unit , with , and an imaginary quaternion , direct multiplication gives the vector formula . It also gives zero real part. The identities and show from this formula that . Hence conjugation defines an orthogonal transformation of .
The polynomial map preserves products by the quaternion table. Its image consists exactly of the matrices in , since their columns have the displayed form and the unitary and determinant-one equations reduce to . It and its coordinate inverse are smooth, so it identifies the Lie group of step 1.1 with .
The unit sphere is path connected: if , normalize the nonzero segment , while is joined to by . Consequently the determinant of the orthogonal map in step 1.3, a continuous function with values in , equals its value at . Thus . Associativity gives , and the coordinate formula in step 1.3 makes smooth.
Identify with . Differentiating conjugation along gives . Differentiating at shows that is contained in the three-dimensional space of skew-symmetric endomorphisms. The displayed cross-product map takes values in that space and is injective: if for every , take a basis vector not parallel to nonzero to get a contradiction. Its three-dimensional image lies in , so the inclusions force to be the full skew-symmetric space and to be an isomorphism. By [F3], there are neighborhoods of and of such that is a diffeomorphism. Choose a smaller open neighborhood with and put ; the restriction remains a diffeomorphism and is open.
The map is onto. For , , so . Choose a unit vector fixed by . Its perpendicular plane is invariant, and the restriction of there is an orientation-preserving planar orthogonal map. By [F4], in a positively oriented orthonormal basis it is rotation through some angle . Substituting into the formula of step 1.3 gives Rodrigues' formula, so . Only this one finite-dimensional choice of an axis and basis is made.
If is the identity, then commutes with . Comparing with first gives , and comparing with then gives . Since is unit, or . Conversely both real unit quaternions act trivially. Therefore , and every fibre is exactly .
Step 3.2 now gives , and both restrictions are diffeomorphisms onto . For arbitrary choose one above it using step 3.1; then is evenly covered by the two translated sheets and . Hence is a covering homomorphism in the sense of Covering homomorphisms of Lie groups, with exactly two sheets. The groups are nonempty and three-dimensional; no zero-dimensional, endpoint, degenerate, or biconditional case is hidden. The proof itself makes only finitely many choices, while is used through the closed-subgroup construction of in [F2].
Depends on
- The Axiom of Countable Choice ($\mathrm{AC}_\omega$)
- Covering homomorphisms of Lie groups
- The quaternions $\mathbb{H}$: real quadruples with componentwise addition and an explicit multiplication formula matching the table on $1, i, j, k$
- $\mathbb{H}$ is a division ring that is not commutative, hence not a field: $q^{-1} = \bar q / N(q)$ for $q \ne 0$, while $ij = k$ and $ji = -k$
- A regular level set is an embedded submanifold
- Cartan closed subgroup theorem
- The smooth inverse function theorem on manifolds
- For $n\ge1$, the determinant over a commutative ring by the Leibniz formula, and $|\det A|$ for a real matrix
- The transpose $A^{\mathsf T}$ of a matrix
- $t\mapsto(\cos t,\sin t)$ is a bijection from $[0,2\pi)$ onto the real unit circle
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
66 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
- Pavel Etingof, MIT 18.745 Lie Groups and Lie Algebras I (standard reference, not scraped)
- Anthony W. Knapp, Lie Groups Beyond an Introduction, 2nd ed. (standard reference, not scraped)