feat(Analysis/CStarAlgebra/Extreme): a C⋆-algebra is unital iff there exists an extreme point in the closed unit ball

Mathlib.lean

@@ -1595,6 +1595,7 @@ public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unitary
 public import Mathlib.Analysis.CStarAlgebra.ContinuousLinearMap
 public import Mathlib.Analysis.CStarAlgebra.ContinuousMap
 public import Mathlib.Analysis.CStarAlgebra.Exponential
+public import Mathlib.Analysis.CStarAlgebra.Extreme
 public import Mathlib.Analysis.CStarAlgebra.GelfandDuality
 public import Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
 public import Mathlib.Analysis.CStarAlgebra.Hom

Mathlib/Analysis/CStarAlgebra/ApproximateUnit.lean

@@ -163,6 +163,16 @@ lemma eventually_star_eq {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
     ∀ᶠ x in l, star x = x :=
   hl.eventually_isSelfAdjoint.mp <| .of_forall fun _ ↦ IsSelfAdjoint.star_eq
 
+omit [StarOrderedRing A] in
+lemma closedBall_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    Metric.closedBall 0 1 ∈ l := by
+  simpa [Metric.closedBall] using hl.eventually_norm
+
+omit [StarOrderedRing A] in
+lemma nonneg_mem {l : Filter A} (hl : l.IsIncreasingApproximateUnit) :
+    {x | 0 ≤ x} ∈ l := by
+  simpa using hl.eventually_nonneg
+
 end Filter.IsIncreasingApproximateUnit
 
 namespace CStarAlgebra
@@ -330,4 +340,6 @@ lemma increasingApproximateUnit :
 
 end CStarAlgebra
 
+instance : (approximateUnit A).NeBot := (increasingApproximateUnit A).neBot
+
 end ApproximateUnit

Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean

@@ -344,6 +344,9 @@ lemma norm_quasispectrum_le (a : A) ⦃x : 𝕜⦄ (hx : x ∈ σₙ 𝕜 a) (ha
     ‖x‖ ≤ ‖a‖ := by
   simpa only [cfcₙ_id 𝕜 a] using norm_apply_le_norm_cfcₙ (id : 𝕜 → 𝕜) a hx
 
+alias _root_.quasispectrum.norm_le_norm_of_mem :=
+  NonUnitalIsometricContinuousFunctionalCalculus.norm_quasispectrum_le
+
 lemma isGreatest_nnnorm_quasispectrum (a : A) (ha : p a := by cfc_tac) :
     IsGreatest ((‖·‖₊) '' σₙ 𝕜 a) ‖a‖₊ := by
   simpa only [cfcₙ_id 𝕜 a] using IsGreatest.nnnorm_cfcₙ (id : 𝕜 → 𝕜) a

Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean

@@ -295,3 +295,36 @@ lemma WeakDual.CharacterSpace.homeoEval_naturality {X Y 𝕜 : Type*} [RCLike 
     (homeoEval Y 𝕜 : C(_, _)).comp f =
       (f.compStarAlgHom' 𝕜 𝕜 |> compContinuousMap).comp (homeoEval X 𝕜 : C(_, _)) :=
   rfl
+
+open scoped CStarAlgebra in
+open Unitization in
+lemma CommCStarAlgebra.norm_add_eq_max {A : Type*} [NonUnitalCommCStarAlgebra A]
+    {a b : A} (h : a * b = 0) : ‖a + b‖ = max ‖a‖ ‖b‖ := by
+  let f := gelfandStarTransform A⁺¹ ∘ inrNonUnitalAlgHom ℂ A
+  have hf : Isometry f := gelfandTransform_isometry _ |>.comp isometry_inr
+  simp_rw [← hf.norm_map_of_map_zero (by simp [f]), show f (a + b) = f a + f b by simp [f]]
+  exact ContinuousMap.norm_add_eq_max <| by simpa [f] using congr(f $h)
+
+open NonUnitalStarAlgebra in
+lemma IsSelfAdjoint.norm_add_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
+    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
+    ‖a + b‖ = max ‖a‖ ‖b‖ := by
+  let S : NonUnitalStarSubalgebra ℂ A := (adjoin ℂ {a, b}).topologicalClosure
+  have hS : IsClosed (S : Set A) := (adjoin ℂ {a, b}).isClosed_topologicalClosure
+  have hab' : a * b = b * a := by
+    rw [hab, eq_comm]; simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
+  let _ : NonUnitalCommRing (adjoin ℂ {a, b}) :=
+    adjoinNonUnitalCommRingOfComm ℂ (by grind) (by grind [IsSelfAdjoint.star_eq])
+  let _ : NonUnitalCommRing S := (adjoin ℂ {a, b}).nonUnitalCommRingTopologicalClosure mul_comm
+  let _ : NonUnitalCommCStarAlgebra S := { }
+  let c : S := ⟨a, subset_closure <| subset_adjoin _ _ <| by grind⟩
+  let d : S := ⟨b, subset_closure <| subset_adjoin _ _ <| by grind⟩
+  exact CommCStarAlgebra.norm_add_eq_max (a := c) (b := d) (by ext; simpa)
+
+lemma IsSelfAdjoint.norm_sub_eq_max {A : Type*} [NonUnitalCStarAlgebra A]
+    {a b : A} (hab : a * b = 0) (ha : IsSelfAdjoint a) (hb : IsSelfAdjoint b) :
+    ‖a - b‖ = max ‖a‖ ‖b‖ := by
+  rw [← sq_eq_sq₀ (by positivity) (by positivity)]
+  simp only [sq, ← ha.norm_add_eq_max hab hb, ← CStarRing.norm_star_mul_self]
+  have : b * a = 0 := by simpa [ha.star_eq, hb.star_eq] using congr(star $hab)
+  simp [sub_mul, mul_sub, hb.star_eq, ha.star_eq, hab, this, add_mul, mul_add]

Mathlib/Analysis/Convex/Extreme.lean

@@ -174,6 +174,10 @@ theorem IsExtreme.extremePoints_eq (hAB : IsExtreme 𝕜 A B) :
   Subset.antisymm (fun _ hx ↦ ⟨hx.1, hAB.extremePoints_subset_extremePoints hx⟩)
     (inter_extremePoints_subset_extremePoints_of_subset hAB.1)
 
+@[nontriviality]
+lemma Set.extremePoints_eq_self [Subsingleton E] (A : Set E) : Set.extremePoints 𝕜 A = A :=
+  subset_antisymm extremePoints_subset fun _ h ↦ ⟨h, fun _ _ _ _ _ ↦ Subsingleton.elim ..⟩
+
 end SMul
 
 section OrderedSemiring

Mathlib/Topology/ContinuousMap/Bounded/Normed.lean

@@ -611,4 +611,22 @@ lemma norm_sub_nonneg (f : α →ᵇ ℝ) :
 
 end
 
+/-- If the product of bounded continuous functions is zero, then the norm of their sum is the
+maximum of their norms. -/
+lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
+    {f g : X →ᵇ R} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
+  have hfg : ∀ x, f x = 0 ∨ g x = 0 := by simpa [DFunLike.ext_iff, mul_eq_zero] using h
+  have hfg' (x : X) : ‖(f + g) x‖ = max ‖f x‖ ‖g x‖ := by obtain (h | h) := hfg x <;> simp [h]
+  apply le_antisymm
+  · rw [norm_le (by positivity)]
+    intro x
+    rw [hfg']
+    apply max_le <;> exact norm_coe_le_norm _ x |>.trans (by simp)
+  · apply max_le
+    all_goals
+      rw [norm_le (by positivity)]
+      intro x
+      grw [← (f + g).norm_coe_le_norm x, hfg']
+      simp
+
 end BoundedContinuousFunction

Mathlib/Topology/ContinuousMap/Compact.lean

@@ -460,4 +460,9 @@ instance [NonUnitalNormedRing β] [StarRing β] [CStarRing β] : CStarRing C(α,
 
 end CStarRing
 
+lemma norm_add_eq_max {X R : Type*} [TopologicalSpace X] [NormedRing R] [IsDomain R]
+    [CompactSpace X] {f g : C(X, R)} (h : f * g = 0) : ‖f + g‖ = max ‖f‖ ‖g‖ := by
+  replace h : mkOfCompact f * mkOfCompact g = 0 := by ext x; simpa using congr($h x)
+  simpa using BoundedContinuousFunction.norm_add_eq_max h
+
 end ContinuousMap