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.
Normalized Pin products and Clifford norm
Statement
Let , Pin, , , and have the definitions in Real Clifford group, Pin, and the two Spin subgroups and Clifford involutions and the norm of a vector product. Then is scalar-valued and multiplicative on . For with anisotropic ,
Pin is exactly . If , it is the subgroup generated by vectors and consists of normalized anisotropic-vector products; its even part consists of the even products and is . For , . In every dimension, is the norm-one subgroup of the full even group.
Facts & Assumptions
Given: The real quadratic space and group definitions above.
The norm of a product of anisotropic vectors is the product of the scalar norms (Clifford involutions and the norm of a vector product).
In positive dimension, Pin is generated by vectors with ; in dimension zero, Pin is . Full Spin is its even subgroup (Real Clifford group, Pin, and the two Spin subgroups).
is a group acting orthogonally; an anisotropic vector acts by its reflection. The action has scalar kernel and every element of is scalar times a product of anisotropic vectors (Twisted Clifford action, reflections, and scalar kernel).
Every orthogonal map factors into anisotropic reflections (Cartan–Dieudonné factorization over a real quadratic space).
Proof
For a vector product, [F1] makes a real scalar. By [F3], every is for and anisotropic ; , so is scalar. For scalar-valued norms, , which proves multiplicativity.
The empty product has norm . Every normalized vector belongs to by [F3], has inverse , and has norm . Thus subgroup words are normalized-vector products, and multiplicativity in step 1.1 shows that they have norm . In dimension zero Pin is , and both scalars belong to and have norm . Hence Pin is contained in the asserted norm locus in every dimension.
Conversely, take with . By [F4], factor into reflections and lift them by normalized vectors to a product with . By [F3], is a nonzero scalar, and step 1.1 gives . Since both norms are and , , so . If , is itself a product of normalized vectors: for , , and for , . If , it is included by definition. Thus every norm- element lies in Pin.
The grading parity of a vector product is its number of factors modulo two, and nonzero scalars are even. In positive dimension, the even elements of Pin are therefore exactly the even normalized products, which are by [F2]. In dimension zero every Clifford element is scalar by [F3], so both signs are even and have norm , giving all three groups . In every dimension the definition of selects the norm-one subgroup; multiplicativity in step 1.1 ensures that it is a subgroup.
Remarks
The norm of an even product can be in mixed signature; “full even Spin” and “norm-one Spin” are intentionally distinct definitions.
Depends on
Used by
- Euclidean Spin is the universal cover of SO(n) for n at least three Corollary
- A mixed-sign even lift has norm minus one Example
- Pin lift squares and the Spin(2) double-angle map Example
- The split even Clifford algebra in signature (1,1) Example
- Euclidean Spin sphere bundle and explicit rotor sections Lemma
- Local Spin lift from the matrix logarithm Lemma
- The even Clifford norm detects the identity component in mixed signature Lemma
- Complex spinor modules and complete reducibility for Euclidean Spin Theorem
- Pin and full-even Spin are topological double covers Theorem
- Real Pin and full-even Spin images, kernels, and definite compactness Theorem
- Real Spin modules from the even Clifford algebra Theorem
Cited to discharge well-definedness by Real Clifford group, Pin, and the two Spin subgroups.
Dependency tree · two levels
8 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.3–1.4 (standard reference, not scraped)
- Eckhard Meinrenken, Lie groups and Clifford algebras, Chapter 2 §4.1 (standard reference, not scraped)