MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/PureStateKernel.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.PureStateExtreme7import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.ExtremeKernel89/-!10# Pure-state translates in the original geometric structure space1112Paper 5.3 is obtained from the received extreme-kernel family theorem and13Notes 11.9 in one direction, and genuine pure-state dual extremality in the14other. The parametrization uses actual subsets of A, so different phases15with the same kernel do not create different GSS points.16-/1718set_option autoImplicit false19noncomputable section20open Set Metric21open scoped CStarAlgebra ComplexOrder2223namespace MathlibAnnex.Analysis.CStarAlgebra2425variable {A : Type*} [NonUnitalCStarAlgebra A] [Nontrivial A]26variable [PartialOrder A] [StarOrderedRing A]2728/-- Paper 5.3: the original S(A) is the family of pure-state translate kernels. -/29theorem geometricStructureFamily_eq_setOf_exists_pureState_unitaryTranslate :30    NormedSpace.geometricStructureFamily ℂ A =31      {I : Set A | ∃ phi : StrongDual ℂ A, IsPureNonUnitalState A phi ∧32        ∃ u : unitary (Unitization ℂ A), ((unitaryTranslate u phi).ker : Set A) = I} := by33  ext I34  rw [mem_geometricStructureFamily_iff_exists_mem_extremePoints_dual_closedBall]35  constructor36  · rintro ⟨rho, hrho, hI⟩37    obtain ⟨phi, hphi, u, _, hrep⟩ :=38      exists_pureState_unitaryTranslate_of_mem_extremePoints_dual_closedBall hrho39    exact ⟨phi, hphi, star u, hrep ▸ hI⟩40  · rintro ⟨phi, hphi, u, hI⟩41    refine ⟨unitaryTranslate u phi, ?_, hI⟩42    exact unitaryTranslate_mem_extremePoints_closedBall u43      (mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hphi)4445/-- A pure-state translate kernel as a point of the existing general GSS. -/46def pureStateTranslateKernel (phi : StrongDual ℂ A)47    (hphi : IsPureNonUnitalState A phi) (u : unitary (Unitization ℂ A)) :48    NormedSpace.GeometricStructureSpace ℂ A :=49  extremeKernel ⟨unitaryTranslate u phi, unitaryTranslate_mem_extremePoints_closedBall u50    (mem_extremePoints_dual_closedBall_of_isPureNonUnitalState phi hphi)⟩5152@[simp]53theorem coe_pureStateTranslateKernel (phi : StrongDual ℂ A)54    (hphi : IsPureNonUnitalState A phi) (u : unitary (Unitization ℂ A)) :55    (pureStateTranslateKernel phi hphi u).val = ((unitaryTranslate u phi).ker : Set A) := rfl5657/-- Every original GSS point has a pure-state translate representative. -/58theorem exists_pureStateTranslateKernel_eq (I : NormedSpace.GeometricStructureSpace ℂ A) :59    ∃ (phi : StrongDual ℂ A) (hphi : IsPureNonUnitalState A phi)60      (u : unitary (Unitization ℂ A)), pureStateTranslateKernel phi hphi u = I := by61  let J : Set A := I.val62  have hI : J ∈ NormedSpace.geometricStructureFamily ℂ A := I.property63  rw [geometricStructureFamily_eq_setOf_exists_pureState_unitaryTranslate] at hI64  obtain ⟨phi, hphi, u, hker⟩ := hI65  exact ⟨phi, hphi, u, Subtype.ext hker⟩6667end MathlibAnnex.Analysis.CStarAlgebra