Star structure on CliffordAlgebra

This file defines the "clifford conjugation", equal to reverse (involute x), and assigns it the star notation.

This choice is somewhat non-canonical; a star structure is also possible under reverse alone. However, defining it gives us access to constructions like unitary.

Most results about star can be obtained by unfolding it via CliffordAlgebra.star_def.

Main definitions

• CliffordAlgebra.instStarRing

@[instance_reducible]

instance CliffordAlgebra.instStarRing {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} : StarRing (CliffordAlgebra Q)

Equations

• CliffordAlgebra.instStarRing = { star := fun (x : CliffordAlgebra Q) => CliffordAlgebra.reverse (CliffordAlgebra.involute x), star_involutive := ⋯, star_mul := ⋯, star_add := ⋯ }

theorem CliffordAlgebra.star_def {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) : star x = reverse (involute x)

theorem CliffordAlgebra.star_def' {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (x : CliffordAlgebra Q) : star x = involute (reverse x)

@[simp]

theorem CliffordAlgebra.star_ι {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (m : M) : star ((ι Q) m) = -(ι Q) m

@[simp]

theorem CliffordAlgebra.star_smul {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (r : R) (x : CliffordAlgebra Q) : star (r • x) = r • star x

Note that this not match the star_smul implied by StarModule; it certainly could if we also conjugated all the scalars, but there appears to be nothing in the literature that advocates doing this.

@[simp]

theorem CliffordAlgebra.star_algebraMap {R : Type u_1} [CommRing R] {M : Type u_2} [AddCommGroup M] [Module R M] {Q : QuadraticForm R M} (r : R) : star ((algebraMap R (CliffordAlgebra Q)) r) = (algebraMap R (CliffordAlgebra Q)) r