MathlibAnnex/Analysis/CStarAlgebra/FacialStructure/ExtremeDecomposition.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.FunctionalRealization7import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.ExtremeCoefficient8import MathlibAnnex.Analysis.CStarAlgebra.FacialStructure.PositiveTranslateUniqueness910/-!11# Pure-state and unitary decomposition of arbitrary extreme dual functionals1213Start with an arbitrary extreme point of the dual unit ball of a nontrivial,14possibly nonunital C-star algebra. The actual Hahn--Banach/auxiliary-GNS model15is compressed to the original-algebra closed orbit. Its two unit vectors,16coefficient recovery and original-algebra cyclicity are proved in17`FunctionalRealization`; the existing extreme-coefficient criterion then18makes this actual representation irreducible. Unitary transitivity gives a19pure positive translate. The positive state is unique, not its translating20unitary. No extremality of the Hahn--Banach extension is used.2122This closes the existence and state-uniqueness assertions of Notes 11.9.23It does not assert maximality of the support slice or a singleton of all24supporting functionals; those require the later slice-separation theorem.25-/2627set_option autoImplicit false28noncomputable section29open Set Metric30open scoped CStarAlgebra ComplexOrder3132namespace MathlibAnnex.Analysis.CStarAlgebra3334universe u35variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]3637/-- The explicitly constructed original-algebra cyclic representation of an38arbitrary extreme dual functional is nonzero and irreducible. -/39theorem NonUnitalFunctional.isIrreducible_cyclicRepresentation40    (rho : StrongDual ℂ A) (hrho : rho ≠ 0)41    (hext : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :42    (NonUnitalFunctional.cyclicRepresentation rho hrho).IsIrreducible := by43  have hn := norm_eq_one_of_mem_extremePoints_dual_closedBall hext44  have hx := NonUnitalFunctional.norm_cyclicSourceVector rho hrho45  have hy := NonUnitalFunctional.norm_cyclicTargetVector rho hrho46  have hcoeff := NonUnitalFunctional.matrixCoefficient_cyclicRepresentation_of_norm_eq_one47    rho hrho hn48  apply NonUnitalCStarRepresentation.isIrreducible_of_extreme_matrixCoefficient_of_denseRange49    (NonUnitalFunctional.cyclicRepresentation rho hrho)50    (NonUnitalFunctional.cyclicSourceVector rho hrho)51    (NonUnitalFunctional.cyclicTargetVector rho hrho) hx hy52  · rwa [hcoeff]53  · rwa [hcoeff]54  · exact NonUnitalFunctional.denseRange_cyclicRepresentation rho hrho5556variable [PartialOrder A] [StarOrderedRing A]5758/-- Every extreme dual unit functional is a unitary translate of a genuine59pure nonunital state. Existence is proved from the arbitrary extreme point,60not from a pre-existing positive translate or irreducible realization. -/61theorem exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall62    {rho : StrongDual ℂ A}63    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :64    ∃ phi : StrongDual ℂ A, IsPureNonUnitalState A phi ∧65      ∃ u : unitary (Unitization ℂ A),66        unitaryTranslate u rho = phi ∧ rho = unitaryTranslate (star u) phi := by67  have hn := norm_eq_one_of_mem_extremePoints_dual_closedBall hrho68  have hne : rho ≠ 0 := norm_ne_zero_iff.mp (by rw [hn]; exact one_ne_zero)69  have hpi := NonUnitalFunctional.isIrreducible_cyclicRepresentation rho hne hrho70  have hx := NonUnitalFunctional.norm_cyclicSourceVector rho hne71  have hy := NonUnitalFunctional.norm_cyclicTargetVector rho hne72  have hcoeff := NonUnitalFunctional.matrixCoefficient_cyclicRepresentation_of_norm_eq_one73    rho hne hn74  obtain ⟨u, hu, hpure, hrecover⟩ :=75    NonUnitalCStarRepresentation.exists_unitaryTranslate_eq_pureState_of_isIrreducible76      (NonUnitalFunctional.cyclicRepresentation rho hne) hpi77      (NonUnitalFunctional.cyclicSourceVector rho hne)78      (NonUnitalFunctional.cyclicTargetVector rho hne) hx hy79  refine ⟨_, hpure, u, ?_, ?_⟩80  · simpa only [hcoeff] using hu81  · simpa only [hcoeff] using hrecover8283/-- The positive pure state in the unitary decomposition is unique.84The unitary is existentially quantified inside the unique-state property. -/85theorem existsUnique_pureState_unitaryTranslate86    {rho : StrongDual ℂ A}87    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :88    ∃! phi : StrongDual ℂ A, IsPureNonUnitalState A phi ∧89      ∃ u : unitary (Unitization ℂ A),90        unitaryTranslate u rho = phi ∧ rho = unitaryTranslate (star u) phi := by91  obtain ⟨phi, hphi, u, hu, hrecover⟩ :=92    exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall hrho93  refine ⟨phi, ⟨hphi, u, hu, hrecover⟩, ?_⟩94  rintro psi ⟨hpsi, v, hv, _⟩95  have hu0 : ∀ a : A, 0 ≤ a → 0 ≤ unitaryTranslate u rho a := by96    intro a ha97    rw [hu]98    exact hphi.1.1 a ha99  have hv0 : ∀ a : A, 0 ≤ a → 0 ≤ unitaryTranslate v rho a := by100    intro a ha101    rw [hv]102    exact hpsi.1.1 a ha103  calc104    psi = unitaryTranslate v rho := hv.symm105    _ = unitaryTranslate u rho :=106      unitaryTranslate_eq_of_nonneg_of_mem_extremePoints_dual_closedBall hrho v u hv0 hu0107    _ = phi := hu108109/-- Every extreme dual unit functional attains the value one at a norm-one110member of the original algebra, not merely of its unitization. -/111theorem exists_norm_eq_one_apply_eq_one_of_mem_extremePoints_dual_closedBall112    {rho : StrongDual ℂ A}113    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :114    ∃ a : A, ‖a‖ = 1 ∧ rho a = 1 := by115  obtain ⟨phi, hphi, u, hu, _⟩ :=116    exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall hrho117  apply exists_norm_eq_one_apply_eq_one_of_nonneg_unitaryTranslate u hrho118  intro a ha119  rw [hu]120  exact hphi.1.1 a ha121122/-- The shared value-one slice of an arbitrary extreme dual functional is123nonempty. No maximality or support-uniqueness claim is part of this theorem. -/124theorem nonempty_unitBallSupportFace_of_mem_extremePoints_dual_closedBall125    {rho : StrongDual ℂ A}126    (hrho : rho ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :127    (NormedSpace.unitBallSupportFace ℂ rho).Nonempty := by128  obtain ⟨a, ha, hval⟩ := exists_norm_eq_one_apply_eq_one_of_mem_extremePoints_dual_closedBall hrho129  exact ⟨a, mem_closedBall_zero_iff.mpr ha.le, hval⟩130131end MathlibAnnex.Analysis.CStarAlgebra