MathlibAnnex/Analysis/CStarAlgebra/Spectrum/CompactRepresentationCharacterization.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.Spectrum.CompactlyRepresented8import MathlibAnnex.Analysis.CStarAlgebra.Representation.PrimitiveCompactRange9import MathlibAnnex.Analysis.CStarAlgebra.Representation.DiscreteCCRCompact1011/-!12# Characterization of algebras admitting faithful compact representations1314A nonunital complex C-star algebra admits a faithful compact-valued15representation if and only if its primitive spectrum is discrete and every16nonzero irreducible representation has literal range equal to the compact17operators. The intrinsic representative used here is the already defined18`PrimitiveSpectrum.reducedAtomicRepresentation`, not a second chosen map.1920The quantified test in the equivalences uses Hilbert spaces in `Type u`,21where the algebra lies in `Type u`. This universe contains the selected GNS22spaces and their dependent Hilbert sum. The common primitive-range bridge23lifts the conclusion to any independently specified Hilbert universe.24Conversely, the first theorem starts from an actual compact representation25in an independent `Type v` and proves compactness of this same reduced atomic26map. No universe-shrinking equivalence or `ULift` identification is assumed.2728The existential formulas expose each Hilbert-space structure before using29it as a local instance. Their reverse witness is the existing reduced atomic30Hilbert sum with its existing structures and representation. No new CCR31predicate, representation definition, or choice operation is introduced.3233The algebraic condition does not say that an arbitrary given faithful34representation is compact-valued: infinite multiplicities need not preserve35compactness. The left sides below concern existence or the fixed reduced36atomic representation. The moreover theorem concerns that same map, whose37range is block-diagonal, not all compact operators on the Hilbert sum.3839The canonical spectral order is installed only locally. Zero algebras and40empty primitive spectra remain included; no unit, nontriviality, separability,41countability, finite-dimensionality, density, or fiber-model hypothesis is42added to the final characterization.43-/4445@[expose] public section4647set_option autoImplicit false48set_option maxHeartbeats 200000049set_option synthInstance.maxHeartbeats 20000050noncomputable section5152open Set53open scoped Classical CStarAlgebra ENNReal lp5455attribute [local instance] _root_.CStarAlgebra.spectralOrder56  _root_.CStarAlgebra.spectralOrderedRing5758namespace MathlibAnnex.Analysis.CStarAlgebra5960open MathlibAnnex.Analysis.InnerProductSpace6162universe u v6364variable {A : Type u} [NonUnitalCStarAlgebra A]65variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]6667namespace PrimitiveSpectrum6869/-- Any actual faithful compact representation, in an independent Hilbert70universe, makes the existing canonical reduced atomic representation71faithfully compact. The latter map is not replaced by the given map. -/72theorem isCompactlyRepresented_reducedAtomicRepresentation_of_isCompactlyRepresented73    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :74    (reducedAtomicRepresentation (A := A)).IsCompactlyRepresented := by75  letI : DiscreteTopology (PrimitiveSpectrum A) :=76    discreteTopology_primitiveSpectrum_of_isCompactlyRepresented pi hpi77  exact isCompactlyRepresented_reducedAtomicRepresentation78    (range_pureStateRepresentative_eq_compact_of_isCompactlyRepresented pi hpi)7980/-- Intrinsic compact-representation characterization. The all-irreducible81test is in the algebra's universe; the common selected-representative bridge82provides the pointwise conclusion in every independent Hilbert universe. -/83theorem isCompactlyRepresented_reducedAtomicRepresentation_iff :84    (reducedAtomicRepresentation (A := A)).IsCompactlyRepresented ↔85      (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]86        [CompleteSpace K] (rho : NonUnitalCStarRepresentation A K),87        rho.IsIrreducible →88          (NonUnitalStarAlgHom.range rho) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K) ∧89      DiscreteTopology (PrimitiveSpectrum A) := by90  constructor91  · intro hAtomic92    refine ⟨?_, discreteTopology_primitiveSpectrum_of_isCompactlyRepresented93      (reducedAtomicRepresentation (A := A)) hAtomic⟩94    exact95      (forall_pureStateRepresentative_range_eq_compact_iff_forall_irreducible_range_eq_compact96        (A := A)).mp97        (range_pureStateRepresentative_eq_compact_of_isCompactlyRepresented98          (reducedAtomicRepresentation (A := A)) hAtomic)99  · rintro ⟨hCCR, hDiscrete⟩100    letI : DiscreteTopology (PrimitiveSpectrum A) := hDiscrete101    exact isCompactlyRepresented_reducedAtomicRepresentation102      ((forall_pureStateRepresentative_range_eq_compact_iff_forall_irreducible_range_eq_compact103        (A := A)).mpr hCCR)104105end PrimitiveSpectrum106107namespace NonUnitalCStarRepresentation108109/-- Existence of a faithful compact representation in the algebra's universe110is equivalent to compactness of its fixed reduced atomic representation.111The reverse direction supplies its actual Hilbert space, structures, and112map, rather than choosing an unspecified representation. -/113theorem exists_isCompactlyRepresented_iff_reducedAtomicRepresentation :114    (∃ (K : Type u) (normed : NormedAddCommGroup K),115      letI : NormedAddCommGroup K := normed116      ∃ inner : InnerProductSpace ℂ K,117        letI : InnerProductSpace ℂ K := inner118        ∃ complete : CompleteSpace K,119          letI : CompleteSpace K := complete120          ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented) ↔121    (PrimitiveSpectrum.reducedAtomicRepresentation (A := A)).IsCompactlyRepresented := by122  constructor123  · rintro ⟨K, normed, h⟩124    letI : NormedAddCommGroup K := normed125    rcases h with ⟨inner, h⟩126    letI : InnerProductSpace ℂ K := inner127    rcases h with ⟨complete, h⟩128    letI : CompleteSpace K := complete129    rcases h with ⟨pi, hpi⟩130    exact PrimitiveSpectrum.isCompactlyRepresented_reducedAtomicRepresentation_of_isCompactlyRepresented131      pi hpi132  · intro hAtomic133    refine ⟨PrimitiveSpectrum.ReducedAtomicHilbertSpace A, inferInstance, ?_⟩134    refine ⟨inferInstance, ?_⟩135    exact ⟨inferInstance, PrimitiveSpectrum.reducedAtomicRepresentation (A := A), hAtomic⟩136137/-- A nonunital complex C-star algebra admits a faithful compact-valued138representation exactly when all its algebra-universe irreducible actions139have full compact range and its existing primitive spectrum is discrete.140An actual representation in another universe yields the same left side via141the canonical reduced atomic representation, not by shrinking its space. -/142theorem exists_isCompactlyRepresented_iff :143    (∃ (K : Type u) (normed : NormedAddCommGroup K),144      letI : NormedAddCommGroup K := normed145      ∃ inner : InnerProductSpace ℂ K,146        letI : InnerProductSpace ℂ K := inner147        ∃ complete : CompleteSpace K,148          letI : CompleteSpace K := complete149          ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented) ↔150    (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K]151      [CompleteSpace K] (rho : NonUnitalCStarRepresentation A K),152      rho.IsIrreducible →153        (NonUnitalStarAlgHom.range rho) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K) ∧154    DiscreteTopology (PrimitiveSpectrum A) :=155  (exists_isCompactlyRepresented_iff_reducedAtomicRepresentation (A := A)).trans156    (PrimitiveSpectrum.isCompactlyRepresented_reducedAtomicRepresentation_iff (A := A))157158end NonUnitalCStarRepresentation159160namespace PrimitiveSpectrum161162/-- Moreover, any given faithful compact representation yields these facts163about the same pre-existing reduced atomic map: faithful compactness, both164literal diagonal range descriptions, isometry, norm preservation, coordinate165compression, and the adjoint identity. In particular its range is not166asserted to contain off-diagonal compact operators. -/167theorem reducedAtomicRepresentation_spec_of_isCompactlyRepresented168    (pi : NonUnitalCStarRepresentation A H) (hpi : pi.IsCompactlyRepresented) :169    (reducedAtomicRepresentation (A := A)).IsCompactlyRepresented ∧170    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =171      (NonUnitalStarAlgHom.range (CompactOperatorC0Sum.diagonalRepresentation172        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ∧173    (NonUnitalStarAlgHom.range (reducedAtomicRepresentation (A := A))) =174      (NonUnitalStarAlgHom.range (CompactOperatorBoundedProduct.diagonalRepresentation175        (fun P : PrimitiveSpectrum A => P.pureStateRepresentative.GNS))) ⊓176        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ177          (ReducedAtomicHilbertSpace A) ∧178    Isometry (reducedAtomicRepresentation (A := A)) ∧179    (∀ a : A, ‖reducedAtomicRepresentation (A := A) a‖ = ‖a‖) ∧180    (∀ (a : A) (P : PrimitiveSpectrum A),181      (coordinateProjection P).comp182        ((reducedAtomicRepresentation (A := A) a).comp (coordinateEmbedding P)) =183          P.pureStateRepresentative.gnsRepresentation a) ∧184    (∀ a : A, ContinuousLinearMap.adjoint (reducedAtomicRepresentation (A := A) a) =185      reducedAtomicRepresentation (star a)) := by186  letI : DiscreteTopology (PrimitiveSpectrum A) :=187    discreteTopology_primitiveSpectrum_of_isCompactlyRepresented pi hpi188  have hSelected := range_pureStateRepresentative_eq_compact_of_isCompactlyRepresented pi hpi189  exact ⟨isCompactlyRepresented_reducedAtomicRepresentation hSelected,190    reducedAtomicRepresentation_range_eq_c0_diagonalRepresentation_range hSelected,191    reducedAtomicRepresentation_range_eq_bounded_diagonalRepresentation_range_inf_compactOperatorStarSubalgebra192      hSelected,193    isometry_reducedAtomicRepresentation (A := A),194    norm_reducedAtomicRepresentation (A := A),195    coordinateProjection_comp_reducedAtomicRepresentation_comp_coordinateEmbedding (A := A),196    adjoint_reducedAtomicRepresentation (A := A)⟩197198end PrimitiveSpectrum199200end MathlibAnnex.Analysis.CStarAlgebra201202end