From cc9de07ab35c004fe561321ca017ace6d8c7dab4 Mon Sep 17 00:00:00 2001 From: Scott Morrison Date: Wed, 2 Mar 2022 02:44:42 +0000 Subject: [PATCH] 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 --- src/algebra/star/basic.lean | 71 ++++++++++--------- src/algebra/star/chsh.lean | 4 +- src/algebra/star/free.lean | 2 +- src/algebra/star/module.lean | 2 +- src/algebra/star/pi.lean | 6 +- src/algebra/star/pointwise.lean | 4 +- src/algebra/star/unitary.lean | 12 ++-- src/analysis/inner_product_space/adjoint.lean | 4 +- src/data/matrix/basic.lean | 4 +- 9 files changed, 56 insertions(+), 53 deletions(-) diff --git a/src/algebra/star/basic.lean b/src/algebra/star/basic.lean index 887d206495a69..382c9fb074b8c 100644 --- a/src/algebra/star/basic.lean +++ b/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⟩ diff --git a/src/algebra/star/chsh.lean b/src/algebra/star/chsh.lean index 51425e78ef6df..3b3bc4f0c4e19 100644 --- a/src/algebra/star/chsh.lean +++ b/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₀) diff --git a/src/algebra/star/free.lean b/src/algebra/star/free.lean index 7f092fad19e67..9e8ef68b90740 100644 --- a/src/algebra/star/free.lean +++ b/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, } diff --git a/src/algebra/star/module.lean b/src/algebra/star/module.lean index 6841734587113..ab098a4a87dab 100644 --- a/src/algebra/star/module.lean +++ b/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. -/ diff --git a/src/algebra/star/pi.lean b/src/algebra/star/pi.lean index bb044dc44f3aa..e86ed581ead55 100644 --- a/src/algebra/star/pi.lean +++ b/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)] : diff --git a/src/algebra/star/pointwise.lean b/src/algebra/star/pointwise.lean index cc4347210a1d0..560462726abfb 100644 --- a/src/algebra/star/pointwise.lean +++ b/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⋆)⁻¹ := diff --git a/src/algebra/star/unitary.lean b/src/algebra/star/unitary.lean index bf2a097d3f7bf..b0053664e7556 100644 --- a/src/algebra/star/unitary.lean +++ b/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 _) diff --git a/src/analysis/inner_product_space/adjoint.lean b/src/analysis/inner_product_space/adjoint.lean index 2536b25b0ff36..401d250da7c5e 100644 --- a/src/analysis/inner_product_space/adjoint.lean +++ b/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⟩ diff --git a/src/data/matrix/basic.lean b/src/data/matrix/basic.lean index 6586152fa9107..59054257655ea 100644 --- a/src/data/matrix/basic.lean +++ b/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, }