MathlibAnnex/Analysis/CStarAlgebra/FacialStructure/PureStateExtreme.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.UnitCoefficient7import MathlibAnnex.Analysis.CStarAlgebra.PureStateGNS.PureIrreducible89/-!10# Pure nonunital states as extreme dual functionals1112This bridge uses the actual GNS representation of the canonical extension,13restricted back to A, and its actual unit GNS vector. Nonzeroness of the14restricted action follows from the recovered norm-one state. The final15extremality is extremality in the whole dual ball, not just in the state space.16-/1718set_option autoImplicit false19noncomputable section20open Set Metric21open scoped CStarAlgebra ComplexOrder2223namespace MathlibAnnex.Analysis.CStarAlgebra2425variable {A : Type*} [NonUnitalCStarAlgebra A]26variable [PartialOrder A] [StarOrderedRing A]2728/-- A pure norm-one positive functional is extreme in the entire dual unit ball. -/29theorem mem_extremePoints_dual_closedBall_of_isPureNonUnitalState30    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :31    phi ∈ (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ := by32  have hphi : phi ∈ nonUnitalStateSpace A := by33    rw [IsPureNonUnitalState, mem_extremePoints_iff_left] at hpure34    exact hpure.135  let Phi : StrongDual ℂ (Unitization ℂ A) := unitizationExtension phi36  have hPhi : Phi ∈ stateSpace (Unitization ℂ A) :=37    unitizationExtension_mem_stateSpace phi hphi38  have hPhiPure : IsPureState (Unitization ℂ A) Phi :=39    isPureState_unitizationExtension phi hphi hpure40  let f : Unitization ℂ A →ₚ[ℂ] ℂ := positiveLinearMapOfMemStateSpace Phi hPhi41  let xi : f.GNS := stateGNSVector Phi hPhi42  have hxi : ‖xi‖ = 1 := norm_stateGNSVector Phi hPhi43  have hxi0 : xi ≠ 0 := by44    intro hz45    simpa [hz] using hxi46  letI : Nontrivial f.GNS := ⟨⟨xi, 0, hxi0⟩⟩47  let rho : Representation (Unitization ℂ A) f.GNS := f.gnsStarAlgHom48  let pi : NonUnitalCStarRepresentation A f.GNS :=49    rho.toNonUnitalStarAlgHom.comp (Unitization.inrNonUnitalStarAlgHom ℂ A)50  have hcoeff : NonUnitalCStarRepresentation.matrixCoefficient pi xi xi = phi := by51    ext a52    change inner ℂ (stateGNSVector Phi hPhi)53      ((positiveLinearMapOfMemStateSpace Phi hPhi).gnsStarAlgHom54        (Unitization.inr a) (stateGNSVector Phi hPhi)) = phi a55    rw [inner_gnsStarAlgHom_stateGNSVector]56    exact unitizationExtension_inr phi a57  have hrho : rho.IsIrreducible := by58    apply (Representation.isIrreducible_iff_starAlgHom rho).259    exact MathlibAnnex.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom Phi hPhi hPhiPure60  have hnonzero : pi.IsNonzero := by61    change ∃ a : A, pi a ≠ 062    by_contra! hz63    have hzero : phi = 0 := by64      rw [← hcoeff]65      ext a66      simp only [NonUnitalCStarRepresentation.matrixCoefficient_apply, hz a,67        ContinuousLinearMap.zero_apply, inner_zero_right]68    have hn := hphi.269    rw [hzero, norm_zero] at hn70    norm_num at hn71  have hpi : pi.IsIrreducible :=72    NonUnitalCStarRepresentation.isIrreducible_restriction_of_isIrreducible_unitization73      rho hrho hnonzero74  rw [← hcoeff]75  exact NonUnitalCStarRepresentation.matrixCoefficient_mem_extremePoints_dual_closedBall_of_isIrreducible76    pi hpi xi xi hxi hxi7778end MathlibAnnex.Analysis.CStarAlgebra