Spin lifts of Eichler transvections #
Let u be an isotropic vector of a quadratic form Q and w a vector orthogonal to it. The
Eichler transvection E_{u,w} (QuadraticMap.transvection) is a proper isometry of Q. It has a
canonical lift to the Spin group, written down inside the even Clifford algebra:
L_{u,w} = 1 + ι w * ι u.
Since u is isotropic and orthogonal to w, the element ι w * ι u squares to zero, so
L_{u,w} is a unit with inverse 1 - ι w * ι u. Conjugation by it is exactly E_{u,w} on the
vectors, with no sign. Moreover w ↦ L_{u,w} turns addition into multiplication and kills
K ∙ u. So the lifts form a homomorphism from the additive group of u^⊥ / K ∙ u into the Spin
group, lifting QuadraticMap.transvectionHom along CliffordAlgebra.spinToSpecialOrthogonal.
These form a unipotent subgroup of the Spin group. In particular every Eichler
transvection lies in the image of Spin, so its spinor norm is trivial.
The lift is stated over a field with 2 invertible and for a nondegenerate form, with no finite
dimensionality assumed except for the spinor-norm corollaries. Nondegeneracy is what puts
1 + ι w * ι u in Mathlib's lipschitzGroup, which is generated by the vectors of invertible
norm. It cannot be dropped: for Q = 0 the Lipschitz group is trivial, while 1 + ι w * ι u is a
nontrivial unit as soon as u and w are linearly independent.
Main definitions #
CliffordAlgebra.spinTransvection hQ hu huw: the Spin element1 + ι w * ι uliftingE_{u,w}.CliffordAlgebra.transvectionLiftHom hQ hu: the homomorphismw ↦ L_{u,w}from the additive group ofu^⊥ / K ∙ uinto the Spin group.
Main results #
CliffordAlgebra.coe_spinToSpecialOrthogonal_spinTransvection: the lift acts on the quadratic space as the Eichler transvectionE_{u,w}.CliffordAlgebra.spinTransvection_add:L_{u,w + w'} = L_{u,w} * L_{u,w'}.QuadraticMap.Isometry.spinGroupMap_spinTransvectionandQuadraticMap.IsometryEquiv.spinGroupEquiv_spinTransvection: the canonical lifts are natural under isometries, in general map form and equivalence-specialized form.QuadraticMap.IsometryEquiv.spinGroupEquiv_comp_transvectionLiftHom: the Spin root-subgroup homomorphisms are natural under isometric equivalences.CliffordAlgebra.spinTransvection_eq_one_iff: foru ≠ 0,L_{u,w} = 1exactly whenw ∈ K ∙ u.CliffordAlgebra.spinToSpecialOrthogonal_comp_transvectionLiftHom: the lifts liftQuadraticMap.transvectionHom.CliffordAlgebra.spinTransvection_pow: powers multiply the parameter by the exponent, as forTauCeti.QuadraticMap.transvection_pow.CliffordAlgebra.transvectionLiftHom_injective: foru ≠ 0the lifts form a copy ofu^⊥ / K ∙ uinside the Spin group.CliffordAlgebra.spinorNorm_transvectionandCliffordAlgebra.orthogonalSpinorNorm_transvection: Eichler transvections have trivial spinor norm.
References #
- M. Eichler, Quadratische Formen und orthogonale Gruppen, Springer (1952).
The canonical Spin lift of an Eichler transvection: for an isotropic vector u and a
vector w orthogonal to it, the element L_{u,w} = 1 + ι w * ι u of the Spin group of a
nondegenerate form. It acts on the quadratic space as the Eichler transvection E_{u,w}
(coe_spinToSpecialOrthogonal_spinTransvection).
Instances For
The Spin lift of E_{u,w} is the Clifford element 1 + ι w * ι u.
The Spin-group map induced by an isometry transports the canonical lift of an Eichler transvection, provided both quadratic forms are nondegenerate.
Transporting the canonical Spin lift of an Eichler transvection along an isometric equivalence transports both of its defining vectors.
The Spin lifts of the Eichler transvections with a fixed isotropic vector u compose
additively in w.
The Spin lift of E_{u,w} is trivial when w is a multiple of u.
The inverse of the Spin lift of E_{u,w} is the Spin lift of E_{u,-w}.
The Spin lift of E_{u,w} depends on w only through its class modulo K ∙ u.
The Spin lift of E_{u,w} acts on the quadratic space as E_{u,w}.
The Spin lift of E_{u,w} maps to E_{u,w} in SO(Q).
For u ≠ 0, the Spin lift of E_{u,w} is trivial exactly when w is a multiple of u.
The Spin lifts of the Eichler transvections with a fixed isotropic vector u, as a
homomorphism w ↦ L_{u,w} from the additive group of u^⊥ / K ∙ u into the Spin group. It lifts
QuadraticMap.transvectionHom (spinToSpecialOrthogonal_comp_transvectionLiftHom) and is
injective for u ≠ 0 (transvectionLiftHom_injective).
Instances For
The quotient homomorphism sends the class of w to the Spin lift L_{u,w}.
Spin root-subgroup homomorphisms are natural under isometric equivalences of quadratic forms.
The Spin lifts lift the Eichler transvections: followed by the projection
Spin(Q) → SO(Q), the homomorphism w ↦ L_{u,w} is w ↦ E_{u,w}.
For u ≠ 0, the Spin lifts of the Eichler transvections with isotropic vector u form a copy
of the additive group u^⊥ / K ∙ u inside the Spin group.
The nth power of a canonical Spin transvection lift multiplies its parameter by n.
An Eichler transvection has trivial spinor norm: it is the image of its Spin lift.
An Eichler transvection has trivial spinor norm as an element of O(Q).