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 #
instance
CliffordAlgebra.instStarRing
{R : Type u_1}
[CommRing R]
{M : Type u_2}
[AddCommGroup M]
[Module R M]
{Q : QuadraticForm R M}
:
Equations
- CliffordAlgebra.instStarRing = StarRing.mk ⋯
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)
:
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)
:
@[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 ((CliffordAlgebra.ι Q) m) = -(CliffordAlgebra.ι 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)
:
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