feat(algebra/star): replace star_monoid with star_semigroup (#12299)

In preparation for allowing non-unital C^* algebras, replace star_monoid with star_semigroup.




Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/algebra/star/basic.lean

@@ -98,61 +98,62 @@ export has_trivial_star (star_trivial)
 attribute [simp] star_trivial
 
 /--
-A `*`-monoid is a monoid `R` with an involutive operations `star`
+A `*`-semigroup is a semigroup `R` with an involutive operations `star`
 so `star (r * s) = star s * star r`.
 -/
-class star_monoid (R : Type u) [monoid R] extends has_involutive_star R :=
+class star_semigroup (R : Type u) [semigroup R] extends has_involutive_star R :=
 (star_mul : ∀ r s : R, star (r * s) = star s * star r)
 
-export star_monoid (star_mul)
+export star_semigroup (star_mul)
 attribute [simp] star_mul
 
 /-- In a commutative ring, make `simp` prefer leaving the order unchanged. -/
-@[simp] lemma star_mul' [comm_monoid R] [star_monoid R] (x y : R) :
+@[simp] lemma star_mul' [comm_semigroup R] [star_semigroup R] (x y : R) :
   star (x * y) = star x * star y :=
 (star_mul x y).trans (mul_comm _ _)
 
 /-- `star` as an `mul_equiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]
-def star_mul_equiv [monoid R] [star_monoid R] : R ≃* Rᵐᵒᵖ :=
+def star_mul_equiv [semigroup R] [star_semigroup R] : R ≃* Rᵐᵒᵖ :=
 { to_fun := λ x, mul_opposite.op (star x),
   map_mul' := λ x y, (star_mul x y).symm ▸ (mul_opposite.op_mul _ _),
   ..(has_involutive_star.star_involutive.to_equiv star).trans op_equiv}
 
 /-- `star` as a `mul_aut` for commutative `R`. -/
 @[simps apply]
-def star_mul_aut [comm_monoid R] [star_monoid R] : mul_aut R :=
+def star_mul_aut [comm_semigroup R] [star_semigroup R] : mul_aut R :=
 { to_fun := star,
   map_mul' := star_mul',
   ..(has_involutive_star.star_involutive.to_equiv star) }
 
 variables (R)
 
-@[simp] lemma star_one [monoid R] [star_monoid R] : star (1 : R) = 1 :=
+@[simp] lemma star_one [monoid R] [star_semigroup R] : star (1 : R) = 1 :=
 op_injective $ (star_mul_equiv : R ≃* Rᵐᵒᵖ).map_one.trans (op_one _).symm
 
 variables {R}
 
-@[simp] lemma star_pow [monoid R] [star_monoid R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
+@[simp] lemma star_pow [monoid R] [star_semigroup R] (x : R) (n : ℕ) : star (x ^ n) = star x ^ n :=
 op_injective $
   ((star_mul_equiv : R ≃* Rᵐᵒᵖ).to_monoid_hom.map_pow x n).trans (op_pow (star x) n).symm
 
-@[simp] lemma star_inv [group R] [star_monoid R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
+@[simp] lemma star_inv [group R] [star_semigroup R] (x : R) : star (x⁻¹) = (star x)⁻¹ :=
 op_injective $
   ((star_mul_equiv : R ≃* Rᵐᵒᵖ).to_monoid_hom.map_inv x).trans (op_inv (star x)).symm
 
-@[simp] lemma star_zpow [group R] [star_monoid R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
+@[simp] lemma star_zpow [group R] [star_semigroup R] (x : R) (z : ℤ) : star (x ^ z) = star x ^ z :=
 op_injective $
   ((star_mul_equiv : R ≃* Rᵐᵒᵖ).to_monoid_hom.map_zpow x z).trans (op_zpow (star x) z).symm
 
 /-- When multiplication is commutative, `star` preserves division. -/
-@[simp] lemma star_div [comm_group R] [star_monoid R] (x y : R) : star (x / y) = star x / star y :=
+@[simp] lemma star_div [comm_group R] [star_semigroup R] (x y : R) : 
+  star (x / y) = star x / star y :=
 (star_mul_aut : R ≃* R).to_monoid_hom.map_div _ _
 
 section
 open_locale big_operators
 
-@[simp] lemma star_prod [comm_monoid R] [star_monoid R] {α : Type*}
+@[simp] lemma star_prod [comm_monoid R] [star_semigroup R] {α : Type*}
   (s : finset α) (f : α → R):
   star (∏ x in s, f x) = ∏ x in s, star (f x) :=
 (star_mul_aut : R ≃* R).map_prod _ _
@@ -165,15 +166,15 @@ Any commutative monoid admits the trivial `*`-structure.
 See note [reducible non-instances].
 -/
 @[reducible]
-def star_monoid_of_comm {R : Type*} [comm_monoid R] : star_monoid R :=
+def star_semigroup_of_comm {R : Type*} [comm_monoid R] : star_semigroup R :=
 { star := id,
   star_involutive := λ x, rfl,
   star_mul := mul_comm }
 
 section
-local attribute [instance] star_monoid_of_comm
+local attribute [instance] star_semigroup_of_comm
 
-/-- Note that since `star_monoid_of_comm` is reducible, `simp` can already prove this. --/
+/-- Note that since `star_semigroup_of_comm` is reducible, `simp` can already prove this. --/
 lemma star_id_of_comm {R : Type*} [comm_semiring R] {x : R} : star x = x := rfl
 
 end
@@ -229,19 +230,19 @@ end
 
 /--
 A `*`-ring `R` is a (semi)ring with an involutive `star` operation which is additive
-which makes `R` with its multiplicative structure into a `*`-monoid
+which makes `R` with its multiplicative structure into a `*`-semigroup
 (i.e. `star (r * s) = star s * star r`).
 -/
-class star_ring (R : Type u) [semiring R] extends star_monoid R :=
+class star_ring (R : Type u) [non_unital_semiring R] extends star_semigroup R :=
 (star_add : ∀ r s : R, star (r + s) = star r + star s)
 
 @[priority 100]
-instance star_ring.to_star_add_monoid [semiring R] [star_ring R] : star_add_monoid R :=
+instance star_ring.to_star_add_monoid [non_unital_semiring R] [star_ring R] : star_add_monoid R :=
 { star_add := star_ring.star_add }
 
 /-- `star` as an `ring_equiv` from `R` to `Rᵐᵒᵖ` -/
 @[simps apply]
-def star_ring_equiv [semiring R] [star_ring R] : R ≃+* Rᵐᵒᵖ :=
+def star_ring_equiv [non_unital_semiring R] [star_ring R] : R ≃+* Rᵐᵒᵖ :=
 { to_fun := λ x, mul_opposite.op (star x),
   ..star_add_equiv.trans (mul_opposite.op_add_equiv : R ≃+ Rᵐᵒᵖ),
   ..star_mul_equiv }
@@ -308,13 +309,14 @@ See note [reducible non-instances].
 def star_ring_of_comm {R : Type*} [comm_semiring R] : star_ring R :=
 { star := id,
   star_add := λ x y, rfl,
-  ..star_monoid_of_comm }
+  ..star_semigroup_of_comm }
 
 /--
 An ordered `*`-ring is a ring which is both an `ordered_add_comm_group` and a `*`-ring,
 and `0 ≤ r ↔ ∃ s, r = star s * s`.
 -/
-class star_ordered_ring (R : Type u) [ring R] [partial_order R] extends star_ring R :=
+class star_ordered_ring (R : Type u) [non_unital_semiring R] [partial_order R]
+  extends star_ring R :=
 (add_le_add_left       : ∀ a b : R, a ≤ b → ∀ c : R, c + a ≤ c + b)
 (nonneg_iff            : ∀ r : R, 0 ≤ r ↔ ∃ s, r = star s * s)
 
@@ -330,12 +332,12 @@ instance : ordered_add_comm_group R :=
 
 end star_ordered_ring
 
-lemma star_mul_self_nonneg [ring R] [partial_order R] [star_ordered_ring R] {r : R} :
-  0 ≤ star r * r :=
+lemma star_mul_self_nonneg
+  [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} : 0 ≤ star r * r :=
 (star_ordered_ring.nonneg_iff _).mpr ⟨r, rfl⟩
 
-lemma star_mul_self_nonneg' [ring R] [partial_order R] [star_ordered_ring R] {r : R} :
-  0 ≤ r * star r :=
+lemma star_mul_self_nonneg'
+  [non_unital_semiring R] [partial_order R] [star_ordered_ring R] {r : R} : 0 ≤ r * star r :=
 by { nth_rewrite_rhs 0 [←star_star r], exact star_mul_self_nonneg }
 
 /--
@@ -357,7 +359,7 @@ export star_module (star_smul)
 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 :=
+instance star_semigroup.to_star_module [comm_monoid R] [star_semigroup R] : star_module R R :=
 ⟨star_mul'⟩
 
 namespace ring_hom_inv_pair
@@ -374,9 +376,9 @@ end ring_hom_inv_pair
 
 namespace units
 
-variables [monoid R] [star_monoid R]
+variables [monoid R] [star_semigroup R]
 
-instance : star_monoid Rˣ :=
+instance : star_semigroup Rˣ :=
 { star := λ u,
   { val := star u,
     inv := star ↑u⁻¹,
@@ -393,10 +395,10 @@ instance {A : Type*} [has_star A] [has_scalar R A] [star_module R A] : star_modu
 
 end units
 
-lemma is_unit.star [monoid R] [star_monoid R] {a : R} : is_unit a → is_unit (star a)
+lemma is_unit.star [monoid R] [star_semigroup R] {a : R} : is_unit a → is_unit (star a)
 | ⟨u, hu⟩ := ⟨star u, hu ▸ rfl⟩
 
-@[simp] lemma is_unit_star [monoid R] [star_monoid R] {a : R} : is_unit (star a) ↔ is_unit a :=
+@[simp] lemma is_unit_star [monoid R] [star_semigroup R] {a : R} : is_unit (star a) ↔ is_unit a :=
 ⟨λ h, star_star a ▸ h.star, is_unit.star⟩
 
 lemma ring.inverse_star [semiring R] [star_ring R] (a : R) :
@@ -408,13 +410,13 @@ begin
   rw [ring.inverse_non_unit _ ha, ring.inverse_non_unit _ (mt is_unit_star.mp ha), star_zero],
 end
 
-instance invertible.star {R : Type*} [monoid R] [star_monoid R] (r : R) [invertible r] :
+instance invertible.star {R : Type*} [monoid R] [star_semigroup R] (r : R) [invertible r] :
   invertible (star r) :=
 { inv_of := star (⅟r),
   inv_of_mul_self := by rw [←star_mul, mul_inv_of_self, star_one],
   mul_inv_of_self := by rw [←star_mul, inv_of_mul_self, star_one] }
 
-lemma star_inv_of {R : Type*} [monoid R] [star_monoid R] (r : R)
+lemma star_inv_of {R : Type*} [monoid R] [star_semigroup R] (r : R)
   [invertible r] [invertible (star r)] :
   star (⅟r) = ⅟(star r) :=
 by { letI := invertible.star r, convert (rfl : star (⅟r) = _) }
@@ -431,7 +433,7 @@ instance [has_star R] : has_star (Rᵐᵒᵖ) :=
 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ᵐᵒᵖ) :=
+instance [monoid R] [star_semigroup R] : star_semigroup (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ᵐᵒᵖ) :=
@@ -444,5 +446,6 @@ end mul_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 :=
+instance star_semigroup.to_opposite_star_module [comm_monoid R] [star_semigroup R] :
+  star_module Rᵐᵒᵖ R :=
 ⟨λ r s, star_mul' s r.unop⟩

src/algebra/star/chsh.lean

@@ -73,14 +73,14 @@ There is a CHSH tuple in 4-by-4 matrices such that
 universes u
 
 /--
-A CHSH tuple in a `star_monoid R` consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that
+A CHSH tuple in a *-monoid consists of 4 self-adjoint involutions `A₀ A₁ B₀ B₁` such that
 the `Aᵢ` commute with the `Bⱼ`.
 
 The physical interpretation is that `A₀` and `A₁` are a pair of boolean observables which
 are spacelike separated from another pair `B₀` and `B₁` of boolean observables.
 -/
 @[nolint has_inhabited_instance]
-structure is_CHSH_tuple {R} [monoid R] [star_monoid R] (A₀ A₁ B₀ B₁ : R) :=
+structure is_CHSH_tuple {R} [monoid R] [star_semigroup R] (A₀ A₁ B₀ B₁ : R) :=
 (A₀_inv : A₀^2 = 1) (A₁_inv : A₁^2 = 1) (B₀_inv : B₀^2 = 1) (B₁_inv : B₁^2 = 1)
 (A₀_sa : star A₀ = A₀) (A₁_sa : star A₁ = A₁) (B₀_sa : star B₀ = B₀) (B₁_sa : star B₁ = B₁)
 (A₀B₀_commutes : A₀ * B₀ = B₀ * A₀)

src/algebra/star/free.lean

@@ -19,7 +19,7 @@ to avoid importing `algebra.star.basic` into the entire hierarchy.
 namespace free_monoid
 variables {α : Type*}
 
-instance : star_monoid (free_monoid α) :=
+instance : star_semigroup (free_monoid α) :=
 { star := list.reverse,
   star_involutive := list.reverse_reverse,
   star_mul := list.reverse_append, }

src/algebra/star/module.lean

@@ -36,7 +36,7 @@ def star_linear_equiv (R : Type*) {A : Type*}
   .. star_add_equiv }
 
 variables (R : Type*) (A : Type*)
-  [semiring R] [star_monoid R] [has_trivial_star R]
+  [semiring R] [star_semigroup R] [has_trivial_star R]
   [add_comm_group A] [module R A] [star_add_monoid A] [star_module R A]
 
 /-- The self-adjoint elements of a star module, as a submodule. -/

src/algebra/star/pi.lean

@@ -30,14 +30,14 @@ lemma star_def [Π i, has_star (f i)] (x : Π i, f i) : star x = λ i, star (x i
 instance [Π i, has_involutive_star (f i)] : has_involutive_star (Π i, f i) :=
 { star_involutive := λ _, funext $ λ _, star_star _ }
 
-instance [Π i, monoid (f i)] [Π i, star_monoid (f i)] : star_monoid (Π i, f i) :=
+instance [Π i, semigroup (f i)] [Π i, star_semigroup (f i)] : star_semigroup (Π i, f i) :=
 { star_mul := λ _ _, funext $ λ _, star_mul _ _ }
 
 instance [Π i, add_monoid (f i)] [Π i, star_add_monoid (f i)] : star_add_monoid (Π i, f i) :=
 { star_add := λ _ _, funext $ λ _, star_add _ _ }
 
-instance [Π i, semiring (f i)] [Π i, star_ring (f i)] : star_ring (Π i, f i) :=
-{ ..pi.star_add_monoid, ..(pi.star_monoid : star_monoid (Π i, f i)) }
+instance [Π i, non_unital_semiring (f i)] [Π i, star_ring (f i)] : star_ring (Π i, f i) :=
+{ ..pi.star_add_monoid, ..(pi.star_semigroup : star_semigroup (Π i, f i)) }
 
 instance {R : Type w}
   [Π i, has_scalar R (f i)] [has_star R] [Π i, has_star (f i)] [Π i, star_module R (f i)] :

src/algebra/star/pointwise.lean

@@ -96,7 +96,7 @@ hs.preimage $ star_injective.inj_on _
 lemma star_singleton {β : Type*} [has_involutive_star β] (x : β) : ({x} : set β)⋆ = {x⋆} :=
 by { ext1 y, rw [mem_star, mem_singleton_iff, mem_singleton_iff, star_eq_iff_star_eq, eq_comm], }
 
-protected lemma star_mul [monoid α] [star_monoid α] (s t : set α) :
+protected lemma star_mul [monoid α] [star_semigroup α] (s t : set α) :
   (s * t)⋆ = t⋆ * s⋆ :=
 by simp_rw [←image_star, ←image2_mul, image_image2, image2_image_left, image2_image_right,
               star_mul, image2_swap _ s t]
@@ -109,7 +109,7 @@ by simp_rw [←image_star, ←image2_add, image_image2, image2_image_left, image
 instance [has_star α] [has_trivial_star α] : has_trivial_star (set α) :=
 { star_trivial := λ s, by { rw [←star_preimage], ext1, simp [star_trivial] } }
 
-protected lemma star_inv [group α] [star_monoid α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=
+protected lemma star_inv [group α] [star_semigroup α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=
 by { ext, simp only [mem_star, mem_inv, star_inv] }
 
 protected lemma star_inv' [division_ring α] [star_ring α] (s : set α) : (s⁻¹)⋆ = (s⋆)⁻¹ :=

src/algebra/star/unitary.lean

@@ -21,10 +21,10 @@ unitary
 -/
 
 /--
-In a `star_monoid R`, `unitary R` is the submonoid consisting of all the elements `U` of
+In a *-monoid, `unitary R` is the submonoid consisting of all the elements `U` of
 `R` such that `star U * U = 1` and `U * star U = 1`.
 -/
-def unitary (R : Type*) [monoid R] [star_monoid R] : submonoid R :=
+def unitary (R : Type*) [monoid R] [star_semigroup R] : submonoid R :=
 { carrier := {U | star U * U = 1 ∧ U * star U = 1},
   one_mem' := by simp only [mul_one, and_self, set.mem_set_of_eq, star_one],
   mul_mem' := λ U B ⟨hA₁, hA₂⟩ ⟨hB₁, hB₂⟩,
@@ -43,7 +43,7 @@ variables {R : Type*}
 namespace unitary
 
 section monoid
-variables [monoid R] [star_monoid R]
+variables [monoid R] [star_semigroup R]
 
 lemma mem_iff {U : R} : U ∈ unitary R ↔ star U * U = 1 ∧ U * star U = 1 := iff.rfl
 @[simp] lemma star_mul_self_of_mem {U : R} (hU : U ∈ unitary R) : star U * U = 1 := hU.1
@@ -73,7 +73,7 @@ instance : group (unitary R) :=
 instance : has_involutive_star (unitary R) :=
 ⟨λ _, by { ext, simp only [coe_star, star_star] }⟩
 
-instance : star_monoid (unitary R) :=
+instance : star_semigroup (unitary R) :=
 ⟨λ _ _, by { ext, simp only [coe_star, submonoid.coe_mul, star_mul] }⟩
 
 instance : inhabited (unitary R) := ⟨1⟩
@@ -95,7 +95,7 @@ lemma to_units_injective : function.injective (to_units : unitary R → Rˣ) :=
 end monoid
 
 section comm_monoid
-variables [comm_monoid R] [star_monoid R]
+variables [comm_monoid R] [star_semigroup R]
 
 instance : comm_group (unitary R) :=
 { ..unitary.group,
@@ -110,7 +110,7 @@ mem_iff.trans $ and_iff_right_of_imp $ λ h, mul_comm U (star U) ▸ h
 end comm_monoid
 
 section group_with_zero
-variables [group_with_zero R] [star_monoid R]
+variables [group_with_zero R] [star_semigroup R]
 
 @[norm_cast] lemma coe_inv (U : unitary R) : ↑(U⁻¹) = (U⁻¹ : R) :=
 eq_inv_of_mul_right_eq_one (coe_mul_star_self _)

src/analysis/inner_product_space/adjoint.lean

@@ -148,7 +148,7 @@ end
 /-- `E →L[𝕜] E` is a star algebra with the adjoint as the star operation. -/
 instance : has_star (E →L[𝕜] E) := ⟨adjoint⟩
 instance : has_involutive_star (E →L[𝕜] E) := ⟨adjoint_adjoint⟩
-instance : star_monoid (E →L[𝕜] E) := ⟨adjoint_comp⟩
+instance : star_semigroup (E →L[𝕜] E) := ⟨adjoint_comp⟩
 instance : star_ring (E →L[𝕜] E) := ⟨linear_isometry_equiv.map_add adjoint⟩
 instance : star_module 𝕜 (E →L[𝕜] E) := ⟨linear_isometry_equiv.map_smulₛₗ adjoint⟩
 
@@ -280,7 +280,7 @@ by rw [is_self_adjoint, ← linear_map.eq_adjoint_iff]
 /-- `E →ₗ[𝕜] E` is a star algebra with the adjoint as the star operation. -/
 instance : has_star (E →ₗ[𝕜] E) := ⟨adjoint⟩
 instance : has_involutive_star (E →ₗ[𝕜] E) := ⟨adjoint_adjoint⟩
-instance : star_monoid (E →ₗ[𝕜] E) := ⟨adjoint_comp⟩
+instance : star_semigroup (E →ₗ[𝕜] E) := ⟨adjoint_comp⟩
 instance : star_ring (E →ₗ[𝕜] E) := ⟨linear_equiv.map_add adjoint⟩
 instance : star_module 𝕜 (E →ₗ[𝕜] E) := ⟨linear_equiv.map_smulₛₗ adjoint⟩
 

src/data/matrix/basic.lean

@@ -1220,7 +1220,7 @@ by simp [conj_transpose]
 @[simp] lemma conj_transpose_sub [add_group α] [star_add_monoid α] (M N : matrix m n α) :
   (M - N)ᴴ = Mᴴ - Nᴴ  := by ext i j; simp
 
-@[simp] lemma conj_transpose_smul [comm_monoid α] [star_monoid α] (c : α) (M : matrix m n α) :
+@[simp] lemma conj_transpose_smul [comm_monoid α] [star_semigroup α] (c : α) (M : matrix m n α) :
   (c • M)ᴴ = (star c) • Mᴴ :=
 by ext i j; simp [mul_comm]
 
@@ -1292,7 +1292,7 @@ instance [add_monoid α] [star_add_monoid α] : star_add_monoid (matrix n n α)
 { star_add := conj_transpose_add }
 
 /-- When `α` is a `*`-(semi)ring, `matrix.has_star` is also a `*`-(semi)ring. -/
-instance [fintype n] [decidable_eq n] [semiring α] [star_ring α] : star_ring (matrix n n α) :=
+instance [fintype n] [semiring α] [star_ring α] : star_ring (matrix n n α) :=
 { star_add := conj_transpose_add,
   star_mul := conj_transpose_mul, }