Star structure on clifford_algebra #
THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.
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 clifford_algebra.star_def.
Main definitions #
@[protected, instance]
def
clifford_algebra.star_ring
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M} :
Equations
- clifford_algebra.star_ring = {to_star_semigroup := {to_has_involutive_star := {to_has_star := {star := λ (x : clifford_algebra Q), ⇑clifford_algebra.reverse (⇑clifford_algebra.involute x)}, star_involutive := _}, star_mul := _}, star_add := _}
theorem
clifford_algebra.star_def
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : clifford_algebra Q) :
theorem
clifford_algebra.star_def'
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(x : clifford_algebra Q) :
@[simp]
theorem
clifford_algebra.star_ι
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(m : M) :
has_star.star (⇑(clifford_algebra.ι Q) m) = -⇑(clifford_algebra.ι Q) m
@[simp]
theorem
clifford_algebra.star_smul
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(r : R)
(x : clifford_algebra Q) :
has_star.star (r • x) = r • has_star.star x
Note that this not match the star_smul implied by star_module; 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
clifford_algebra.star_algebra_map
{R : Type u_1}
[comm_ring R]
{M : Type u_2}
[add_comm_group M]
[module R M]
{Q : quadratic_form R M}
(r : R) :
has_star.star (⇑(algebra_map R (clifford_algebra Q)) r) = ⇑(algebra_map R (clifford_algebra Q)) r