MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/AbsoluteState.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.NonUnitalStateGNS7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.RepresentationComponents8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.PureStateKernel910/-!11# Absolute pure states, their GNS representations, and components1213`extremeAbsoluteState` is the positive state singled out by the already proved14unitary-translate existence and uniqueness. It is not an arbitrary norming state15or a definition of the component relation. Its representation below is literally16the GNS representation of its canonical extension restricted to the original A.17The kernel of a functional and the kernel of a representation remain distinct.1819The component statements use the received `Related`, the whole coefficient20family, and the existing gamma. No topological comparison with an irreducible21spectrum, self-adjoint-part assertion, or zero-algebra extension is claimed here.22-/2324set_option autoImplicit false25noncomputable section26open Set Metric27open scoped CStarAlgebra ComplexOrder2829namespace MathlibAnnex.Analysis.CStarAlgebra3031universe u v32variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]33variable [PartialOrder A] [StarOrderedRing A]3435private def absoluteStateContinuousMap {H : Type v}36    [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]37    (pi : NonUnitalCStarRepresentation A H) : A →L[ℂ] (H →L[ℂ] H) :=38  LinearMap.mkContinuous39    { toFun := pi, map_add' := map_add pi, map_smul' := map_smul pi }40    1 (fun a => by41      change ‖pi a‖ ≤ 1 * ‖a‖42      simpa only [one_mul] using NonUnitalStarAlgHom.norm_apply_le pi a)4344/-- The unique positive pure state in an extreme functional's unitary decomposition.45Only the state is made into a definition; translating unitaries need not be unique. -/46def extremeAbsoluteState (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :47    StrongDual ℂ A :=48  (exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall rho.property).choose4950theorem isPureNonUnitalState_extremeAbsoluteState51    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :52    IsPureNonUnitalState A (extremeAbsoluteState rho) :=53  (exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall rho.property).choose_spec.15455/-- Existence of a translating unitary and the exact inverse formula. -/56theorem exists_unitaryTranslate_eq_extremeAbsoluteState57    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :58    ∃ u : unitary (Unitization ℂ A),59      unitaryTranslate u rho.val = extremeAbsoluteState rho ∧60        rho.val = unitaryTranslate (star u) (extremeAbsoluteState rho) :=61  (exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall rho.property).choose_spec.26263/-- Any positive pure translate is this state. This uses the received uniqueness64proof, rather than choosing one unitary and claiming it to be unique. -/65theorem eq_extremeAbsoluteState_of_unitaryTranslate_eq66    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ)67    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi)68    (u : unitary (Unitization ℂ A)) (hu : unitaryTranslate u rho.val = phi) :69    phi = extremeAbsoluteState rho := by70  obtain ⟨v, hv, -⟩ := exists_unitaryTranslate_eq_extremeAbsoluteState rho71  have hnonneg : ∀ a : A, 0 ≤ a → 0 ≤ unitaryTranslate u rho.val a := by72    intro a ha73    rw [hu]74    exact hpure.1.1 a ha75  have hnonneg' : ∀ a : A, 0 ≤ a → 0 ≤ unitaryTranslate v rho.val a := by76    intro a ha77    rw [hv]78    exact (isPureNonUnitalState_extremeAbsoluteState rho).1.1 a ha79  exact hu.symm.trans ((unitaryTranslate_eq_of_nonneg_of_mem_extremePoints_dual_closedBall80    rho.property u v hnonneg hnonneg').trans hv)8182/-- The actual canonical-extension GNS space of the absolute state. -/83abbrev ExtremeGNSHilbertSpace84    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :=85  NonUnitalStateGNS.Space (extremeAbsoluteState rho)86    (isPureNonUnitalState_extremeAbsoluteState rho).18788/-- The actual absolute-state GNS action of the original algebra. -/89def extremeGNSRepresentation90    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :91    NonUnitalCStarRepresentation A (ExtremeGNSHilbertSpace rho) :=92  NonUnitalStateGNS.representation (extremeAbsoluteState rho)93    (isPureNonUnitalState_extremeAbsoluteState rho).19495theorem isIrreducible_extremeGNSRepresentation96    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :97    (extremeGNSRepresentation rho).IsIrreducible :=98  NonUnitalStateGNS.isIrreducible_representation (extremeAbsoluteState rho)99    (isPureNonUnitalState_extremeAbsoluteState rho).1100    (isPureNonUnitalState_extremeAbsoluteState rho)101102/-- An arbitrary extreme functional is recovered by unit vectors in the GNS103of its absolute state, not merely in an auxiliary cyclic coefficient model. -/104theorem exists_unit_vectors_matrixCoefficient_extremeGNSRepresentation_eq105    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :106    ∃ x y : ExtremeGNSHilbertSpace rho, ‖x‖ = 1 ∧ ‖y‖ = 1 ∧107      NonUnitalCStarRepresentation.matrixCoefficient (extremeGNSRepresentation rho) x y = rho.val := by108  obtain ⟨u, -, hrep⟩ := exists_unitaryTranslate_eq_extremeAbsoluteState rho109  obtain ⟨x, y, hx, hy, hcoeff⟩ :=110    NonUnitalStateGNS.exists_unit_vectors_matrixCoefficient_eq_unitaryTranslate111      (extremeAbsoluteState rho) (isPureNonUnitalState_extremeAbsoluteState rho).1112      (isPureNonUnitalState_extremeAbsoluteState rho) (star u)113  exact ⟨x, y, hx, hy, hcoeff.trans hrep.symm⟩114115/-- The corresponding equality of actual GSS points. -/116theorem exists_matrixCoefficientKernel_extremeGNSRepresentation_eq117    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :118    ∃ (x y : ExtremeGNSHilbertSpace rho) (hx : x ≠ 0) (hy : y ≠ 0),119      NonUnitalCStarRepresentation.matrixCoefficientKernel (extremeGNSRepresentation rho)120        (isIrreducible_extremeGNSRepresentation rho) x y hx hy = extremeKernel rho := by121  obtain ⟨x, y, hx, hy, hcoeff⟩ := exists_unit_vectors_matrixCoefficient_extremeGNSRepresentation_eq rho122  have hx0 : x ≠ 0 := norm_ne_zero_iff.mp (by rw [hx]; exact one_ne_zero)123  have hy0 : y ≠ 0 := norm_ne_zero_iff.mp (by rw [hy]; exact one_ne_zero)124  refine ⟨x, y, hx0, hy0, ?_⟩125  apply Subtype.ext126  change ((NonUnitalCStarRepresentation.matrixCoefficient (extremeGNSRepresentation rho) x y).ker : Set A) = _127  rw [hcoeff]128  rfl129130/-- The auxiliary representation, or any other irreducible coefficient realization131of a kernel, is equivalent to the actual GNS of the absolute state. The equality132branch is justified by the proved inequivalent-kernel separation. -/133theorem unitaryEquivalent_extremeGNSRepresentation_of_matrixCoefficientKernel_eq134    {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]135    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible)136    (x y : H) (hx : x ≠ 0) (hy : y ≠ 0)137    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ)138    (hker : NonUnitalCStarRepresentation.matrixCoefficientKernel pi hpi x y hx hy = extremeKernel rho) :139    pi.UnitaryEquivalent (extremeGNSRepresentation rho) := by140  obtain ⟨z, w, hz, hw, hpoint⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq rho141  exact NonUnitalCStarRepresentation.unitaryEquivalent_of_linked_matrixCoefficientKernel142    pi (extremeGNSRepresentation rho) hpi (isIrreducible_extremeGNSRepresentation rho)143    x y z w hx hy hz hw (Or.inl (hker.trans hpoint.symm))144145/-- Paper 5.8 in its absolute-state GNS form, using the original component relation. -/146theorem related_extremeKernel_iff_unitaryEquivalent_extremeGNSRepresentation147    (rho tau : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :148    (NormedSpace.geometricStructureClosure ℂ A).Related (extremeKernel rho) (extremeKernel tau) ↔149      (extremeGNSRepresentation rho).UnitaryEquivalent (extremeGNSRepresentation tau) := by150  obtain ⟨x, y, hx, hy, hrho⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq rho151  obtain ⟨z, w, hz, hw, htau⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq tau152  rw [← hrho, ← htau]153  exact NonUnitalCStarRepresentation.related_matrixCoefficientKernel_iff_unitaryEquivalent154    (extremeGNSRepresentation rho) (extremeGNSRepresentation tau)155    (isIrreducible_extremeGNSRepresentation rho) (isIrreducible_extremeGNSRepresentation tau)156    x y z w hx hy hz hw157158/-- Paper 5.9: ker(rho) and ker(abs(rho)) lie in the same actual component. -/159theorem related_extremeKernel_extremeAbsoluteState160    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :161    (NormedSpace.geometricStructureClosure ℂ A).Related (extremeKernel rho)162      (extremeKernel ⟨extremeAbsoluteState rho,163        mem_extremePoints_dual_closedBall_of_isPureNonUnitalState _164          (isPureNonUnitalState_extremeAbsoluteState rho)⟩) := by165  obtain ⟨x, y, hx, hy, hpoint⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq rho166  let phi := extremeAbsoluteState rho167  have hpure : IsPureNonUnitalState A phi := isPureNonUnitalState_extremeAbsoluteState rho168  let xi := NonUnitalStateGNS.vector phi hpure.1169  have hxi : xi ≠ 0 := norm_ne_zero_iff.mp (by rw [NonUnitalStateGNS.norm_vector]; exact one_ne_zero)170  have hstate : NonUnitalCStarRepresentation.matrixCoefficientKernel171      (extremeGNSRepresentation rho) (isIrreducible_extremeGNSRepresentation rho) xi xi hxi hxi =172        extremeKernel ⟨extremeAbsoluteState rho,173          mem_extremePoints_dual_closedBall_of_isPureNonUnitalState _ hpure⟩ := by174    apply Subtype.ext175    change ((NonUnitalCStarRepresentation.matrixCoefficient176      (NonUnitalStateGNS.representation phi hpure.1) xi xi).ker : Set A) = (phi.ker : Set A)177    rw [NonUnitalStateGNS.matrixCoefficient_representation]178  rw [← hpoint, ← hstate]179  exact NonUnitalCStarRepresentation.related_matrixCoefficientKernel180    (extremeGNSRepresentation rho) (isIrreducible_extremeGNSRepresentation rho)181    x y xi xi hx hy hxi hxi182183/-- Paper 5.10: the WHOLE component is the family of absolute-state GNS coefficient kernels. -/184theorem component_extremeKernel_eq_matrixCoefficientKernelFamily185    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :186    (NormedSpace.geometricStructureClosure ℂ A).component (extremeKernel rho) =187      NonUnitalCStarRepresentation.matrixCoefficientKernelFamily (extremeGNSRepresentation rho)188        (isIrreducible_extremeGNSRepresentation rho) := by189  obtain ⟨x, y, hx, hy, hpoint⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq rho190  rw [← hpoint]191  exact NonUnitalCStarRepresentation.component_matrixCoefficientKernel_eq_family192    (extremeGNSRepresentation rho) (isIrreducible_extremeGNSRepresentation rho) x y hx hy193194/-- The component intersection on the received geometric spectrum is the actual195representation kernel of the absolute-state GNS action. -/196theorem geometricSpectrumKernel_toGeometricSpectrum_extremeKernel197    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :198    NormedSpace.geometricSpectrumKernel ℂ A (NormedSpace.toGeometricSpectrum ℂ A (extremeKernel rho)) =199      ((absoluteStateContinuousMap (extremeGNSRepresentation rho)).ker : Set A) := by200  obtain ⟨x, y, hx, hy, hpoint⟩ := exists_matrixCoefficientKernel_extremeGNSRepresentation_eq rho201  rw [← hpoint]202  exact NonUnitalCStarRepresentation.geometricSpectrumKernel_toGeometricSpectrum_matrixCoefficientKernel203    (extremeGNSRepresentation rho) (isIrreducible_extremeGNSRepresentation rho) x y hx hy204205/-- Literal gamma interface for subsequent spectral-topology work; no injectivity206of gamma and no comparison topology are concluded from this equality. -/207theorem geometricSpectrumToPrimitive_toGeometricSpectrum_extremeKernel_val208    (rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ) :209    (NormedSpace.geometricSpectrumToPrimitive ℂ A210      (NormedSpace.toGeometricSpectrum ℂ A (extremeKernel rho))).val =211      ((absoluteStateContinuousMap (extremeGNSRepresentation rho)).ker : Set A) := by212  rw [NormedSpace.geometricSpectrumToPrimitive_val]213  exact geometricSpectrumKernel_toGeometricSpectrum_extremeKernel rho214215/-- Every actual geometric-spectrum point has an extreme kernel representative. -/216theorem exists_toGeometricSpectrum_extremeKernel_eq (C : NormedSpace.GeometricSpectrum ℂ A) :217    ∃ rho : (closedBall (0 : StrongDual ℂ A) 1).extremePoints ℝ,218      NormedSpace.toGeometricSpectrum ℂ A (extremeKernel rho) = C := by219  obtain ⟨I, rfl⟩ := NormedSpace.toGeometricSpectrum_surjective ℂ A C220  obtain ⟨rho, rfl⟩ := extremeKernel_surjective I221  exact ⟨rho, rfl⟩222223/-- A pure state is its own absolute state; translation by the unit gives the224positive translate to which the proved uniqueness applies. -/225theorem extremeAbsoluteState_eq_of_isPureNonUnitalState226    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :227    extremeAbsoluteState ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩ = phi := by228  symm229  apply eq_extremeAbsoluteState_of_unitaryTranslate_eq _ phi hpure 1230  exact unitaryTranslate_one phi231232/-- The final assertion of Paper 5.9, stated with the correct type: every233geometric-spectrum component contains a PURE-STATE KERNEL point of S(A). -/234theorem exists_pureState_kernel_mem_geometricSpectrum (C : NormedSpace.GeometricSpectrum ℂ A) :235    ∃ (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi),236      extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩ ∈ C.val := by237  obtain ⟨rho, rfl⟩ := exists_toGeometricSpectrum_extremeKernel_eq C238  exact ⟨extremeAbsoluteState rho, isPureNonUnitalState_extremeAbsoluteState rho,239    related_extremeKernel_extremeAbsoluteState rho⟩240241/-- Paper 5.10 specialized literally to a pure state and its actual GNS242representation, not to a second chosen state having an equal component. -/243theorem component_pureStateKernel_eq_matrixCoefficientKernelFamily244    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :245    (NormedSpace.geometricStructureClosure ℂ A).component246      (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩) =247      NonUnitalCStarRepresentation.matrixCoefficientKernelFamily248        (NonUnitalStateGNS.representation phi hpure.1)249        (NonUnitalStateGNS.isIrreducible_representation phi hpure.1 hpure) := by250  let xi := NonUnitalStateGNS.vector phi hpure.1251  have hxi : xi ≠ 0 := norm_ne_zero_iff.mp (by rw [NonUnitalStateGNS.norm_vector]; exact one_ne_zero)252  have hk : NonUnitalCStarRepresentation.matrixCoefficientKernel253      (NonUnitalStateGNS.representation phi hpure.1)254      (NonUnitalStateGNS.isIrreducible_representation phi hpure.1 hpure) xi xi hxi hxi =255        extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩ := by256    apply Subtype.ext257    change ((NonUnitalCStarRepresentation.matrixCoefficient258      (NonUnitalStateGNS.representation phi hpure.1) xi xi).ker : Set A) = (phi.ker : Set A)259    rw [NonUnitalStateGNS.matrixCoefficient_representation]260  rw [← hk]261  exact NonUnitalCStarRepresentation.component_matrixCoefficientKernel_eq_family262    (NonUnitalStateGNS.representation phi hpure.1)263    (NonUnitalStateGNS.isIrreducible_representation phi hpure.1 hpure) xi xi hxi hxi264265/-- The unit-vector version of the whole component formula in Paper 5.10. -/266theorem component_pureStateKernel_eq_setOf_exists_unit_vectors267    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :268    (NormedSpace.geometricStructureClosure ℂ A).component269      (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩) =270      {I : NormedSpace.GeometricStructureSpace ℂ A |271        ∃ x y : NonUnitalStateGNS.Space phi hpure.1, ‖x‖ = 1 ∧ ‖y‖ = 1 ∧272          ((NonUnitalCStarRepresentation.matrixCoefficient273            (NonUnitalStateGNS.representation phi hpure.1) x y).ker : Set A) = I.val} := by274  rw [component_pureStateKernel_eq_matrixCoefficientKernelFamily phi hpure]275  ext I276  exact NonUnitalCStarRepresentation.mem_matrixCoefficientKernelFamily_iff_exists_unit_vectors277    (NonUnitalStateGNS.representation phi hpure.1)278    (NonUnitalStateGNS.isIrreducible_representation phi hpure.1 hpure) I279280/-- The pure-state form of J_C = ker(pi_phi) on the received gamma map. -/281theorem geometricSpectrumToPrimitive_toGeometricSpectrum_pureStateKernel_val282    (phi : StrongDual ℂ A) (hpure : IsPureNonUnitalState A phi) :283    (NormedSpace.geometricSpectrumToPrimitive ℂ A284      (NormedSpace.toGeometricSpectrum ℂ A285        (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩))).val =286      ((absoluteStateContinuousMap (NonUnitalStateGNS.representation phi hpure.1)).ker : Set A) := by287  change {a : A | ∀ I : NormedSpace.GeometricStructureSpace ℂ A,288    I ∈ (NormedSpace.geometricStructureClosure ℂ A).component289      (extremeKernel ⟨phi, mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hpure⟩) →290        a ∈ I.val} = _291  rw [component_pureStateKernel_eq_matrixCoefficientKernelFamily phi hpure]292  exact NonUnitalCStarRepresentation.setOf_forall_mem_matrixCoefficientKernelFamily_eq_ker293    (NonUnitalStateGNS.representation phi hpure.1)294    (NonUnitalStateGNS.isIrreducible_representation phi hpure.1 hpure)295296end MathlibAnnex.Analysis.CStarAlgebra