MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/CompactRepresentationRigidity.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.CompactDirectSumRigidity8import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.CompactRepresentationTransport9import MathlibAnnex.Analysis.CStarAlgebra.DirectSum.CompactlyRepresentedDecomposition10import MathlibAnnex.Analysis.CStarAlgebra.Spectrum.CompactRepresentationCharacterization11import MathlibAnnex.Analysis.CStarAlgebra.GeometricStructure.StarAlgEquiv1213/-!14# One-sided compact representation rigidity of geometric structure spaces1516If one nonunital complex C-star algebra has an actual faithful compact-valued17representation, a full geometric-structure closure homeomorphism to a second18algebra forces a star-algebra equivalence. Compact representability of the19second algebra is derived by transport to its already defined reduced atomic20representation, not required as an additional premise.2122The two actual representations supply the canonical compact c₀ decompositions.23Their dependent fibers are the very cyclic subspaces used in those models.24Each fiber is nontrivial by its existing chosen nonzero cyclic vector. The25all-index given-model rigidity theorem handles empty and nonempty index types,26so no nontriviality, nonempty-index, unit, or separability premise is added.27Both spectral orders are fixed locally before any model fiber is used.2829The final equivalence concerns existence: a star equivalence exists if and30only if a full GSS homeomorphism exists, provided either algebra admits a31faithful compact representation. The given-representation theorem permits32its Hilbert space to lie in an independent universe. The existential version33uses each algebra's own universe, exactly as in the compact-representation34characterization; its canonical reduced atomic witness is not obtained by35shrinking an arbitrary Hilbert space.3637The star equivalence need not induce the specified nonlinear GSS38homeomorphism. Only existence of a star equivalence is concluded. Conversely,39a star equivalence supplies its own induced full GSS homeomorphism. No claim40about equality of these two geometric maps is made.41-/4243@[expose] public section44set_option autoImplicit false45set_option maxHeartbeats 200000046set_option synthInstance.maxHeartbeats 20000047noncomputable section4849open scoped CStarAlgebra5051namespace MathlibAnnex.Analysis.CStarAlgebra5253universe u v w5455variable {A : Type u} {B : Type v}56variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]57variable {H : Type w} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]5859/-- A faithful compact-valued representation on one side and a full GSS60homeomorphism force a star equivalence. The target representation, both61compact models, and all fiber nontriviality proofs are produced internally.62The zero-algebra and empty-index cases use the existing all-index theorem. -/63theorem nonempty_starAlgEquiv_of_isCompactlyRepresented_of_geometricStructure_homeomorph64    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented)65    (e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)66      (NormedSpace.geometricStructureClosure ℂ B)) :67    Nonempty (A ≃⋆ₐ[ℂ] B) := by68  letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A69  letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A70  letI : PartialOrder B := _root_.CStarAlgebra.spectralOrder B71  letI : StarOrderedRing B := _root_.CStarAlgebra.spectralOrderedRing B72  let rho : NonUnitalCStarRepresentation B (PrimitiveSpectrum.ReducedAtomicHilbertSpace B) :=73    PrimitiveSpectrum.reducedAtomicRepresentation (A := B)74  have hrho : rho.IsCompactlyRepresented :=75    PrimitiveSpectrum.isCompactlyRepresented_reducedAtomicRepresentation_of_geometricStructure_homeomorph76      e pi hpi77  let EA : A ≃⋆ₐ[ℂ] CompactOperatorC0Sum78      (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi) :=79    pi.compactC0Decomposition hpi80  let EB : B ≃⋆ₐ[ℂ] CompactOperatorC0Sum81      (fun j : MinimalClosedStarIdeal B => j.CompactModelSpace rho hrho) :=82    rho.compactC0Decomposition hrho83  letI : ∀ i : MinimalClosedStarIdeal A, Nontrivial (i.CompactModelSpace pi hpi) :=84    fun i => MinimalClosedStarIdeal.instNontrivialCompactModelSpace i pi hpi85  letI : ∀ j : MinimalClosedStarIdeal B, Nontrivial (j.CompactModelSpace rho hrho) :=86    fun j => MinimalClosedStarIdeal.instNontrivialCompactModelSpace j rho hrho87  exact nonempty_starAlgEquiv_of_compact_direct_sum_models_of_geometricStructure_homeomorph88    (fun i : MinimalClosedStarIdeal A => i.CompactModelSpace pi hpi)89    (fun j : MinimalClosedStarIdeal B => j.CompactModelSpace rho hrho)90    EA EB e9192/-- With an actual faithful compact representation of `A`, existence of a93star equivalence to `B` is equivalent to existence of a full GSS homeomorphism.94The reverse implication derives compact representability of `B`; it does not95assume that an arbitrary prescribed representation of `B` is compact. -/96theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_isCompactlyRepresented97    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :98    Nonempty (A ≃⋆ₐ[ℂ] B) ↔99      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)100        (NormedSpace.geometricStructureClosure ℂ B)) := by101  constructor102  · rintro ⟨E⟩103    exact ⟨geometricStructureHomeomorphOfStarAlgEquiv E⟩104  · rintro ⟨e⟩105    exact nonempty_starAlgEquiv_of_isCompactlyRepresented_of_geometricStructure_homeomorph106      pi hpi e107108/-- The one-sided compact GSS characterization. Either algebra may supply109existence of a faithful compact representation in its own universe, with the110Hilbert carrier and its structures explicitly quantified. The characterization111provides its same canonical reduced atomic witness; the right-hand branch112uses the inverse geometric homeomorphism and reverses the resulting star113equivalence. Neither algebra is assumed to be nonzero. -/114theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_exists_isCompactlyRepresented115    (hCompact :116      (∃ (K : Type u) (normed : NormedAddCommGroup K),117        letI : NormedAddCommGroup K := normed118        ∃ inner : InnerProductSpace ℂ K,119          letI : InnerProductSpace ℂ K := inner120          ∃ complete : CompleteSpace K,121            letI : CompleteSpace K := complete122            ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented) ∨123      (∃ (K : Type v) (normed : NormedAddCommGroup K),124        letI : NormedAddCommGroup K := normed125        ∃ inner : InnerProductSpace ℂ K,126          letI : InnerProductSpace ℂ K := inner127          ∃ complete : CompleteSpace K,128            letI : CompleteSpace K := complete129            ∃ pi : NonUnitalCStarRepresentation B K, pi.IsCompactlyRepresented)) :130    Nonempty (A ≃⋆ₐ[ℂ] B) ↔131      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)132        (NormedSpace.geometricStructureClosure ℂ B)) := by133  constructor134  · rintro ⟨E⟩135    exact ⟨geometricStructureHomeomorphOfStarAlgEquiv E⟩136  · rintro ⟨e⟩137    rcases hCompact with hA | hB138    · letI : PartialOrder A := _root_.CStarAlgebra.spectralOrder A139      letI : StarOrderedRing A := _root_.CStarAlgebra.spectralOrderedRing A140      have hAtomic :=141        (NonUnitalCStarRepresentation.exists_isCompactlyRepresented_iff_reducedAtomicRepresentation142          (A := A)).mp hA143      exact nonempty_starAlgEquiv_of_isCompactlyRepresented_of_geometricStructure_homeomorph144        (PrimitiveSpectrum.reducedAtomicRepresentation (A := A)) hAtomic e145    · letI : PartialOrder B := _root_.CStarAlgebra.spectralOrder B146      letI : StarOrderedRing B := _root_.CStarAlgebra.spectralOrderedRing B147      have hAtomic :=148        (NonUnitalCStarRepresentation.exists_isCompactlyRepresented_iff_reducedAtomicRepresentation149          (A := B)).mp hB150      obtain ⟨E⟩ :=151        nonempty_starAlgEquiv_of_isCompactlyRepresented_of_geometricStructure_homeomorph152          (PrimitiveSpectrum.reducedAtomicRepresentation (A := B)) hAtomic e.symm153      exact ⟨E.symm⟩154155end MathlibAnnex.Analysis.CStarAlgebra