diff --git a/Mathlib/Algebra/Algebra/Defs.lean b/Mathlib/Algebra/Algebra/Defs.lean index ed95babadabe62..18858a87579893 100644 --- a/Mathlib/Algebra/Algebra/Defs.lean +++ b/Mathlib/Algebra/Algebra/Defs.lean @@ -421,3 +421,9 @@ theorem algebraMap.smul' [Monoid A] [MulDistribMulAction A C] [SMulDistribClass algebraMap B C (a • b) = a • (algebraMap B C b) := coe_smul' _ _ _ end algebraMap + +attribute [local instance] IsUnital.toSemiring in +/-- A unital non-unital algebra is an algebra. -/ +noncomputable abbrev IsUnital.toAlgebra {R A : Type*} [CommSemiring R] [NonUnitalSemiring A] + [Module R A] [IsScalarTower R A A] [SMulCommClass R A A] [IsUnital A] : Algebra R A := + .ofModule smul_mul_assoc mul_smul_comm diff --git a/Mathlib/Algebra/Group/Defs.lean b/Mathlib/Algebra/Group/Defs.lean index d948baeee2b0ef..0a6426f1f20052 100644 --- a/Mathlib/Algebra/Group/Defs.lean +++ b/Mathlib/Algebra/Group/Defs.lean @@ -45,6 +45,8 @@ We register the following instances: -/ +set_option linter.style.longFile 1700 + @[expose] public section assert_not_exists MonoidWithZero DenselyOrdered Function.const_injective @@ -418,6 +420,38 @@ theorem mul_one : ∀ a : M, a * 1 = a := end MulOneClass +section IsUnital + +/-- A multiplicative magma is **unital** if there exists a unit. + +**Note**: Do not use this unless it is the only reasonable way to phrase or prove a statement. +In general you should use `NonUnitalRing`, `Ring`, etc. -/ +@[mk_iff] class IsUnital (A : Type*) [Mul A] : Prop where + isUnital : ∃ u : A, ∀ x : A, u * x = x ∧ x * u = x + +/-- A multiplicative magma is **not-unital** if there does not exist a unit. -/ +@[mk_iff] class IsNotUnital (A : Type*) [Mul A] : Prop where + isNotUnital : ∀ u : A, ∃ x : A, u * x ≠ x ∨ x * u ≠ x + +@[simp] lemma not_isUnital_iff_isNotUnital {A : Type*} [Mul A] : ¬IsUnital A ↔ IsNotUnital A := by + simp [isUnital_iff, isNotUnital_iff, -not_and, Classical.not_and_iff_not_or_not] + +@[simp] lemma not_isNotUnital_iff_isUnital {A : Type*} [Mul A] : ¬IsNotUnital A ↔ IsUnital A := by + grind [not_isUnital_iff_isNotUnital] + +variable {A : Type*} + +/-- A unital magma is `MulOneClass`. -/ +noncomputable abbrev IsUnital.toMulOneClass [Mul A] [IsUnital A] : MulOneClass A where + one := isUnital.choose + one_mul a := (isUnital.choose_spec a).1 + mul_one a := (isUnital.choose_spec a).2 + +lemma MulOneClass.isUnital [MulOneClass A] : IsUnital A where + isUnital := ⟨1, fun x ↦ ⟨one_mul x, mul_one x⟩⟩ + +end IsUnital + section variable {M : Type u} @@ -784,6 +818,10 @@ end IsDedekindFiniteMonoid end Monoid +attribute [local instance] IsUnital.toMulOneClass in +/-- A unital semigroup is a monoid. -/ +noncomputable abbrev IsUnital.toMonoid {A : Type*} [Semigroup A] [IsUnital A] : Monoid A where + /-- An additive monoid is torsion-free if scalar multiplication by every non-zero element `n : ℕ` is injective. -/ @[mk_iff] diff --git a/Mathlib/Algebra/Ring/Defs.lean b/Mathlib/Algebra/Ring/Defs.lean index 5bcb9b4e73ec77..ff1fc7bf83ddea 100644 --- a/Mathlib/Algebra/Ring/Defs.lean +++ b/Mathlib/Algebra/Ring/Defs.lean @@ -529,3 +529,38 @@ scoped instance (priority := 50) [Ring R] [IsMulCommutative R] : CommRing R where end IsMulCommutative + +noncomputable section +namespace IsUnital +variable {A : Type*} + +attribute [local instance] IsUnital.toMulOneClass + +/-- A unital non-associative semiring is a non-associative semiring. -/ +abbrev toNonAssocSemiring [NonUnitalNonAssocSemiring A] [IsUnital A] : NonAssocSemiring A where + +/-- A unital non-unital non-associative commutative semiring is a non-associative +commutative semiring. -/ +abbrev toNonAssocCommSemiring [NonUnitalNonAssocCommSemiring A] [IsUnital A] : + NonAssocCommSemiring A where + +/-- A unital non-unital semiring is a semiring. -/ +abbrev toSemiring [NonUnitalSemiring A] [IsUnital A] : Semiring A where + +/-- A unital non-unital commutative semiring is a commutative semiring. -/ +abbrev toCommSemiring [NonUnitalCommSemiring A] [IsUnital A] : CommSemiring A where + +/-- A unital non-unital non-associative ring is a non-associative ring. -/ +abbrev toNonAssocRing [NonUnitalNonAssocRing A] [IsUnital A] : NonAssocRing A where + +/-- A unital non-unital non-associative commutative ring is a non-associative commutative ring. -/ +abbrev toNonAssocCommRing [NonUnitalNonAssocCommRing A] [IsUnital A] : NonAssocCommRing A where + +/-- A unital non-unital ring is a ring. -/ +abbrev toRing [NonUnitalRing A] [IsUnital A] : Ring A where + +/-- A unital non-unital commutative ring is a commutative ring. -/ +abbrev toCommRing [NonUnitalCommRing A] [IsUnital A] : CommRing A where + +end IsUnital +end diff --git a/Mathlib/Analysis/CStarAlgebra/Classes.lean b/Mathlib/Analysis/CStarAlgebra/Classes.lean index 023287c12afe89..ac668009b9a87a 100644 --- a/Mathlib/Analysis/CStarAlgebra/Classes.lean +++ b/Mathlib/Analysis/CStarAlgebra/Classes.lean @@ -141,3 +141,16 @@ noncomputable instance [CStarAlgebra A] : CStarAlgebra Aᵐᵒᵖ where noncomputable instance [CommCStarAlgebra A] : CommCStarAlgebra Aᵐᵒᵖ where end MulOpposite + +attribute [local instance] IsUnital.toMulOneClass in +/-- A unital non-unital C⋆-algebra is a C⋆-algebra. -/ +noncomputable abbrev IsUnital.toCStarAlgebra {A : Type*} [NonUnitalCStarAlgebra A] [IsUnital A] : + CStarAlgebra A where + __ := ‹NonUnitalCStarAlgebra A› + __ := toSemiring + __ := toAlgebra + +attribute [local instance] IsUnital.toCStarAlgebra in +/-- A unital non-unital commutative C⋆-algebra is a commutative C⋆-algebra. -/ +noncomputable abbrev IsUnital.toCommCStarAlgebra {A : Type*} [NonUnitalCommCStarAlgebra A] + [IsUnital A] : CommCStarAlgebra A where diff --git a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean index 56caf8a9da64e3..6f8f8d546dd209 100644 --- a/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean +++ b/Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean @@ -346,6 +346,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 diff --git a/Mathlib/Analysis/CStarAlgebra/Extreme.lean b/Mathlib/Analysis/CStarAlgebra/Extreme.lean index 7bf7715670618e..69dbf1116bfa01 100644 --- a/Mathlib/Analysis/CStarAlgebra/Extreme.lean +++ b/Mathlib/Analysis/CStarAlgebra/Extreme.lean @@ -6,8 +6,14 @@ Authors: Monica Omar, Jireh Loreaux, Jon Bannon module public import Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Order +public import Mathlib.Analysis.CStarAlgebra.Unitary.Maps public import Mathlib.Analysis.Convex.Extreme +import Mathlib.Analysis.Convex.Strict.Extreme +import Mathlib.Analysis.CStarAlgebra.ApproximateUnit +import Mathlib.Analysis.CStarAlgebra.GelfandDuality +import Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs + /-! # Extreme points of the closed unit ball in C⋆-algebras This file contains results on the extreme points of the closed unit ball in (unital) C⋆-algebras. @@ -20,8 +26,208 @@ public section open Set Metric CFC CStarAlgebra Unitization +open scoped ComplexStarModule in +lemma CStarAlgebra.one_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] : + 1 ∈ extremePoints ℝ (closedBall (0 : A) 1) := by + nontriviality A + /- Suppose that `1` is a convex combination of `x` and `y`. Then, since `1` is self + adjoint, it is also a combination of their real and imaginary parts, which we + call `a` and `b`. Moreover, `b` is a linear polynomial in the variable `a`, so we + may write it as the continuous functional calculus applied to the appropriate + function of `a`. -/ + refine ⟨by simp, fun x hx y hy hxy ↦ ?_⟩ + let +nondep (eq := ha') a : A := ℜ x + let +nondep (eq := hb') b : A := ℜ y + simp only [mem_closedBall, dist_zero_right] at hx hy + have ha : ‖a‖ ≤ 1 := by simpa [ha'] using realPart.norm_le _ |>.trans hx + have hb : ‖b‖ ≤ 1 := by simpa [hb'] using realPart.norm_le _ |>.trans hy + obtain ⟨c₁, hc₁, c₂, hc₂, hc, hcab⟩ := by simpa [openSegment] using hxy + replace hcab : c₁ • a + c₂ • b = 1 := by simpa [ha', hb'] using congr((ℜ $hcab : A)) + have : b = c₂⁻¹ • 1 - c₂⁻¹ • c₁ • a := by + simpa [inv_smul_smul₀ hc₂.ne', eq_sub_iff_add_eq'] using congr(c₂⁻¹ • $hcab) + rw [this, ← cfc_id' ℝ a, ← cfc_one ℝ a, ← cfc_smul .., ← cfc_smul .., ← cfc_smul .., + ← cfc_sub .., ← cfc_smul .., ← cfc_add .., cfc_eq_cfc_iff_eqOn] at hcab + /- By passing to functions, we will show that `a = 1`. In particular, the constant + function `1` on the `ℝ`-spectrum of `a` is a convex combination of functions (one of + which is the identity) which are bounded in absolute value by `1`. Since `1 : ℝ` is + extreme in `Icc (-1) 1`, we conclude that these functions must be `1` on the + spectrum of `a`. -/ + obtain rfl : a = 1 := by + refine CFC.eq_one_of_spectrum_subset_one (R := ℝ) a fun r hr ↦ ?_ + have h1_mem : (1 : ℝ) ∈ openSegment ℝ r (c₂⁻¹ - c₂⁻¹ * c₁ * r) := + ⟨c₁, c₂, hc₁, hc₂, hc, by simpa [mul_assoc] using hcab hr⟩ + have key : (1 : ℝ) ∈ extremePoints ℝ (Icc (-1) 1) := by simp + simp only [mem_singleton_iff] + refine mem_extremePoints_iff_left.mp key |>.2 _ ?_ _ ?_ h1_mem + · simpa [abs_le] using (spectrum.norm_le_norm_of_mem hr).trans ha + · suffices c₂⁻¹ - c₂⁻¹ * c₁ * r ∈ spectrum ℝ b by + simpa [abs_le] using (spectrum.norm_le_norm_of_mem this).trans hb + rw [this, ← Algebra.algebraMap_eq_smul_one, sub_eq_add_neg, sub_eq_add_neg] + rwa [add_comm c₂⁻¹, spectrum.add_mem_add_iff, ← spectrum.neg_eq, Set.neg_mem_neg, smul_smul, + spectrum.smul_eq_smul _ _ (nonempty_of_mem hr), ← smul_eq_mul _ r, + Set.smul_mem_smul_set_iff₀ (by positivity)] + /- Since `ℜ x = a = 1`, so too we conclude `ℜ y = b = 1`. -/ + obtain rfl : b = 1 := by + simpa [← smul_assoc, ← sub_smul, (sub_eq_iff_eq_add.mpr hc.symm).symm, mul_sub, hc₂.ne'] + clear this hb ha hcab hb' hc hc₂ hc₁ c₁ c₂ hy hxy y + /- Since `ℜ x = 1`, the real and imaginary parts of `x` commute, so `x` is normal. It + then suffices to show that `ℑ x = 0`. -/ + have hx' : IsStarNormal x := by simp [isStarNormal_iff_commute_realPart_imaginaryPart, ← ha'] + suffices (ℑ x : A) = 0 by rw [← realPart_add_I_smul_imaginaryPart x, ← ha', this]; simp + let := spectralOrder A + let := spectralOrderedRing A + /- Note that `‖1 + (ℑ x) ^ 2‖ = ‖(ℜ x) ^ 2 + (ℑ x) ^ 2‖ = ‖star x * x‖ = ‖x‖ ^ 2 ≤ 1`. + Therefore, `1 + (ℑ x) ^ 2 ≤ 1`, so `(ℑ x) ^ 2 ≤ 0`. Since `(ℑ x) ^ 2` is clearly nonnegative, + we conclude that it is zero, and hence so also `ℑ x = 0`, as desired. -/ + rw [← sq_le_one_iff₀ (by positivity), sq, ← CStarRing.norm_star_mul_self, + star_mul_self_eq_realPart_sq_add_imaginaryPart_sq, ← ha', mul_one, ← sq, + norm_le_one_iff_of_nonneg _ (add_nonneg zero_le_one (ℑ x).2.sq_nonneg)] at hx + rw [← norm_eq_zero, ← sq_eq_zero_iff, ← IsSelfAdjoint.norm_mul_self (ℑ x).2, ← sq, norm_eq_zero] + exact le_antisymm (by simpa using hx) (ℑ x).2.sq_nonneg + +lemma Unitary.coe_mem_extremePoints_unitClosedBall {A : Type*} [CStarAlgebra A] (u : unitary A) : + (u : A) ∈ extremePoints ℝ (closedBall 0 1) := by + rw [← map_zero (mulLeft ℝ A u), ← LinearIsometryEquiv.image_closedBall, ← image_extremePoints] + exact ⟨1 , ⟨one_mem_extremePoints_unitClosedBall, by simp⟩⟩ + variable {A : Type*} [NonUnitalCStarAlgebra A] +theorem star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall {a : A} + (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : a * star a * a = a := by + let := spectralOrder A + let := spectralOrderedRing A + suffices a * abs a = a by rw [mul_assoc, ← abs_mul_abs, ← mul_assoc, this, this] + obtain ⟨ha, h⟩ := mem_extremePoints_iff_left.mp ha + simp only [mem_closedBall, dist_zero_right] at ha h + refine @h _ ?_ ((2 : ℝ) • a - a * abs a) ?_ ⟨2⁻¹, 2⁻¹, by simp [smul_sub, ← two_mul]⟩ + · grw [norm_mul_le, norm_abs, ha, one_mul, ha] + · calc + _ = ‖(2 : ℝ) • abs a - abs a * abs a‖ := by + simp_rw [← sq_eq_sq₀ (norm_nonneg _) (norm_nonneg _), sq, ← CStarRing.norm_star_mul_self] + simp only [star_sub, star_smul, star_mul, mul_sub, mul_smul_comm, sub_mul, smul_mul_assoc] + simp [abs_nonneg a |>.star_eq, mul_assoc, ← mul_assoc _ a, ← abs_mul_abs] + _ = ‖cfcₙ (fun x : ℝ ↦ 2 * x - x * x) (abs a)‖ := by + rw [cfcₙ_sub _ _, cfcₙ_const_mul _ _, cfcₙ_mul _ _, cfcₙ_id' ℝ (abs a)] + _ ≤ _ := norm_cfcₙ_le fun x hx ↦ by + have := x.le_norm_self.trans (by grw [quasispectrum.norm_le_norm_of_mem _ hx, norm_abs, ha]) + rw [Real.norm_of_nonneg] <;> nlinarith [quasispectrum_nonneg_of_nonneg _ (by simp) _ hx] + +attribute [local grind .] IsSelfAdjoint.star_mul_self IsIdempotentElem IsSelfAdjoint.mul_star_self +attribute [local grind] IsStarProjection + +/-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a +partial isometry (in other words, `star a * a` is a projection). -/ +theorem isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall + {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (star a * a) := by + grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha] + +/-- Every extreme point in the closed unit ball of a `NonUnitalCStarAlgebra` is a +partial isometry (in other words, `a * star a` is a projection). -/ +theorem isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall + {a : A} (ha : a ∈ extremePoints ℝ (closedBall 0 1)) : IsStarProjection (a * star a) := by + grind [star_self_conjugate_eq_self_of_mem_extremePoints_closedUnitBall ha] + +/-- If `x` is an extreme point in the closed unit ball of a C⋆-algebra `A`, +with initial projection `p = star x * x` and final projection `q = x * star x`, +"`(1 - q) A (1 - p) = 0`". Note: This notation is an informal +shorthand used in paper proofs to make them more transparent, but it is +nonsense to refer to `1`, and the notation means that everything should be +considered as fully expanded. This is reflected in the statement below. +*The converse is Sakai 1.6.4.* -/ +private theorem eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall + {x a b : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) (ha : a ∈ closedBall 0 1) + (hb : a = b - b * (star x * x) - (x * star x) * b + (x * star x) * b * (star x * x)) : + a = 0 := by + have hP := isStarProjection_star_mul_self_of_mem_extremePoints_closedUnitBall hx + have hQ := isStarProjection_self_mul_star_of_mem_extremePoints_closedUnitBall hx + set p := star x * x with hp + /- Notice that `x = q * x * p`, and `star x = p * star x * q` formally yield + `star x * (1 - q) * b * (1 - p) = 0` with the above abusive notation. By substituting for `a` in + `‖star a * x * star x * a‖` and expanding, we obtain this, and its adjoint, rigorously. -/ + have hxa : star x * a = 0 := by + rw [← norm_eq_zero, ← mul_self_eq_zero, ← CStarRing.norm_star_mul_self] + simp [hb, mul_add, mul_sub, add_mul, sub_mul] + grind + have hax : star a * x = 0 := by simpa [star_mul] using congr(star $hxa) + /- Similarly, guided by the formal `star a = (1 - p) * star b * (1 - q)`, we obtain + the following by substitution and expansion. -/ + have hpa : p * (star a * a) = 0 := by + simp only [hb, mul_add, mul_sub, star_add, star_sub, star_mul, add_mul, sub_mul] + grind [star_star_mul x x] + -- The facts `hxa` and `hax` yield that cross terms vanish. + have : star (x + a) * (x + a) = p + star a * a := by simp [hp, mul_add, add_mul, hax, hxa] + -- This, the C⋆-identity and `hpa` obtain + have : ‖p + star a * a‖ = ‖x + a‖ * ‖x + a‖ := by rw [← this, CStarRing.norm_star_mul_self] + /- Since `p` and `star a * a` are self-adjoint + with product zero that the norm of their sum is the max of the norms of these contractions. -/ + have hmax : ‖p + star a * a‖ ≤ 1 := by + rw [IsSelfAdjoint.star_mul_self x |>.norm_add_eq_max (.star_mul_self a) hpa, sup_le_iff] + simp only [CStarRing.norm_star_mul_self] + grw [mem_closedBall_zero_iff.mp hx.1, mem_closedBall_zero_iff.mp hx.1, + mem_closedBall_zero_iff.mp ha, mem_closedBall_zero_iff.mp ha, one_mul, and_self] + have : ‖x + a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by grind + /- Using `hxa` and `hax`, cross terms vanish and we have + `‖x - a‖ * ‖x - a‖ = ‖p + star a * a‖ ≤ 1`. -/ + have : ‖x - a‖ ≤ 1 := sq_le_one_iff₀ (by positivity) |>.mp <| by + simp [sq, ← CStarRing.norm_star_mul_self, sub_mul, mul_sub, hax, hxa, ← hp, hmax] + rw [mem_extremePoints_iff_left] at hx + exact add_eq_left.mp <| @hx.2 (x + a) (by simpa) (x - a) (by simpa) + ⟨2⁻¹, 2⁻¹, by simp [smul_add, smul_sub, ← add_smul, ← one_div]⟩ + +open Filter Topology in +/-- When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra, +then `star x * x + x * star x - x * star x * star x * x` is a right identity. +(See also `CStarAlgebra.ofExtremePtOne_mul` for the left identity.) -/ +theorem CStarAlgebra.mul_ofExtremePtOne {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) + (a : A) : a * (star x * x + x * star x - x * star x * (star x * x)) = a := by + let := spectralOrder A + let := spectralOrderedRing A + let u := approximateUnit A + let hu := increasingApproximateUnit A + let f (t : A) : A := t - t * (star x * x) - x * star x * t + x * star x * t * (star x * x) + have h (t : A) : f t = 0 := by + simpa using eq_zero_of_eq_sub_of_mem_closedBall_of_mem_extremePoints_closedUnitBall + hx (inv_norm_smul_mem_unitClosedBall (f t)) (b := ‖f t‖⁻¹ • t) + (by simp [← mul_assoc, smul_mul_assoc, mul_smul_comm, sub_sub, ← smul_sub, ← smul_add, f]) + have h_tendsto : Tendsto (fun t ↦ a * f t) u + (𝓝 (a - a * (star x * x + x * star x - x * star x * (star x * x)))) := by + conv => enter [1, t]; simp only [f]; rw [sub_add, sub_sub, add_sub, mul_sub] + apply_rules [Tendsto.sub, Tendsto.add, hu.tendsto_mul_left, hu.tendsto_mul_right, + Tendsto.mul_const, Tendsto.const_mul] + simpa [h, sub_eq_zero, eq_comm (a := (0 : A)), eq_comm (a := a)] using h_tendsto + +@[simp] +theorem star_mem_extremePoints_closedBall_zero_iff {A : Type*} [NonUnitalSeminormedRing A] + [StarRing A] [NormedStarGroup A] [Module ℝ A] [StarModule ℝ A] {x : A} (c : ℝ) : + star x ∈ extremePoints ℝ (closedBall 0 c) ↔ x ∈ extremePoints ℝ (closedBall 0 c) := by + suffices ∀ x : A, x ∈ extremePoints ℝ (closedBall 0 c) → star x ∈ extremePoints ℝ (closedBall 0 c) + from ⟨fun h ↦ star_star x ▸ this (star x) h, this x⟩ + refine fun x hx ↦ ⟨by simpa using hx.1, fun y hy z hz ⟨α, β, hα, hβ, hαβ, hxyz⟩ ↦ ?_⟩ + rw [eq_star_iff_eq_star, eq_comm] at hxyz ⊢ + rw [mem_extremePoints_iff_left] at hx + apply @hx.2 _ (by simpa using hy) (star z) (by simpa using hz) ⟨star α, star β, ?_⟩ + simp [← hxyz, hα, hβ, hαβ] + +/-- When `x` is an extreme point of the closed unit ball in an a priori non-unital C⋆-algebra, +then `star x * x + x * star x - x * star x * star x * x` is a left identity. +(See also `CStarAlgebra.mul_ofExtremePtOne` for the right identity.) -/ +theorem CStarAlgebra.ofExtremePtOne_mul {x : A} (hx : x ∈ extremePoints ℝ (closedBall 0 1)) + (a : A) : (star x * x + x * star x - x * star x * (star x * x)) * a = a := by + simpa [add_comm] using congr(star $(mul_ofExtremePtOne (x := star x) (by simpa) (star a))) + +/-- A C⋆-algebra is unital iff there exists an extreme point of the closed unit ball. + +To upgrade a non-unital C⋆-algebra to a unital one, use `IsUnital.toCStarAlgebra`. -/ +theorem CStarAlgebra.isUnital_iff : + IsUnital A ↔ (extremePoints ℝ (closedBall (0 : A) 1)).Nonempty := by + rw [nonempty_def] + refine ⟨fun h ↦ let := h.toCStarAlgebra; ⟨1, one_mem_extremePoints_unitClosedBall⟩, ?_⟩ + exact fun ⟨x, hx⟩ ↦ ⟨_, fun y ↦ ⟨ofExtremePtOne_mul hx y, mul_ofExtremePtOne hx y⟩⟩ + +theorem CStarAlgebra.isNotUnital_iff : + IsNotUnital A ↔ extremePoints ℝ (closedBall (0 : A) 1) = ∅ := by + simpa [not_nonempty_iff_eq_empty] using isUnital_iff.not + /-- The star projections in a non-unital C⋆-algebra are exactly the extreme points of the nonnegative closed unit ball. -/ theorem isStarProjection_iff_mem_extremePoints_setOfPred_nonneg_inter_unitClosedBall