Reversal on odd elements in dimension at most four #
Reversal fixes every vector and, up to a vector, negates every product of three vectors
(CliffordAlgebra.ι_mul_ι_mul_ι_add_reverse in
TauCeti/LinearAlgebra/CliffordAlgebra/Reversal/Basic.lean). In dimension at most four the odd
part of the Clifford algebra is spanned by the vectors and the products of three vectors, so for
every odd element y the sum y + reverse y is a vector, and an odd element fixed by reversal is
a vector as soon as 2 is invertible.
This is the odd counterpart of TauCeti/LinearAlgebra/CliffordAlgebra/Reversal/Three.lean, where
an even element plus its reversal is a scalar in dimension three. Its use is the low-dimensional
identification of Spin groups: an even unit x with reverse x * x = 1 sends a vector ι v to
the odd element x * ι v * reverse x, which reversal fixes, so in dimension at most four it is a
vector again. The bound is sharp: in dimension five the odd part also contains the volume element,
which reversal fixes.
Main results #
CliffordAlgebra.add_reverse_mem_range_ι_of_mem_evenOdd_one_of_finrank_le_four: in dimension at most four, an odd element plus its reversal is a vector.CliffordAlgebra.mem_range_ι_of_mem_evenOdd_one_of_reverse_eq_of_finrank_le_four: in dimension at most four, an odd element fixed by reversal is a vector.
References #
- H. B. Lawson and M.-L. Michelsohn, Spin Geometry (1989), Chapter I, §2.
In dimension at most four, an odd element plus its reversal is a vector. The odd part is then spanned by the vectors and the products of three vectors, and reversal fixes the former and negates the latter up to a vector.
In dimension at most four, an odd element fixed by reversal is a vector.