feat(star/basic): add a star_monoid (units R) instance (#9681)

This also moves all the `opposite R` instances to be adjacent, and add some missing `star_module` definitions.

src/algebra/star/basic.lean

@@ -11,6 +11,7 @@ import algebra.group_power.lemmas
 import algebra.field_power
 import data.equiv.ring_aut
 import data.equiv.mul_add_aut
+import group_theory.group_action.units
 
 /-!
 # Star monoids, rings, and modules
@@ -50,12 +51,6 @@ A star operation (e.g. complex conjugate).
 -/
 add_decl_doc star
 
-/-- The opposite type carries the same star operation. -/
-instance [has_star R] : has_star (Rᵒᵖ) :=
-{ star := λ r, op (star (r.unop)) }
-
-@[simp] lemma unop_star [has_star R] (r : Rᵒᵖ) : unop (star r) = star (unop r) := rfl
-@[simp] lemma op_star [has_star R] (r : R) : op (star r) = star (op r) := rfl
 
 /--
 Typeclass for a star operation with is involutive.
@@ -71,9 +66,6 @@ star_involutive _
 lemma star_injective [has_involutive_star R] : function.injective (star : R → R) :=
 star_involutive.injective
 
-instance [has_involutive_star R] : has_involutive_star (Rᵒᵖ) :=
-{ star_involutive := λ r, unop_injective (star_star r.unop) }
-
 /--
 A `*`-monoid is a monoid `R` with an involutive operations `star`
 so `star (r * s) = star s * star r`.
@@ -136,9 +128,6 @@ open_locale big_operators
 
 end
 
-instance [monoid R] [star_monoid R] : star_monoid (Rᵒᵖ) :=
-{ star_mul := λ x y, unop_injective (star_mul y.unop x.unop) }
-
 /--
 Any commutative monoid admits the trivial `*`-structure.
 
@@ -168,9 +157,6 @@ class star_add_monoid (R : Type u) [add_monoid R] extends has_involutive_star R
 export star_add_monoid (star_add)
 attribute [simp] star_add
 
-instance [add_monoid R] [star_add_monoid R] : star_add_monoid (Rᵒᵖ) :=
-{ star_add := λ x y, unop_injective (star_add x.unop y.unop) }
-
 /-- `star` as an `add_equiv` -/
 @[simps apply]
 def star_add_equiv [add_monoid R] [star_add_monoid R] : R ≃+ R :=
@@ -222,9 +208,6 @@ class star_ring (R : Type u) [semiring R] extends star_monoid R :=
 instance star_ring.to_star_add_monoid [semiring R] [star_ring R] : star_add_monoid R :=
 { star_add := star_ring.star_add }
 
-instance [semiring R] [star_ring R] : star_ring (Rᵒᵖ) :=
-{ .. opposite.star_add_monoid }
-
 /-- `star` as an `ring_equiv` from `R` to `Rᵒᵖ` -/
 @[simps apply]
 def star_ring_equiv [semiring R] [star_ring R] : R ≃+* Rᵒᵖ :=
@@ -303,4 +286,55 @@ attribute [simp] star_smul
 
 /-- A commutative star monoid is a star module over itself via `monoid.to_mul_action`. -/
 instance star_monoid.to_star_module [comm_monoid R] [star_monoid R] : star_module R R :=
-⟨λ r s, (star_mul r s).trans (mul_comm _ _)⟩
+⟨star_mul'⟩
+
+/-! ### Instances -/
+
+namespace units
+
+variables [monoid R] [star_monoid R]
+
+instance : star_monoid (units R) :=
+{ star := λ u,
+  { val := star u,
+    inv := star ↑u⁻¹,
+    val_inv := (star_mul _ _).symm.trans $ (congr_arg star u.inv_val).trans $ star_one _,
+    inv_val := (star_mul _ _).symm.trans $ (congr_arg star u.val_inv).trans $ star_one _ },
+  star_involutive := λ u, units.ext (star_involutive _),
+  star_mul := λ u v, units.ext (star_mul _ _) }
+
+@[simp] lemma coe_star (u : units R) : ↑(star u) = (star ↑u : R) := rfl
+@[simp] lemma coe_star_inv (u : units R) : ↑(star u)⁻¹ = (star ↑u⁻¹ : R) := rfl
+
+instance {A : Type*} [has_star A] [has_scalar R A] [star_module R A] : star_module (units R) A :=
+⟨λ u a, (star_smul ↑u a : _)⟩
+
+end units
+
+namespace opposite
+
+/-- The opposite type carries the same star operation. -/
+instance [has_star R] : has_star (Rᵒᵖ) :=
+{ star := λ r, op (star (r.unop)) }
+
+@[simp] lemma unop_star [has_star R] (r : Rᵒᵖ) : unop (star r) = star (unop r) := rfl
+@[simp] lemma op_star [has_star R] (r : R) : op (star r) = star (op r) := rfl
+
+instance [has_involutive_star R] : has_involutive_star (Rᵒᵖ) :=
+{ star_involutive := λ r, unop_injective (star_star r.unop) }
+
+instance [monoid R] [star_monoid R] : star_monoid (Rᵒᵖ) :=
+{ star_mul := λ x y, unop_injective (star_mul y.unop x.unop) }
+
+instance [add_monoid R] [star_add_monoid R] : star_add_monoid (Rᵒᵖ) :=
+{ star_add := λ x y, unop_injective (star_add x.unop y.unop) }
+
+instance [semiring R] [star_ring R] : star_ring (Rᵒᵖ) :=
+{ .. opposite.star_add_monoid }
+
+end opposite
+
+/-- A commutative star monoid is a star module over its opposite via
+`monoid.to_opposite_mul_action`. -/
+instance star_monoid.to_opposite_star_module [comm_monoid R] [star_monoid R] : star_module Rᵒᵖ R :=
+⟨λ r s, star_mul' s r.unop⟩