Reversal in three-dimensional Clifford algebras #
In dimension three, an even Clifford element plus its reversal is scalar. Thus every two-by-two matrix model identifies reversal with adjugation and the norm-one equation with determinant one.
theorem
CliffordAlgebra.exists_add_reverseEven_eq_smul_one_of_finrank_eq_three
{K : Type u}
[Field K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(Q : QuadraticForm K V)
(hV : Module.finrank K V = 3)
(x : ↥(even Q))
:
∃ (r : K), x + (reverseEven Q) x = r • 1
In dimension three, every even element plus its reversal is scalar.
theorem
CliffordAlgebra.map_reverseEven_eq_adjugate_of_finrank_eq_three
{K : Type u}
[Field K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(Q : QuadraticForm K V)
(hV : Module.finrank K V = 3)
(e : ↥(even Q) ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)
(x : ↥(even Q))
:
Reversal transported through any two-by-two model is matrix adjugation.
theorem
CliffordAlgebra.map_reverseEven_mul_eq_det_smul_one_of_finrank_eq_three
{K : Type u}
[Field K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(Q : QuadraticForm K V)
(hV : Module.finrank K V = 3)
(e : ↥(even Q) ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)
(x : ↥(even Q))
:
The Clifford norm product maps to the matrix determinant times the identity.
theorem
CliffordAlgebra.reverseEven_mul_eq_one_iff_det_eq_one_of_finrank_eq_three
{K : Type u}
[Field K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(Q : QuadraticForm K V)
(hV : Module.finrank K V = 3)
(e : ↥(even Q) ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)
(x : ↥(even Q))
:
The Clifford norm-one equation is equivalent to determinant one.
theorem
CliffordAlgebra.star_mul_self_eq_one_iff_det_eq_one_of_finrank_eq_three
{K : Type u}
[Field K]
{V : Type v}
[AddCommGroup V]
[Module K V]
(Q : QuadraticForm K V)
(hV : Module.finrank K V = 3)
(e : ↥(even Q) ≃ₐ[K] Matrix (Fin 2) (Fin 2) K)
(x : ↥(even Q))
:
On the even Clifford subalgebra in dimension three, the Clifford star-norm equation is
equivalent to determinant one in any two-by-two matrix model.