MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/ElementaryCharacterization.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.NormalPartFiniteCharacter8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.ElementaryOfFiniteConjugation910/-!11# Compact-operator models characterized by singleton and finite conjugation1213This is a small joint endpoint, not a new definition of `IsElementary`.14The model is the existing `IsCompactOperatorModel`; the iff uses a pure GNS15model in the source-algebra universe. Any given compact model on a separately16specified Hilbert universe also gives such a GNS model by the theorem below.1718The source-class carrier is `max u w` for the converse. That converse needs19access to the actual small GNS and its full bounded-operator algebra. No large20witness is shrunk, and no collection of all universes is made into a type.2122Theorem 7.7 in the supplied paper assumes nonseparability. Here the finite23character argument supplies its previously separate finite-target branch, so24the characterization is stated for every nontrivial complex C-star algebra.25The printed theorem is a specialization, not a change to the historical text.26- Only forward full continuity of the tested finite maps is assumed.27- A zero Hilbert space is not counted as a singleton spectrum.28- No isometry assertion about the selected bounded conjugation maps is made.29-/3031@[expose] public section32set_option autoImplicit false33noncomputable section34open Set3536namespace MathlibAnnex.Analysis.CStarAlgebra3738universe u v w uA uL39variable {A : Type u} [NonUnitalCStarAlgebra A]40variable [PartialOrder A] [StarOrderedRing A]41variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]4243attribute [local instance] HomKernelQuotient.imageCStarAlgebra HomKernelQuotient.isClosed_image4445/-- The forward property on the FULL geometric structure space of a given46nonzero compact model, in all Hilbert dimensions. The same pi and preimage47homeomorphism are used; the source-class universes are independent. -/48theorem hasContinuousFiniteConjugation_of_isCompactOperatorModel_all_dimensions49    [Nontrivial H] (pi : NonUnitalCStarRepresentation A H)50    (hpi : IsCompactOperatorModel pi) :51    (NormedSpace.geometricStructureClosure ℂ A).HasContinuousFiniteConjugation52      (ClosureCat.IsCStarRealizable.{uA, uL}) := by53  have hi := isIrreducible_of_isCompactOperatorModel pi hpi54  letI : Nontrivial A := NonUnitalCStarRepresentation.nontrivial_algebra_of_isNonzero pi hi.155  have hs := exists_forall_eq_irreducibleSpectrum_of_isCompactOperatorModel pi hpi56  have hrange := range_eq_compactOperatorStarSubalgebra_of_isCompactOperatorModel pi hpi57  have hn : ((NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range pi)).subspace (normalPart (NonUnitalStarAlgHom.range pi))).HasContinuousFiniteConjugation58      (ClosureCat.IsCStarRealizable.{uA, uL}) := by59    dsimp +instances only [HomKernelQuotient.imageCStarAlgebra,60      NonUnitalStarSubalgebra.nonUnitalCStarAlgebra]61    rw [hrange]62    exact hasContinuousFiniteConjugation_compact_operators_all_dimensions63  exact (singletonImageNormalPartHomeomorph hs pi hi).hasContinuousFiniteConjugation hn6465/-- The existence-including component condition follows from the SAME given66model, including Hilbert dimensions one and two. -/67theorem exists_component_hasContinuousFiniteConjugation_of_isCompactOperatorModel_all_dimensions68    [Nontrivial H] (pi : NonUnitalCStarRepresentation A H)69    (hpi : IsCompactOperatorModel pi) :70    ∃ I : NormedSpace.GeometricStructureSpace ℂ A,71      ((NormedSpace.geometricStructureClosure ℂ A).subspace72        ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation73          (ClosureCat.IsCStarRealizable.{uA, uL}) := by74  have hi := isIrreducible_of_isCompactOperatorModel pi hpi75  letI : Nontrivial A := NonUnitalCStarRepresentation.nontrivial_algebra_of_isNonzero pi hi.176  have hs := exists_forall_eq_irreducibleSpectrum_of_isCompactOperatorModel pi hpi77  obtain ⟨I, _⟩ := exists_forall_eq_irreducibleSpectrum_iff_exists_component_eq_univ.mp hs78  exact ⟨I, (singletonComponentHomeomorph hs I).symm.hasContinuousFiniteConjugation79    (hasContinuousFiniteConjugation_of_isCompactOperatorModel_all_dimensions pi hpi)⟩8081/-- Minimal joint iff for Theorem 7.7, generalized to nontrivial A. Both the82singleton and the target-component quantifiers include existence. The strong83R23 endpoint still records the same faithful pi, star isomorphism and literal84preimage homeomorphism, rather than having those witnesses reselected here. -/85theorem exists_pureState_compactOperatorModel_iff_singleton_finiteConjugation86    [Nontrivial A] :87    (∃ phi : NonUnitalPureState A, IsCompactOperatorModel phi.gnsRepresentation) ↔88      (∃ q : IrreducibleSpectrum A, ∀ r : IrreducibleSpectrum A, r = q) ∧89      ∃ I : NormedSpace.GeometricStructureSpace ℂ A,90        ((NormedSpace.geometricStructureClosure ℂ A).subspace91          ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation92            (ClosureCat.IsCStarRealizable.{u, max u w}) := by93  constructor94  · rintro ⟨phi, hmodel⟩95    letI : Nontrivial phi.GNS := NonUnitalCStarRepresentation.nontrivial_of_isNonzero96      phi.gnsRepresentation phi.isIrreducible_gnsRepresentation.197    exact ⟨exists_forall_eq_irreducibleSpectrum_of_isCompactOperatorModel98        phi.gnsRepresentation hmodel,99      exists_component_hasContinuousFiniteConjugation_of_isCompactOperatorModel_all_dimensions100        phi.gnsRepresentation hmodel⟩101  · rintro ⟨hsingle, hproperty⟩102    obtain ⟨phi, _hfaith, _hnormal, _r, _hr, hmodel, _hrest⟩ :=103      exists_faithful_compactOperatorModel_of_singleton_finiteConjugation hsingle hproperty104    exact ⟨phi, hmodel⟩105106/-- A model on ANY separately specified Hilbert universe gives a pure-GNS107compact model in the algebra's own universe. This is proved through the actual108forward property and the existing converse, not by an unproved Small instance. -/109theorem exists_pureState_compactOperatorModel_of_isCompactOperatorModel110    [Nontrivial H] (pi : NonUnitalCStarRepresentation A H)111    (hpi : IsCompactOperatorModel pi) :112    ∃ phi : NonUnitalPureState A, IsCompactOperatorModel phi.gnsRepresentation := by113  have hi := isIrreducible_of_isCompactOperatorModel pi hpi114  letI : Nontrivial A := NonUnitalCStarRepresentation.nontrivial_algebra_of_isNonzero pi hi.1115  have hp : ∃ I : NormedSpace.GeometricStructureSpace ℂ A,116      ((NormedSpace.geometricStructureClosure ℂ A).subspace117        ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation118          (ClosureCat.IsCStarRealizable.{u, u}) :=119    exists_component_hasContinuousFiniteConjugation_of_isCompactOperatorModel_all_dimensions pi hpi120  exact (exists_pureState_compactOperatorModel_iff_singleton_finiteConjugation.{u, 0}).mpr121    ⟨exists_forall_eq_irreducibleSpectrum_of_isCompactOperatorModel pi hpi, hp⟩122123/-- Remark 7.8: the component condition (ii) itself is invariant under a full124GSS homeomorphism. Neither singleton spectrum nor compactness is an input.125The SAME universally quantified source class is kept in both directions. -/126theorem exists_component_finiteConjugation_iff_of_geometricStructure_homeomorph127    {B : Type v} [NonUnitalCStarAlgebra B]128    (e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)129      (NormedSpace.geometricStructureClosure ℂ B)) :130    (∃ I : NormedSpace.GeometricStructureSpace ℂ A,131      ((NormedSpace.geometricStructureClosure ℂ A).subspace132        ((NormedSpace.geometricStructureClosure ℂ A).component I)).HasContinuousFiniteConjugation133          (ClosureCat.IsCStarRealizable.{uA, uL})) ↔134    (∃ J : NormedSpace.GeometricStructureSpace ℂ B,135      ((NormedSpace.geometricStructureClosure ℂ B).subspace136        ((NormedSpace.geometricStructureClosure ℂ B).component J)).HasContinuousFiniteConjugation137          (ClosureCat.IsCStarRealizable.{uA, uL})) :=138  e.exists_hasContinuousFiniteConjugation_component_iff139140end MathlibAnnex.Analysis.CStarAlgebra