MathlibAnnex/Analysis/CStarAlgebra/FacialStructure/ExtremeMaximalFace.lean

Exact source · gss-v0.5.0

Fixed commit original · Raw UTF-8 source · Back to GSS Companion

Select a source link from a manuscript to highlight its exact range.

1/-2Copyright (c) 2026 Ryotaro Tanaka. All rights reserved.3Released under Apache 2.0 license as described in the file LICENSE.4Authors: Ryotaro Tanaka5-/6import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.ExtremeSliceSeparation7import MathlibAnnex.Analysis.Normed.GeometricStructure.WeakStarMaximalFace89/-!10# Maximal faces and their entire supporting families1112For a nontrivial possibly nonunital C-star algebra, the maximal proper faces13of the closed unit ball are exactly the value-one slices of extreme dual14unit functionals. Every such slice has exactly one supporting functional in15the entire closed dual ball.1617The latter conclusion is not obtained by renaming uniqueness among extreme18points. We identify the intersection of the actual weak-star support family19with the extreme dual ball and apply the received weak-star Krein--Milman20identity. The resulting singleton is then carried back to the original21`supportFunctionals`. All face and support definitions are imported from MAIN.22-/2324set_option autoImplicit false25set_option maxHeartbeats 200000026set_option synthInstance.maxHeartbeats 20000027noncomputable section28open Set Metric29open scoped CStarAlgebra ComplexOrder3031namespace MathlibAnnex.Analysis.CStarAlgebra3233universe u34variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]35variable [PartialOrder A] [StarOrderedRing A]3637/-- The converse half of Notes 11.14: the slice of an arbitrary extreme38functional is a maximal proper face, not merely a nonempty exposed face. -/39theorem isMaximalFace_unitBallSupportFace_of_mem_extremePoints_dual_closedBall40    {rho : StrongDual ℂ A}41    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :42    NormedSpace.IsMaximalFace (NormedSpace.unitBallSupportFace ℂ rho) := by43  have hn := norm_eq_one_of_mem_extremePoints_dual_closedBall hrho44  obtain ⟨G, hFG, hG⟩ := NormedSpace.exists_isMaximalFace_of_convex_subset_sphere45    (nonempty_unitBallSupportFace_of_mem_extremePoints_dual_closedBall hrho)46    (NormedSpace.convex_unitBallSupportFace ℂ rho)47    (NormedSpace.unitBallSupportFace_subset_sphere ℂ hn.le)48  obtain ⟨tau, _, htau, hGtau⟩ := hG.exists_extreme_eq_unitBallSupportFace ℂ49  have heq : rho = tau :=50    eq_of_unitBallSupportFace_subset_of_mem_extremePoints_dual_closedBall hrho htau51      (by simpa only [hGtau] using hFG)52  rw [heq]53  rwa [hGtau] at hG5455/-- The actual weak-star support family of an extreme slice has one point.56The closure and convex hull here are explicitly in WeakDual, not StrongDual. -/57theorem weakStarSupportFunctionals_unitBallSupportFace_eq_singleton58    {rho : StrongDual ℂ A}59    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :60    NormedSpace.weakStarSupportFunctionals ℂ (NormedSpace.unitBallSupportFace ℂ rho) =61      {rho.toWeakDual} := by62  let F : Set A := NormedSpace.unitBallSupportFace ℂ rho63  have hn := norm_eq_one_of_mem_extremePoints_dual_closedBall hrho64  have hball : F ⊆ closedBall (0 : A) 1 := fun _ hx => hx.165  have hrs : rho ∈ NormedSpace.supportFunctionals ℂ F :=66    ⟨hn.le, fun _ hx => hx.2⟩67  have hinter : NormedSpace.weakStarSupportFunctionals ℂ F ∩68      (WeakDual.toStrongDual ⁻¹' closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ =69        {rho.toWeakDual} := by70    ext f71    constructor72    · rintro ⟨hf, hext⟩73      have hext' := (NormedSpace.mem_extremePoints_closedBall_toStrongDual_iff ℂ f).mpr hext74      have heq : rho = f.toStrongDual :=75        eq_of_unitBallSupportFace_subset_of_mem_extremePoints_dual_closedBall hrho hext'76          (fun a ha => ⟨ha.1, hf.2 a ha⟩)77      apply Set.mem_singleton_iff.mpr78      exact (congrArg (fun g : StrongDual ℂ A => g.toWeakDual) heq).symm79    · intro hf80      have hfr : f = StrongDual.toWeakDual rho := Set.mem_singleton_iff.mp hf81      rw [hfr]82      exact ⟨hrs, (NormedSpace.mem_extremePoints_closedBall_toStrongDual_iff83        ℂ (StrongDual.toWeakDual rho)).mp hrho⟩84  have hkm := NormedSpace.closure_convexHull_inter_extremePoints_closedBall_weakStarSupportFunctionals85    ℂ hball86  rw [hinter, convexHull_singleton, closure_singleton] at hkm87  exact hkm.symm8889/-- The full supporting family, including nonextreme functionals, is a90singleton. This is the complete uniqueness assertion in Notes 11.14. -/91theorem supportFunctionals_unitBallSupportFace_eq_singleton92    {rho : StrongDual ℂ A}93    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :94    NormedSpace.supportFunctionals ℂ (NormedSpace.unitBallSupportFace ℂ rho) = {rho} := by95  rw [← NormedSpace.image_toStrongDual_weakStarSupportFunctionals,96    weakStarSupportFunctionals_unitBallSupportFace_eq_singleton hrho,97    Set.image_singleton]98  rfl99100/-- The maximal proper faces of the original algebra's unit ball are exactly101its extreme dual value-one slices. -/102theorem isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall (F : Set A) :103    NormedSpace.IsMaximalFace F ↔ ∃ rho : StrongDual ℂ A,104      rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ∧105        F = NormedSpace.unitBallSupportFace ℂ rho := by106  constructor107  · intro hF108    obtain ⟨rho, _, hrho, hFrho⟩ := hF.exists_extreme_eq_unitBallSupportFace ℂ109    exact ⟨rho, hrho, hFrho⟩110  · rintro ⟨rho, hrho, rfl⟩111    exact isMaximalFace_unitBallSupportFace_of_mem_extremePoints_dual_closedBall hrho112113/-- A maximal proper face has exactly one extreme value-one representation,114and its entire supporting family consists of that same functional. -/115theorem existsUnique_extreme_support_of_isMaximalFace {F : Set A}116    (hF : NormedSpace.IsMaximalFace F) :117    ∃! rho : StrongDual ℂ A,118      rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ ∧119        F = NormedSpace.unitBallSupportFace ℂ rho ∧120          NormedSpace.supportFunctionals ℂ F = {rho} := by121  obtain ⟨rho, hrho, hFrho⟩ :=122    (isMaximalFace_iff_exists_mem_extremePoints_dual_closedBall F).mp hF123  have hs : NormedSpace.supportFunctionals ℂ F = {rho} := by124    rw [hFrho]125    exact supportFunctionals_unitBallSupportFace_eq_singleton hrho126  refine ⟨rho, ⟨hrho, hFrho, hs⟩, ?_⟩127  rintro tau ⟨_, _, hst⟩128  have hmem : tau ∈ ({rho} : Set (StrongDual ℂ A)) := by129    rw [← hs, hst]130    exact Set.mem_singleton tau131  exact Set.mem_singleton_iff.mp hmem132133end MathlibAnnex.Analysis.CStarAlgebra