Reversal on Clifford subalgebras

This file restricts Clifford reversal to the even subalgebra, records its action on bivectors, develops its naturality under the standard even-algebra equivalences, computes a product of three vectors plus its reversal, and records general reverse-norm identities and comparisons with Clifford conjugation.

def CliffordAlgebra.reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) : ↥(even Q) →ₗ[R] ↥(even Q)

Reversal restricted to the even Clifford subalgebra.

Equations

• CliffordAlgebra.reverseEven Q = CliffordAlgebra.reverse.restrict ⋯

@[simp]

theorem CliffordAlgebra.coe_reverseEven_apply {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : ↥(even Q)) : ↑((reverseEven Q) x) = reverse ↑x

Coercing the restricted reversal agrees with Clifford reversal.

@[simp]

theorem CliffordAlgebra.reverse_eq_star_of_mem_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : ↥(even Q)) : reverse ↑x = star ↑x

On the even Clifford subalgebra, Clifford reversal agrees with Clifford star.

@[simp]

theorem CliffordAlgebra.reverseEven_map_one {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : (reverseEven Q) 1 = 1

Reversal restricted to the even subalgebra fixes its unit.

@[simp]

theorem CliffordAlgebra.reverseEven_algebraMap {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (r : R) : (reverseEven Q) ((algebraMap R ↥(even Q)) r) = (algebraMap R ↥(even Q)) r

Reversal restricted to the even subalgebra fixes scalars.

@[simp]

theorem CliffordAlgebra.reverseEven_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x y : ↥(even Q)) : (reverseEven Q) (x * y) = (reverseEven Q) y * (reverseEven Q) x

Reversal restricted to the even subalgebra reverses products.

@[simp]

theorem CliffordAlgebra.reverseEven_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m₁ m₂ : M) : (reverseEven Q) (((even.ι Q).bilin m₁) m₂) = ((even.ι Q).bilin m₂) m₁

Reversal swaps the two vectors in a bilinear generator of the even Clifford algebra.

@[simp]

theorem CliffordAlgebra.reverseEven_reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : ↥(even Q)) : (reverseEven Q) ((reverseEven Q) x) = x

Reversal restricted to the even subalgebra is an involution.

Naturality

theorem CliffordAlgebra.evenEquivOfIsometry_reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {N : Type u_1} [AddCommGroup N] [Module R N] {P : QuadraticForm R N} (e : QuadraticMap.IsometryEquiv Q P) (x : ↥(even Q)) : (evenEquivOfIsometry e) ((reverseEven Q) x) = (reverseEven P) ((evenEquivOfIsometry e) x)

An isometry-induced equivalence of even Clifford algebras commutes with reversal.

theorem CliffordAlgebra.evenEquivEvenNeg_reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(even Q)) : (evenEquivEvenNeg Q) ((reverseEven Q) x) = (reverseEven (-Q)) ((evenEquivEvenNeg Q) x)

The even-algebra equivalence associated to negating a form commutes with reversal.

theorem CliffordAlgebra.equivEven_symm_reverseEven {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (x : ↥(even (EquivEven.Q' Q))) : (equivEven Q).symm ((reverseEven (EquivEven.Q' Q)) x) = star ((equivEven Q).symm x)

The inverse of the standard even Clifford equivalence sends reversal to star.

Reversal of products of vectors

theorem CliffordAlgebra.ι_mul_ι_mul_ι_add_reverse {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] (Q : QuadraticForm R M) (a b c : M) : (ι Q) a * (ι Q) b * (ι Q) c + reverse ((ι Q) a * (ι Q) b * (ι Q) c) = (ι Q) (QuadraticMap.polar (⇑Q) b c • a - QuadraticMap.polar (⇑Q) a c • b + QuadraticMap.polar (⇑Q) a b • c)

A product of three vectors plus its reversal is a vector, namely polar b c • a - polar a c • b + polar a b • c: reversing the product costs three transpositions of adjacent generators, each of which contributes a polarization term. This is the analogue one degree up of Mathlib's CliffordAlgebra.ι_mul_ι_add_swap.

Reverse norms and comparison with Clifford conjugation

theorem CliffordAlgebra.reverse_prod_map_ι_mul_prod_map_ι {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (l : List M) : reverse (List.map (⇑(ι Q)) l).prod * (List.map (⇑(ι Q)) l).prod = (algebraMap R (CliffordAlgebra Q)) (List.map (⇑Q) l).prod

The reverse norm of a product of vectors is the product of their quadratic norms.

theorem CliffordAlgebra.star_mul_self_eq_reverse_mul_self_of_mem_even {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x ∈ evenOdd Q 0) : star x * x = reverse x * x

On an even element, the star norm and the reverse norm agree.

theorem CliffordAlgebra.star_mul_self_eq_neg_reverse_mul_self_of_mem_odd {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : CliffordAlgebra Q} (hx : x ∈ evenOdd Q 1) : star x * x = -(reverse x * x)

On an odd element, the star norm is the negative of the reverse norm.

theorem CliffordAlgebra.star_mul_self_eq_neg_one_pow_smul_reverse_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (l : List M) : star (List.map (⇑(ι Q)) l).prod * (List.map (⇑(ι Q)) l).prod = (-1) ^ l.length • (reverse (List.map (⇑(ι Q)) l).prod * (List.map (⇑(ι Q)) l).prod)

On a product of r vectors, the star norm is (-1) ^ r times the reverse norm.

theorem CliffordAlgebra.reverse_mul_mul_self_mul {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x y : CliffordAlgebra Q} {r : R} (hx : reverse x * x = (algebraMap R (CliffordAlgebra Q)) r) : reverse (x * y) * (x * y) = (algebraMap R (CliffordAlgebra Q)) r * (reverse y * y)

When the reverse norm of x is the scalar r, the reverse norm of x * y is r times the reverse norm of y.

theorem CliffordAlgebra.self_mul_reverse_of_reverse_mul_self {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} {r : R} (hx : reverse ↑x * ↑x = (algebraMap R (CliffordAlgebra Q)) r) : ↑x * reverse ↑x = (algebraMap R (CliffordAlgebra Q)) r

If the reverse norm of a unit is a scalar, then so is the reverse norm on the other side.

theorem CliffordAlgebra.reverse_inv_mul_inv {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} {x : (CliffordAlgebra Q)ˣ} {r : Rˣ} (hx : reverse ↑x * ↑x = (algebraMap R (CliffordAlgebra Q)) ↑r) : reverse ↑x⁻¹ * ↑x⁻¹ = (algebraMap R (CliffordAlgebra Q)) ↑r⁻¹

If the reverse norm of a unit is the scalar unit r, that of its inverse is r⁻¹.

@[simp]

theorem CliffordAlgebra.reverse_bivector {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (q : QuadraticForm R M) (a b : M) : reverse (bivector q a b) = -bivector q a b

Clifford reversal negates every bivector.

@[simp]

theorem CliffordAlgebra.reverse_bivectorExterior {R : Type u} {M : Type v} [CommRing R] [AddCommGroup M] [Module R M] [Invertible 2] (q : QuadraticForm R M) (x : ↥(⋀[R]^2 M)) : reverse ((bivectorExterior q) x) = -(bivectorExterior q) x

Clifford reversal negates the image of the exterior-square bivector map.