chore: namespace lemmas to CStarAlgebra instead of CStarRing (#16653

)

This changes the namespace from `CStarRing` to `CStarAlgebra` for any lemmas whose hypotheses imply `Module ℂ A`. We reserve `CStarRing` for lemmas pertaining only to the normed ring structure, but which do not involve the `ℂ`-algebra structure.

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Instances.lean

@@ -23,7 +23,7 @@ import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
   elements in an `ℝ`-algebra with a continuous functional calculus for selfadjoint elements,
   where every element has compact spectrum, and where nonnegative elements have nonnegative
   spectrum. In particular, this includes unital C⋆-algebras over `ℝ`.
-* `CStarRing.instNonnegSpectrumClass`: In a unital C⋆-algebra over `ℂ` which is also a
+* `CStarAlgebra.instNonnegSpectrumClass`: In a unital C⋆-algebra over `ℂ` which is also a
   `StarOrderedRing`, the spectrum of a nonnegative element is nonnegative.
 
 ## Tags
@@ -495,7 +495,7 @@ variable {A : Type*} [NormedRing A] [CompleteSpace A]
 variable [PartialOrder A] [StarRing A] [StarOrderedRing A] [CStarRing A]
 variable [NormedAlgebra ℂ A] [StarModule ℂ A]
 
-instance CStarRing.instNonnegSpectrumClass : NonnegSpectrumClass ℝ A :=
+instance CStarAlgebra.instNonnegSpectrumClass : NonnegSpectrumClass ℝ A :=
   .of_spectrum_nonneg fun a ha ↦ by
     rw [StarOrderedRing.nonneg_iff] at ha
     induction ha using AddSubmonoid.closure_induction' with
@@ -511,7 +511,7 @@ instance CStarRing.instNonnegSpectrumClass : NonnegSpectrumClass ℝ A :=
       exact hx.nnreal_add (.of_nonneg x_mem) (.of_nonneg y_mem) hy
 
 open ComplexOrder in
-instance CStarRing.instNonnegSpectrumClassComplexUnital : NonnegSpectrumClass ℂ A where
+instance CStarAlgebra.instNonnegSpectrumClassComplexUnital : NonnegSpectrumClass ℂ A where
   quasispectrum_nonneg_of_nonneg a ha x := by
     rw [mem_quasispectrum_iff]
     refine (Or.elim · ge_of_eq fun hx ↦ ?_)
@@ -531,7 +531,7 @@ selfadjoint and has nonnegative spectrum.
 This is not declared as an instance because one may already have a partial order with better
 definitional properties. However, it can be useful to invoke this as an instance in proofs. -/
 @[reducible]
-def CStarRing.spectralOrder : PartialOrder A where
+def CStarAlgebra.spectralOrder : PartialOrder A where
   le x y := IsSelfAdjoint (y - x) ∧ SpectrumRestricts (y - x) ContinuousMap.realToNNReal
   le_refl := by
     simp only [sub_self, IsSelfAdjoint.zero, true_and, forall_const]
@@ -544,9 +544,9 @@ def CStarRing.spectralOrder : PartialOrder A where
   le_trans x y z hxy hyz :=
     ⟨by simpa using hyz.1.add hxy.1, by simpa using hyz.2.nnreal_add hyz.1 hxy.1 hxy.2⟩
 
-/-- The `CStarRing.spectralOrder` on a unital C⋆-algebra is a `StarOrderedRing`. -/
-lemma CStarRing.spectralOrderedRing : @StarOrderedRing A _ (CStarRing.spectralOrder A) _ :=
-  let _ := CStarRing.spectralOrder A
+/-- The `CStarAlgebra.spectralOrder` on a unital C⋆-algebra is a `StarOrderedRing`. -/
+lemma CStarAlgebra.spectralOrderedRing : @StarOrderedRing A _ (CStarAlgebra.spectralOrder A) _ :=
+  let _ := CStarAlgebra.spectralOrder A
   { le_iff := by
       intro x y
       constructor
@@ -578,12 +578,12 @@ variable {A : Type*} [NonUnitalNormedRing A] [CompleteSpace A]
 variable [PartialOrder A] [StarRing A] [StarOrderedRing A] [CStarRing A]
 variable [NormedSpace ℂ A] [IsScalarTower ℂ A A] [SMulCommClass ℂ A A] [StarModule ℂ A]
 
-instance CStarRing.instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where
+instance CStarAlgebra.instNonnegSpectrumClass' : NonnegSpectrumClass ℝ A where
   quasispectrum_nonneg_of_nonneg a ha := by
     rw [Unitization.quasispectrum_eq_spectrum_inr' _ ℂ]
     -- should this actually be an instance on the `Unitization`? (probably scoped)
-    let _ := CStarRing.spectralOrder (Unitization ℂ A)
-    have := CStarRing.spectralOrderedRing (Unitization ℂ A)
+    let _ := CStarAlgebra.spectralOrder (Unitization ℂ A)
+    have := CStarAlgebra.spectralOrderedRing (Unitization ℂ A)
     apply spectrum_nonneg_of_nonneg
     rw [StarOrderedRing.nonneg_iff] at ha ⊢
     have := AddSubmonoid.mem_map_of_mem (Unitization.inrNonUnitalStarAlgHom ℂ A) ha

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Order.lean

@@ -24,11 +24,11 @@ the spectral order.
   C⋆-algebra.
 * `mul_star_le_algebraMap_norm_sq` and `star_mul_le_algebraMap_norm_sq`, which give similar
   statements for `a * star a` and `star a * a`.
-* `CStarRing.norm_le_norm_of_nonneg_of_le`: in a non-unital C⋆-algebra, if `0 ≤ a ≤ b`, then
+* `CStarAlgebra.norm_le_norm_of_nonneg_of_le`: in a non-unital C⋆-algebra, if `0 ≤ a ≤ b`, then
   `‖a‖ ≤ ‖b‖`.
-* `CStarRing.conjugate_le_norm_smul`: in a non-unital C⋆-algebra, we have that
+* `CStarAlgebra.conjugate_le_norm_smul`: in a non-unital C⋆-algebra, we have that
   `star a * b * a ≤ ‖b‖ • (star a * a)` (and a primed version for the `a * b * star a` case).
-* `CStarRing.inv_le_inv_iff`: in a unital C⋆-algebra, `b⁻¹ ≤ a⁻¹` iff `a ≤ b`.
+* `CStarAlgebra.inv_le_inv_iff`: in a unital C⋆-algebra, `b⁻¹ ≤ a⁻¹` iff `a ≤ b`.
 
 ## Tags
 
@@ -43,9 +43,11 @@ variable {A : Type*} [NonUnitalNormedRing A] [CompleteSpace A]
   [PartialOrder A] [StarRing A] [StarOrderedRing A] [CStarRing A] [NormedSpace ℂ A] [StarModule ℂ A]
   [SMulCommClass ℂ A A] [IsScalarTower ℂ A A]
 
-instance instPartialOrder : PartialOrder (Unitization ℂ A) := CStarRing.spectralOrder _
+instance instPartialOrder : PartialOrder (Unitization ℂ A) :=
+    CStarAlgebra.spectralOrder _
 
-instance instStarOrderedRing : StarOrderedRing (Unitization ℂ A) := CStarRing.spectralOrderedRing _
+instance instStarOrderedRing : StarOrderedRing (Unitization ℂ A) :=
+    CStarAlgebra.spectralOrderedRing _
 
 lemma inr_le_iff (a b : A) (ha : IsSelfAdjoint a := by cfc_tac)
     (hb : IsSelfAdjoint b := by cfc_tac) :
@@ -124,11 +126,13 @@ lemma IsSelfAdjoint.neg_algebraMap_norm_le_self {a : A} (ha : IsSelfAdjoint a :=
     exact IsSelfAdjoint.le_algebraMap_norm_self (neg ha)
   exact neg_le.mp this
 
-lemma CStarRing.mul_star_le_algebraMap_norm_sq {a : A} : a * star a ≤ algebraMap ℝ A (‖a‖ ^ 2) := by
+lemma CStarAlgebra.mul_star_le_algebraMap_norm_sq {a : A} :
+    a * star a ≤ algebraMap ℝ A (‖a‖ ^ 2) := by
   have : a * star a ≤ algebraMap ℝ A ‖a * star a‖ := IsSelfAdjoint.le_algebraMap_norm_self
   rwa [CStarRing.norm_self_mul_star, ← pow_two] at this
 
-lemma CStarRing.star_mul_le_algebraMap_norm_sq {a : A} : star a * a ≤ algebraMap ℝ A (‖a‖ ^ 2) := by
+lemma CStarAlgebra.star_mul_le_algebraMap_norm_sq {a : A} :
+    star a * a ≤ algebraMap ℝ A (‖a‖ ^ 2) := by
   have : star a * a ≤ algebraMap ℝ A ‖star a * a‖ := IsSelfAdjoint.le_algebraMap_norm_self
   rwa [CStarRing.norm_star_mul_self, ← pow_two] at this
 
@@ -138,7 +142,7 @@ lemma IsSelfAdjoint.toReal_spectralRadius_eq_norm {a : A} (ha : IsSelfAdjoint a)
     (spectralRadius ℝ a).toReal = ‖a‖ := by
   simp [ha.spectrumRestricts.spectralRadius_eq, ha.spectralRadius_eq_nnnorm]
 
-namespace CStarRing
+namespace CStarAlgebra
 
 lemma norm_or_neg_norm_mem_spectrum [Nontrivial A] {a : A}
     (ha : IsSelfAdjoint a := by cfc_tac) : ‖a‖ ∈ spectrum ℝ a ∨ -‖a‖ ∈ spectrum ℝ a := by
@@ -189,7 +193,7 @@ lemma nnnorm_le_natCast_iff_of_nonneg (a : A) (n : ℕ) (ha : 0 ≤ a := by cfc_
     ‖a‖₊ ≤ n ↔ a ≤ n := by
   simpa using nnnorm_le_iff_of_nonneg a n
 
-end CStarRing
+end CStarAlgebra
 
 section Inv
 
@@ -209,7 +213,7 @@ lemma CFC.conjugate_rpow_neg_one_half {a : A} (h₀ : IsUnit a) (ha : 0 ≤ a :=
 
 /-- In a unital C⋆-algebra, if `a` is nonnegative and invertible, and `a ≤ b`, then `b` is
 invertible. -/
-lemma CStarRing.isUnit_of_le {a b : A} (h₀ : IsUnit a) (ha : 0 ≤ a := by cfc_tac)
+lemma CStarAlgebra.isUnit_of_le {a b : A} (h₀ : IsUnit a) (ha : 0 ≤ a := by cfc_tac)
     (hab : a ≤ b) : IsUnit b := by
   rw [← spectrum.zero_not_mem_iff ℝ≥0] at h₀ ⊢
   nontriviality A
@@ -230,7 +234,7 @@ lemma le_iff_norm_sqrt_mul_rpow {a b : A} (hbu : IsUnit b) (ha : 0 ≤ a) (hb :
     rw [← sq_le_one_iff (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self, star_mul,
       IsSelfAdjoint.of_nonneg sqrt_nonneg, IsSelfAdjoint.of_nonneg rpow_nonneg,
       ← mul_assoc, mul_assoc _ _ (sqrt a), sqrt_mul_sqrt_self a,
-      CStarRing.norm_le_one_iff_of_nonneg _ hbab]
+      CStarAlgebra.norm_le_one_iff_of_nonneg _ hbab]
   refine ⟨fun h ↦ ?_, fun h ↦ ?_⟩
   · calc
       _ ≤ ↑b ^ (-(1 / 2) : ℝ) * (b : A) * ↑b ^ (-(1 / 2) : ℝ) :=
@@ -252,8 +256,10 @@ lemma le_iff_norm_sqrt_mul_sqrt_inv {a : A} {b : Aˣ} (ha : 0 ≤ a) (hb : 0 ≤
     CFC.rpow_rpow (b : A) _ _ (by simp) (by norm_num), le_iff_norm_sqrt_mul_rpow b.isUnit ha hb]
   norm_num
 
+namespace CStarAlgebra
+
 /-- In a unital C⋆-algebra, if `0 ≤ a ≤ b` and `a` and `b` are units, then `b⁻¹ ≤ a⁻¹`. -/
-protected lemma CStarRing.inv_le_inv {a b : Aˣ} (ha : 0 ≤ (a : A))
+protected lemma inv_le_inv {a b : Aˣ} (ha : 0 ≤ (a : A))
     (hab : (a : A) ≤ b) : (↑b⁻¹ : A) ≤ a⁻¹ := by
   have hb := ha.trans hab
   have hb_inv : (0 : A) ≤ b⁻¹ := inv_nonneg_of_nonneg b hb
@@ -267,44 +273,46 @@ protected lemma CStarRing.inv_le_inv {a b : Aˣ} (ha : 0 ≤ (a : A))
 
 /-- In a unital C⋆-algebra, if `0 ≤ a` and `0 ≤ b` and `a` and `b` are units, then `a⁻¹ ≤ b⁻¹`
 if and only if `b ≤ a`. -/
-protected lemma CStarRing.inv_le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (b : A)) :
+protected lemma inv_le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (b : A)) :
     (↑a⁻¹ : A) ≤ b⁻¹ ↔ (b : A) ≤ a :=
-  ⟨CStarRing.inv_le_inv (inv_nonneg_of_nonneg a ha), CStarRing.inv_le_inv hb⟩
+  ⟨CStarAlgebra.inv_le_inv (inv_nonneg_of_nonneg a ha), CStarAlgebra.inv_le_inv hb⟩
 
-lemma CStarRing.inv_le_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
+lemma inv_le_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
     (↑a⁻¹ : A) ≤ b ↔ (↑b⁻¹ : A) ≤ a := by
-  simpa using CStarRing.inv_le_inv_iff ha (inv_nonneg_of_nonneg b hb)
+  simpa using CStarAlgebra.inv_le_inv_iff ha (inv_nonneg_of_nonneg b hb)
 
-lemma CStarRing.le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
+lemma le_inv_iff {a b : Aˣ} (ha : 0 ≤ (a : A)) (hb : 0 ≤ (↑b : A)) :
     a ≤ (↑b⁻¹ : A) ↔ b ≤ (↑a⁻¹ : A) := by
-  simpa using CStarRing.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb
+  simpa using CStarAlgebra.inv_le_inv_iff (inv_nonneg_of_nonneg a ha) hb
 
-lemma CStarRing.one_le_inv_iff_le_one {a : Aˣ} (ha : 0 ≤ (a : A)) :
+lemma one_le_inv_iff_le_one {a : Aˣ} (ha : 0 ≤ (a : A)) :
     1 ≤ (↑a⁻¹ : A) ↔ a ≤ 1 := by
-  simpa using CStarRing.le_inv_iff (a := 1) (by simp) ha
+  simpa using CStarAlgebra.le_inv_iff (a := 1) (by simp) ha
 
-lemma CStarRing.inv_le_one_iff_one_le {a : Aˣ} (ha : 0 ≤ (a : A)) :
+lemma inv_le_one_iff_one_le {a : Aˣ} (ha : 0 ≤ (a : A)) :
     (↑a⁻¹ : A) ≤ 1 ↔ 1 ≤ a := by
-  simpa using CStarRing.inv_le_iff ha (b := 1) (by simp)
+  simpa using CStarAlgebra.inv_le_iff ha (b := 1) (by simp)
 
-lemma CStarRing.inv_le_one {a : Aˣ} (ha : 1 ≤ a) : (↑a⁻¹ : A) ≤ 1 :=
-  CStarRing.inv_le_one_iff_one_le (zero_le_one.trans ha) |>.mpr ha
+lemma inv_le_one {a : Aˣ} (ha : 1 ≤ a) : (↑a⁻¹ : A) ≤ 1 :=
+  CStarAlgebra.inv_le_one_iff_one_le (zero_le_one.trans ha) |>.mpr ha
 
-lemma CStarRing.le_one_of_one_le_inv {a : Aˣ} (ha : 1 ≤ (↑a⁻¹ : A)) : (a : A) ≤ 1 := by
-  simpa using CStarRing.inv_le_one ha
+lemma le_one_of_one_le_inv {a : Aˣ} (ha : 1 ≤ (↑a⁻¹ : A)) : (a : A) ≤ 1 := by
+  simpa using CStarAlgebra.inv_le_one ha
 
-lemma CStarRing.rpow_neg_one_le_rpow_neg_one {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) :
+lemma rpow_neg_one_le_rpow_neg_one {a b : A} (ha : 0 ≤ a) (hab : a ≤ b) (hau : IsUnit a) :
     b ^ (-1 : ℝ) ≤ a ^ (-1 : ℝ) := by
   lift b to Aˣ using isUnit_of_le hau ha hab
   lift a to Aˣ using hau
   rw [rpow_neg_one_eq_inv a ha, rpow_neg_one_eq_inv b (ha.trans hab)]
-  exact CStarRing.inv_le_inv ha hab
+  exact CStarAlgebra.inv_le_inv ha hab
 
-lemma CStarRing.rpow_neg_one_le_one {a : A} (ha : 1 ≤ a) : a ^ (-1 : ℝ) ≤ 1 := by
+lemma rpow_neg_one_le_one {a : A} (ha : 1 ≤ a) : a ^ (-1 : ℝ) ≤ 1 := by
   lift a to Aˣ using isUnit_of_le isUnit_one zero_le_one ha
   rw [rpow_neg_one_eq_inv a (zero_le_one.trans ha)]
   exact inv_le_one ha
 
+end CStarAlgebra
+
 end Inv
 
 end CStar_unital
@@ -315,7 +323,7 @@ variable {A : Type*} [NonUnitalNormedRing A] [CompleteSpace A] [PartialOrder A]
   [StarOrderedRing A] [CStarRing A] [NormedSpace ℂ A] [StarModule ℂ A]
   [SMulCommClass ℂ A A] [IsScalarTower ℂ A A]
 
-namespace CStarRing
+namespace CStarAlgebra
 
 open ComplexOrder in
 instance instNonnegSpectrumClassComplexNonUnital : NonnegSpectrumClass ℂ A where
@@ -375,6 +383,6 @@ lemma isClosed_nonneg : IsClosed {a : A | 0 ≤ a} := by
   refine isClosed_eq ?_ ?_ |>.inter <| isClosed_le ?_ ?_
   all_goals fun_prop
 
-end CStarRing
+end CStarAlgebra
 
 end CStar_nonunital

Mathlib/Analysis/CStarAlgebra/Module/Constructions.lean

@@ -142,7 +142,7 @@ lemma max_le_prod_norm (x : C⋆ᵐᵒᵈ (E × F)) : max ‖x.1‖ ‖x.2‖ 
     Real.sqrt_le_sqrt_iff]
   constructor
   all_goals
-    apply norm_le_norm_of_nonneg_of_le
+    apply CStarAlgebra.norm_le_norm_of_nonneg_of_le
     all_goals
       aesop (add safe apply CStarModule.inner_self_nonneg)
 
@@ -260,7 +260,7 @@ lemma norm_apply_le_norm (x : C⋆ᵐᵒᵈ (Π i, E i)) (i : ι) : ‖x i‖ 
   let _ : NormedAddCommGroup (C⋆ᵐᵒᵈ (Π i, E i)) := normedAddCommGroup
   refine abs_le_of_sq_le_sq' ?_ (by positivity) |>.2
   rw [pi_norm_sq, norm_sq_eq]
-  refine norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
+  refine CStarAlgebra.norm_le_norm_of_nonneg_of_le inner_self_nonneg ?_
   exact Finset.single_le_sum (fun j _ ↦ inner_self_nonneg (x := x j)) (Finset.mem_univ i)
 
 open Finset in

Mathlib/Analysis/CStarAlgebra/Module/Defs.lean

@@ -209,7 +209,7 @@ lemma inner_mul_inner_swap_le [CompleteSpace A] {x y : E} : ⟪y, x⟫ * ⟪x, y
             _ ≤ ‖x‖ ^ 2 • (star a * a) - ‖x‖ ^ 2 • (⟪y, x⟫ * a)
                   - ‖x‖ ^ 2 • (star a * ⟪x, y⟫) + ‖x‖ ^ 2 • (‖x‖ ^ 2 • ⟪y, y⟫) := by
                       gcongr
-                      calc _ ≤ ‖⟪x, x⟫_A‖ • (star a * a) := CStarRing.conjugate_le_norm_smul
+                      calc _ ≤ ‖⟪x, x⟫_A‖ • (star a * a) := CStarAlgebra.conjugate_le_norm_smul
                         _ = (Real.sqrt ‖⟪x, x⟫_A‖) ^ 2 • (star a * a) := by
                                   congr
                                   have : 0 ≤ ‖⟪x, x⟫_A‖ := by positivity
@@ -226,7 +226,7 @@ lemma norm_inner_le [CompleteSpace A] {x y : E} : ‖⟪x, y⟫‖ ≤ ‖x‖ *
   have := calc ‖⟪x, y⟫‖ ^ 2 = ‖⟪y, x⟫ * ⟪x, y⟫‖ := by
                 rw [← star_inner x, CStarRing.norm_star_mul_self, pow_two]
     _ ≤ ‖‖x‖^ 2 • ⟪y, y⟫‖ := by
-                refine CStarRing.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
+                refine CStarAlgebra.norm_le_norm_of_nonneg_of_le ?_ inner_mul_inner_swap_le
                 rw [← star_inner x]
                 exact star_mul_self_nonneg ⟪x, y⟫_A
     _ = ‖x‖ ^ 2 * ‖⟪y, y⟫‖ := by simp [norm_smul]