MathlibAnnex/Analysis/CStarAlgebra/GeometricStructure/SubhomogeneousCharacterization.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.HomogeneousCharacterization89/-!10# Uniform finite bounds on irreducible representation dimensions1112These are raw representation-side subhomogeneous criteria, not a new definition13of type I or a substitute for the independent Glimm--Sakai bridge. The common14finite-dimensional comparison proof is reused with the predicate `m ≤ n`.15Every representation condition includes finiteness, and n = 0 is treated by a16nonzero pure GNS witness. The zero C-star algebra is outside this module's scope.17-/1819@[expose] public section20set_option autoImplicit false21noncomputable section2223namespace MathlibAnnex.Analysis.CStarAlgebra2425universe u w26variable {A : Type u} [NonUnitalCStarAlgebra A] [hA : Nontrivial A]27attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra28  _root_.CStarAlgebra.spectralOrder _root_.CStarAlgebra.spectralOrderedRing2930include hA in31/-- A uniform finite bound on all irreducible dimensions is equivalent to32finite compact component models satisfying that bound. Neither direction of33full continuity is a premise on the finite comparisons. -/34theorem forall_irreducible_finrank_le_iff_component_compact_comparison (n : ℕ) :35    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],36      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →37        FiniteDimensional ℂ L ∧ Module.finrank ℂ L ≤ n) ↔38    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,39      ClosureSpace.HasFiniteDimensionalCompactComparison.{u, u}40        ((NormedSpace.geometricStructureClosure ℂ A).subspace41          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ n) :=42  forall_irreducible_finiteDimensional_finrank_iff_component_compact_comparison (fun m => m ≤ n)4344include hA in45/-- Full homeomorphisms give the same bounded-dimension condition. The full46continuity was proved from finite character in the common theorem. -/47theorem forall_irreducible_finrank_le_iff_component_compact_homeomorph (n : ℕ) :48    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],49      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →50        FiniteDimensional ℂ L ∧ Module.finrank ℂ L ≤ n) ↔51    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,52      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{u, u}53        ((NormedSpace.geometricStructureClosure ℂ A).subspace54          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ n) :=55  forall_irreducible_finiteDimensional_finrank_iff_component_compact_homeomorph (fun m => m ≤ n)5657include hA in58/-- There is no zero bound on the finite dimensions of all nonzero irreducible59representations of a nontrivial C-star algebra. -/60theorem not_forall_irreducible_finrank_le_zero :61    ¬ (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],62      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →63        FiniteDimensional ℂ L ∧ Module.finrank ℂ L ≤ 0) := by64  intro h65  obtain ⟨m, hm, hm0⟩ := exists_pos_finrank_of_forall_pure_state (fun m => m ≤ 0)66    (fun phi => h phi.GNS phi.gnsRepresentation phi.isIrreducible_gnsRepresentation)67  exact (lt_irrefl (0 : ℕ)) (lt_of_lt_of_le hm hm0)6869include hA in70/-- The bounded component condition is also impossible at n = 0, even if71compact target carriers may inhabit a separate universe. -/72theorem not_forall_component_compact_comparison_finrank_le_zero :73    ¬ (∀ I : NormedSpace.GeometricStructureSpace ℂ A,74      ClosureSpace.HasFiniteDimensionalCompactComparison.{w, u}75        ((NormedSpace.geometricStructureClosure ℂ A).subspace76          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ 0)) := by77  intro h78  obtain ⟨m, hm, hm0⟩ := exists_pos_finrank_of_forall_pure_state (fun m => m ≤ 0)79    (forall_pure_state_finiteDimensional_finrank_of_component_compact_comparisons80      (fun m => m ≤ 0) h)81  exact (lt_irrefl (0 : ℕ)) (lt_of_lt_of_le hm hm0)8283include hA in84/-- The full compact-model condition cannot have zero dimension or a zero85upper bound. This is a consequence of the real nonzero witnesses, not vacuity. -/86theorem not_forall_component_compact_homeomorph_finrank_le_zero :87    ¬ (∀ I : NormedSpace.GeometricStructureSpace ℂ A,88      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{w, u}89        ((NormedSpace.geometricStructureClosure ℂ A).subspace90          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ 0)) := by91  intro h92  exact not_forall_component_compact_comparison_finrank_le_zero93    (fun I => (h I).hasFiniteDimensionalCompactComparison)9495end MathlibAnnex.Analysis.CStarAlgebra