feat: port LinearAlgebra.CliffordAlgebra.Star (#5405)

Co-authored-by: Jeremy Tan Jie Rui <reddeloostw@gmail.com>

Mathlib.lean

@@ -2000,6 +2000,7 @@ import Mathlib.LinearAlgebra.Charpoly.ToMatrix
 import Mathlib.LinearAlgebra.CliffordAlgebra.Basic
 import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
 import Mathlib.LinearAlgebra.CliffordAlgebra.Grading
+import Mathlib.LinearAlgebra.CliffordAlgebra.Star
 import Mathlib.LinearAlgebra.Coevaluation
 import Mathlib.LinearAlgebra.Contraction
 import Mathlib.LinearAlgebra.CrossProduct

Mathlib/LinearAlgebra/CliffordAlgebra/Star.lean

@@ -0,0 +1,75 @@
+/-
+Copyright (c) 2022 Eric Wieser. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Eric Wieser
+
+! This file was ported from Lean 3 source module linear_algebra.clifford_algebra.star
+! leanprover-community/mathlib commit 4d66277cfec381260ba05c68f9ae6ce2a118031d
+! Please do not edit these lines, except to modify the commit id
+! if you have ported upstream changes.
+-/
+import Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
+
+/-!
+# 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
+
+* `clifford_algebra.star_ring`
+
+-/
+
+
+variable {R : Type _} [CommRing R]
+
+variable {M : Type _} [AddCommGroup M] [Module R M]
+
+variable {Q : QuadraticForm R M}
+
+namespace CliffordAlgebra
+
+instance : StarRing (CliffordAlgebra Q) where
+  -- porting note: cannot infer `Q`
+  star x := reverse (Q := Q) (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]
+
+-- porting note: cannot infer `Q`
+theorem star_def (x : CliffordAlgebra Q) : star x = reverse (Q := Q) (involute x) :=
+  rfl
+#align clifford_algebra.star_def CliffordAlgebra.star_def
+
+-- porting note: cannot infer `Q`
+theorem star_def' (x : CliffordAlgebra Q) : star x = involute (reverse (Q := Q) x) :=
+  reverse_involute _
+#align clifford_algebra.star_def' CliffordAlgebra.star_def'
+
+@[simp]
+theorem star_ι (m : M) : star (ι Q m) = -ι Q m := by rw [star_def, involute_ι, map_neg, reverse_ι]
+#align clifford_algebra.star_ι CliffordAlgebra.star_ι
+
+/-- 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 star_smul (r : R) (x : CliffordAlgebra Q) : star (r • x) = r • star x := by
+  rw [star_def, star_def, map_smul, map_smul]
+#align clifford_algebra.star_smul CliffordAlgebra.star_smul
+
+@[simp]
+theorem star_algebraMap (r : R) :
+    star (algebraMap R (CliffordAlgebra Q) r) = algebraMap R (CliffordAlgebra Q) r := by
+  rw [star_def, involute.commutes, reverse.commutes]
+#align clifford_algebra.star_algebra_map CliffordAlgebra.star_algebraMap
+
+end CliffordAlgebra