mathlib documentation

linear_algebra.clifford_algebra.star

Star structure on clifford_algebra #

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 #

@[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) :
@[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) :

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) :