feat(linear_algebra/clifford_algebra/star): add a possibly-non-canoni…

…cal star structure (#15866)

See the module docstring for a discussion of non-canonicity.

src/linear_algebra/clifford_algebra/equivs.lean

@@ -3,10 +3,11 @@ Copyright (c) 2021 Eric Wieser. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Eric Wieser
 -/
+import algebra.dual_number
 import algebra.quaternion_basis
 import data.complex.module
 import linear_algebra.clifford_algebra.conjugation
-import algebra.dual_number
+import linear_algebra.clifford_algebra.star
 import linear_algebra.quadratic_form.prod
 
 /-!
@@ -46,7 +47,7 @@ is the same as `clifford_algebra.involute`.
 We show additionally that this equivalence sends `quaternion_algebra.conj` to the clifford conjugate
 and vice-versa:
 
-* `clifford_algebra_quaternion.to_quaternion_involute_reverse`
+* `clifford_algebra_quaternion.to_quaternion_star`
 * `clifford_algebra_quaternion.of_quaternion_conj`
 
 ## Dual numbers
@@ -270,11 +271,11 @@ lemma to_quaternion_ι (v : R × R) :
   to_quaternion (ι (Q c₁ c₂) v) = (⟨0, v.1, v.2, 0⟩ : ℍ[R,c₁,c₂]) :=
 clifford_algebra.lift_ι_apply _ _ v
 
-/-- The "clifford conjugate" (aka `involute ∘ reverse = reverse ∘ involute`) maps to the quaternion
-conjugate. -/
-lemma to_quaternion_involute_reverse (c : clifford_algebra (Q c₁ c₂)) :
-  to_quaternion (involute (reverse c)) = quaternion_algebra.conj (to_quaternion c) :=
+/-- The "clifford conjugate" maps to the quaternion conjugate. -/
+lemma to_quaternion_star (c : clifford_algebra (Q c₁ c₂)) :
+  to_quaternion (star c) = quaternion_algebra.conj (to_quaternion c) :=
 begin
+  simp only [clifford_algebra.star_def'],
   induction c using clifford_algebra.induction,
   case h_grade0 : r
   { simp only [reverse.commutes, alg_hom.commutes, quaternion_algebra.coe_algebra_map,
@@ -337,12 +338,11 @@ alg_equiv.of_alg_hom to_quaternion of_quaternion
   to_quaternion_comp_of_quaternion
   of_quaternion_comp_to_quaternion
 
-/-- The quaternion conjugate maps to the "clifford conjugate" (aka
-`involute ∘ reverse = reverse ∘ involute`). -/
+/-- The quaternion conjugate maps to the "clifford conjugate" (aka `star`). -/
 @[simp] lemma of_quaternion_conj (q : ℍ[R,c₁,c₂]) :
-  of_quaternion (q.conj) = (of_quaternion q).reverse.involute :=
+  of_quaternion (q.conj) = star (of_quaternion q) :=
 clifford_algebra_quaternion.equiv.injective $
-  by rw [equiv_apply, equiv_apply, to_quaternion_involute_reverse, to_quaternion_of_quaternion,
+  by rw [equiv_apply, equiv_apply, to_quaternion_star, to_quaternion_of_quaternion,
     to_quaternion_of_quaternion]
 
 -- this name is too short for us to want it visible after `open clifford_algebra_quaternion`

src/linear_algebra/clifford_algebra/star.lean

@@ -0,0 +1,55 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+-/
+import linear_algebra.clifford_algebra.conjugation
+
+/-!
+# 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
+
+* `clifford_algebra.star_ring`
+
+-/
+
+variables {R : Type*} [comm_ring R]
+variables {M : Type*} [add_comm_group M] [module R M]
+variables {Q : quadratic_form R M}
+
+namespace clifford_algebra
+
+instance : star_ring (clifford_algebra Q) :=
+{ star := λ x, reverse (involute x),
+  star_involutive := λ x,
+    by simp only [reverse_involute_commute.eq, reverse_reverse, involute_involute],
+  star_mul := λ x y, by simp only [map_mul, reverse.map_mul],
+  star_add := λ x y, by simp only [map_add] }
+
+lemma star_def (x : clifford_algebra Q) : star x = reverse (involute x) := rfl
+lemma star_def' (x : clifford_algebra Q) : star x = involute (reverse x) := reverse_involute _
+
+@[simp] lemma star_ι (m : M) : star (ι Q m) = -ι Q m :=
+by rw [star_def, involute_ι, map_neg, reverse_ι]
+
+/-- 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] lemma star_smul (r : R) (x : clifford_algebra Q) :
+  star (r • x) = r • star x :=
+by rw [star_def, star_def, map_smul, map_smul]
+
+@[simp] lemma star_algebra_map (r : R) :
+  star (algebra_map R (clifford_algebra Q) r) = algebra_map R (clifford_algebra Q) r :=
+by rw [star_def, involute.commutes, reverse.commutes]
+
+end clifford_algebra