MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/GCRCharacterization.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-/67import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.NormalPartCompactComparison8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.NormalPartFiniteConjugation910/-!11# Representation-side GCR and CCR criteria from actual components1213No independent factor-representation definition of type I or Glimm--Sakai14bridge is assumed here. The left sides of the criteria are explicitly the15compact containment/equality conditions on actual irreducible images. The16right sides are separately named geometric comparison predicates, NOT17renamings or definitions of type I.1819The small tests use Hilbert carriers in the algebra universe, where the actual20pure GNS witnesses live. Separate theorems transport the conclusion to EVERY21independently specified Hilbert universe through an actual unitary equivalence.22No universe of all Hilbert spaces is formed. A model Hilbert space is explicitly23nontrivial; a merely subsingleton empty spectrum is not a compact target model.24-/2526@[expose] public section27set_option autoImplicit false28noncomputable section29open Set30open scoped CStarAlgebra3132namespace ClosureSpace3334open MathlibAnnex.Analysis.CStarAlgebra35attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra3637/-- The geometric conclusion in the continuous finite comparison criterion.38This predicate says nothing by definition about irreducible representation images. -/39def HasContinuousFiniteCompactComparison.{uH, uX} {X : Type uX}40    (c : ClosureSpace X) : Prop :=41  ∃ (H : Type uH) (instN : NormedAddCommGroup H),42    letI := instN43    ∃ instI : InnerProductSpace ℂ H,44      letI := instI45      ∃ instC : CompleteSpace H,46        letI := instC47        ∃ instT : Nontrivial H,48          letI := instT49          ∃ e : FiniteHomeomorph c50              (NormedSpace.geometricStructureClosure ℂ51                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)),52            c.Continuous (NormedSpace.geometricStructureClosure ℂ53              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) e.toEquiv5455/-- The full-homeomorphism conclusion, kept separate from the one-direction56continuity predicate. -/57def HasCompactOperatorHomeomorph.{uH, uX} {X : Type uX}58    (c : ClosureSpace X) : Prop :=59  ∃ (H : Type uH) (instN : NormedAddCommGroup H),60    letI := instN61    ∃ instI : InnerProductSpace ℂ H,62      letI := instI63      ∃ instC : CompleteSpace H,64        letI := instC65        ∃ instT : Nontrivial H,66          letI := instT67          Nonempty (Homeomorph c68            (NormedSpace.geometricStructureClosure ℂ69              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))7071end ClosureSpace7273namespace MathlibAnnex.Analysis.CStarAlgebra7475universe u v w76attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra77  HomKernelQuotient.imageCStarAlgebra HomKernelQuotient.isClosed_image7879section Concrete80variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]81variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))82variable [IsClosed (S : Set (H →L[ℂ] H))]83variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))8485include hS in86/-- The concrete equivalence. The forward witness is H itself; the converse87accepts any witnessed nonzero model in this universe and uses the actual map. -/88theorem compact_le_iff_normalPart_hasContinuousFiniteCompactComparison :89    ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ≤ S ↔90      ClosureSpace.HasContinuousFiniteCompactComparison.{u, u}91        ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) := by92  constructor93  · intro h94    letI : Nontrivial H :=95      NonUnitalCStarRepresentation.nontrivial_of_isNonzero96        (NonUnitalStarSubalgebraClass.subtype S) hS.197    exact ⟨H, inferInstance, inferInstance, inferInstance, inferInstance,98      normalPartToCompactFiniteHomeomorph S hS,99      continuous_normalPartToCompactFiniteHomeomorph S hS h⟩100  · rintro ⟨K, instN, instI, instC, instT, e, he⟩101    letI := instN102    letI := instI103    letI := instC104    letI := instT105    exact compactOperatorStarSubalgebra_le_of_continuous_finiteHomeomorph S hS e he106107include hS in108/-- The concrete CCR counterpart uses full homeomorphisms on the right. -/109theorem eq_compact_iff_normalPart_hasCompactOperatorHomeomorph :110    S = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ↔111      ClosureSpace.HasCompactOperatorHomeomorph.{u, u}112        ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) := by113  constructor114  · intro h115    letI : Nontrivial H :=116      NonUnitalCStarRepresentation.nontrivial_of_isNonzero117        (NonUnitalStarSubalgebraClass.subtype S) hS.1118    exact ⟨H, inferInstance, inferInstance, inferInstance, inferInstance,119      nonempty_homeomorph_compact_of_eq S h⟩120  · rintro ⟨K, instN, instI, instC, instT, ⟨e⟩⟩121    letI := instN122    letI := instI123    letI := instC124    letI := instT125    exact eq_compactOperatorStarSubalgebra_of_homeomorph S hS e126127end Concrete128129section Algebra130variable {A : Type u} [NonUnitalCStarAlgebra A] [hA : Nontrivial A]131attribute [local instance] _root_.CStarAlgebra.spectralOrder132  _root_.CStarAlgebra.spectralOrderedRing133variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]134135/-- Pure GNS tests imply compact containment for any irreducible representation136in an independently specified Hilbert universe. The bridge is a real unitary137intertwiner, not equality of primitive kernels. -/138theorem compact_le_range_of_forall_pure_state139    (h : ∀ phi : NonUnitalPureState A,140      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS ≤ (NonUnitalStarAlgHom.range phi.gnsRepresentation))141    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :142    ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ≤ (NonUnitalStarAlgHom.range pi) := by143  obtain ⟨phi, hU⟩ := pi.exists_pureState_unitaryEquivalent_gnsRepresentation hpi144  exact hU.symm.compactOperatorStarSubalgebra_le_range (h phi)145146/-- The same actual unitary transports the full compact-image equality. -/147theorem range_eq_compact_of_forall_pure_state148    (h : ∀ phi : NonUnitalPureState A,149      (NonUnitalStarAlgHom.range phi.gnsRepresentation) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS)150    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :151    (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H := by152  obtain ⟨phi, hU⟩ := pi.exists_pureState_unitaryEquivalent_gnsRepresentation hpi153  exact hU.symm.range_eq_compactOperatorStarSubalgebra (h phi)154155include hA in156/-- A compact target may initially inhabit ANY specified universe. Composing157its actual comparison with the GNS normal-part restriction proves the small158pure-GNS condition. No downward ULift or assumed smallness is used. -/159theorem forall_pure_state_compact_le_of_component_compact_comparisons160    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,161      ClosureSpace.HasContinuousFiniteCompactComparison.{w, u}162        ((NormedSpace.geometricStructureClosure ℂ A).subspace163          ((NormedSpace.geometricStructureClosure ℂ A).component I))) :164    ∀ phi : NonUnitalPureState A,165      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS ≤ (NonUnitalStarAlgHom.range phi.gnsRepresentation) := by166  intro phi167  let pi := phi.gnsRepresentation168  let x := phi.gnsVector169  let I := NonUnitalCStarRepresentation.matrixCoefficientKernel pi170    phi.isIrreducible_gnsRepresentation x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero171  let a := imageNormalPartHomeomorph pi phi.isIrreducible_gnsRepresentation172    x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero173  obtain ⟨K, instN, instI, instC, instT, e, he⟩ := h I174  letI := instN175  letI := instI176  letI := instC177  letI := instT178  exact compactOperatorStarSubalgebra_le_of_continuous_finiteHomeomorph (NonUnitalStarAlgHom.range pi)179    ((NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2180      phi.isIrreducible_gnsRepresentation)181    (a.toFiniteHomeomorph.trans e) (he.comp a.continuous_toFun)182183184include hA in185/-- Representation-side GCR, expressed first with actual small pure GNS tests.186Each component model is composed from the existing literal preimage normal-part187homeomorphism and the identity-vector compact comparison. -/188theorem forall_pure_state_compact_le_iff_component_compact_comparison :189    (∀ phi : NonUnitalPureState A,190      ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS ≤ (NonUnitalStarAlgHom.range phi.gnsRepresentation)) ↔191    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,192      ClosureSpace.HasContinuousFiniteCompactComparison.{u, u}193        ((NormedSpace.geometricStructureClosure ℂ A).subspace194          ((NormedSpace.geometricStructureClosure ℂ A).component I)) := by195  constructor196  · intro h I197    obtain ⟨K, instN, instI, instC, pi, hpi, a, _ha⟩ :=198      exists_representation_normalPart_homeomorph_component A I199    letI := instN200    letI := instI201    letI := instC202    letI : Nontrivial K := pi.nontrivial_of_isNonzero hpi.1203    have hi := (NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2 hpi204    let b := normalPartToCompactFiniteHomeomorph (NonUnitalStarAlgHom.range pi) hi205    have hb := continuous_normalPartToCompactFiniteHomeomorph (NonUnitalStarAlgHom.range pi) hi206      (compact_le_range_of_forall_pure_state h pi hpi)207    exact ⟨K, inferInstance, inferInstance, inferInstance, inferInstance,208      a.symm.toFiniteHomeomorph.trans b, hb.comp a.continuous_invFun⟩209  · exact forall_pure_state_compact_le_of_component_compact_comparisons210211include hA in212/-- The component criterion implies compact containment for ALL independently213specified Hilbert universes, not just the small GNS representatives. -/214theorem compact_le_range_of_component_compact_comparisons215    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,216      ClosureSpace.HasContinuousFiniteCompactComparison.{w, u}217        ((NormedSpace.geometricStructureClosure ℂ A).subspace218          ((NormedSpace.geometricStructureClosure ℂ A).component I)))219    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :220    ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ≤ (NonUnitalStarAlgHom.range pi) :=221  compact_le_range_of_forall_pure_state222    (forall_pure_state_compact_le_of_component_compact_comparisons h) pi hpi223224include hA in225/-- Exact all-representation form with the small universe explicitly fixed.226The preceding theorem is the independently quantified extension to any other227Hilbert universe. No independent type-I equivalence is asserted. -/228theorem forall_irreducible_compact_le_iff_component_compact_comparison :229    (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K],230      ∀ pi : NonUnitalCStarRepresentation A K, pi.IsIrreducible →231        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K ≤ (NonUnitalStarAlgHom.range pi)) ↔232    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,233      ClosureSpace.HasContinuousFiniteCompactComparison.{u, u}234        ((NormedSpace.geometricStructureClosure ℂ A).subspace235          ((NormedSpace.geometricStructureClosure ℂ A).component I)) := by236  constructor237  · intro h238    apply forall_pure_state_compact_le_iff_component_compact_comparison.1239    intro phi240    exact h phi.GNS phi.gnsRepresentation phi.isIrreducible_gnsRepresentation241  · intro h K _ _ _ pi hpi242    exact compact_le_range_of_component_compact_comparisons h pi hpi243244include hA in245/-- Arbitrary-universe FULL compact component models yield the actual compact246image equality in the small pure GNS representatives. -/247theorem forall_pure_state_range_eq_compact_of_component_compact_homeomorphs248    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,249      ClosureSpace.HasCompactOperatorHomeomorph.{w, u}250        ((NormedSpace.geometricStructureClosure ℂ A).subspace251          ((NormedSpace.geometricStructureClosure ℂ A).component I))) :252    ∀ phi : NonUnitalPureState A,253      (NonUnitalStarAlgHom.range phi.gnsRepresentation) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS := by254  intro phi255  let pi := phi.gnsRepresentation256  let x := phi.gnsVector257  let I := NonUnitalCStarRepresentation.matrixCoefficientKernel pi258    phi.isIrreducible_gnsRepresentation x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero259  let a := imageNormalPartHomeomorph pi phi.isIrreducible_gnsRepresentation260    x x phi.gnsVector_ne_zero phi.gnsVector_ne_zero261  obtain ⟨K, instN, instI, instC, instT, ⟨e⟩⟩ := h I262  letI := instN263  letI := instI264  letI := instC265  letI := instT266  exact eq_compactOperatorStarSubalgebra_of_homeomorph (NonUnitalStarAlgHom.range pi)267    ((NonUnitalCStarRepresentation.isIrreducible_imageRepresentation_iff pi).2268      phi.isIrreducible_gnsRepresentation)269    (a.trans e)270271272include hA in273/-- The CCR counterpart: actual compact-image equality corresponds to FULL274component homeomorphisms, rather than merely continuous finite homeomorphisms. -/275theorem forall_pure_state_range_eq_compact_iff_component_compact_homeomorph :276    (∀ phi : NonUnitalPureState A,277      (NonUnitalStarAlgHom.range phi.gnsRepresentation) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ phi.GNS) ↔278    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,279      ClosureSpace.HasCompactOperatorHomeomorph.{u, u}280        ((NormedSpace.geometricStructureClosure ℂ A).subspace281          ((NormedSpace.geometricStructureClosure ℂ A).component I)) := by282  constructor283  · intro h I284    obtain ⟨K, instN, instI, instC, pi, hpi, a, _ha⟩ :=285      exists_representation_normalPart_homeomorph_component A I286    letI := instN287    letI := instI288    letI := instC289    letI : Nontrivial K := pi.nontrivial_of_isNonzero hpi.1290    obtain ⟨b⟩ := nonempty_homeomorph_compact_of_eq (NonUnitalStarAlgHom.range pi)291      (range_eq_compact_of_forall_pure_state h pi hpi)292    exact ⟨K, inferInstance, inferInstance, inferInstance, inferInstance, ⟨a.symm.trans b⟩⟩293  · exact forall_pure_state_range_eq_compact_of_component_compact_homeomorphs294295include hA in296/-- Full component comparison implies compact-image equality in every separate297Hilbert universe, through actual unitary transport. -/298theorem range_eq_compact_of_component_compact_homeomorphs299    (h : ∀ I : NormedSpace.GeometricStructureSpace ℂ A,300      ClosureSpace.HasCompactOperatorHomeomorph.{w, u}301        ((NormedSpace.geometricStructureClosure ℂ A).subspace302          ((NormedSpace.geometricStructureClosure ℂ A).component I)))303    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsIrreducible) :304    (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H :=305  range_eq_compact_of_forall_pure_state306    (forall_pure_state_range_eq_compact_of_component_compact_homeomorphs h) pi hpi307308include hA in309/-- Exact all-representation CCR criterion, with small representatives and310arbitrary-Hilbert-universe transport separately proved. -/311theorem forall_irreducible_range_eq_compact_iff_component_compact_homeomorph :312    (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K],313      ∀ pi : NonUnitalCStarRepresentation A K, pi.IsIrreducible →314        (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K) ↔315    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,316      ClosureSpace.HasCompactOperatorHomeomorph.{u, u}317        ((NormedSpace.geometricStructureClosure ℂ A).subspace318          ((NormedSpace.geometricStructureClosure ℂ A).component I)) := by319  constructor320  · intro h321    apply forall_pure_state_range_eq_compact_iff_component_compact_homeomorph.1322    intro phi323    exact h phi.GNS phi.gnsRepresentation phi.isIrreducible_gnsRepresentation324  · intro h K _ _ _ pi hpi325    exact range_eq_compact_of_component_compact_homeomorphs h pi hpi326327end Algebra328end MathlibAnnex.Analysis.CStarAlgebra