Irreducible dimension at most a fixed number

MathlibAnnex.Analysis.CStarAlgebra.forall_irreducible_finrank_le_iff_component_compact_homeomorph

theorem

Characterizes a uniform finite dimension bound by full compact component models.

Statement

Let be a nonzero complex C*-algebra, and let .

For a complex C*-algebra , write for its geometric structure space. Its points are the unions of kernels of norm-one bounded complex-linear functionals supporting a maximal proper face of the closed unit ball of ; faces use real convexity. Write for the hull–kernel closure on :

These are the geometric structure definition and its closure, with the norm-one description justified by the norm-one support characterization.

For , let be its finite-chain component: the points reachable from by a finite chain in which adjacent points are equal or form a nonclosed two-point set. Give the induced closure

For a complex Hilbert space , let be the algebra of compact operators on . In particular, denotes closure on , where is itself the algebra to which the geometric structure construction is applied.

The following conditions are equivalent:

• Every irreducible -representation on a complex Hilbert space has finite-dimensional and .
• For every , there are a nonzero finite-dimensional complex Hilbert space with and a bijection such that

Here is the closure on the geometric structure space of the compact-operator algebra on this same . Thus is a homeomorphism of closure spaces. The model and the map may depend on ; the bound is common to all components.

Assumptions

The algebra is nonzero; no assumption is made. Representations are -homomorphisms into bounded operators, without a requirement of unitality. Irreducibility includes a nonzero action, but does not require faithfulness. All Hilbert spaces are complex and complete. The compatible order on supplies positivity and pure states. Finite-dimensionality is a conclusion on the representation side and a requirement on the model side. It is separate from the numerical dimension bound. No separability hypothesis is added.

Conclusion

A uniform finite bound on the dimensions of all irreducible representations is equivalent to the compact-operator component models in (1), with the same bound. For nonzero , both sides are false at , by the cited zero-bound exclusions. This does not add as an input assumption.

theorem forall_irreducible_finrank_le_iff_component_compact_homeomorph (n : ℕ) :
    (∀ (L : Type u) [NormedAddCommGroup L] [InnerProductSpace ℂ L] [CompleteSpace L],
      ∀ pi : NonUnitalCStarRepresentation A L, pi.IsIrreducible →
        FiniteDimensional ℂ L ∧ Module.finrank ℂ L ≤ n) ↔
    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,
      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{u, u}
        ((NormedSpace.geometricStructureClosure ℂ A).subspace
          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ n)

universe u w
variable {A : Type u} [NonUnitalCStarAlgebra A] [hA : Nontrivial A]
attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra
  _root_.CStarAlgebra.spectralOrder _root_.CStarAlgebra.spectralOrderedRing

include hA in

def HasFiniteDimensionalCompactHomeomorph.{uH, uX} {X : Type uX}
    (c : ClosureSpace X) (P : ℕ → Prop) : Prop :=
  ∃ (H : Type uH) (instN : NormedAddCommGroup H),
    letI := instN
    ∃ instI : InnerProductSpace ℂ H,
      letI := instI
      ∃ instC : CompleteSpace H,
        letI := instC
        ∃ instT : Nontrivial H,
          letI := instT
          FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) ∧
            Nonempty (Homeomorph c
              (NormedSpace.geometricStructureClosure ℂ
                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))

    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,
      ClosureSpace.HasFiniteDimensionalCompactHomeomorph.{u, u}
        ((NormedSpace.geometricStructureClosure ℂ A).subspace
          ((NormedSpace.geometricStructureClosure ℂ A).component I)) (fun m => m ≤ n) :=

structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where
  continuous_toFun : c.Continuous d toFun
  continuous_invFun : d.Continuous c invFun

Read exact source with highlighted declaration · Raw UTF-8 source · LFH Companion ·

Technical documentation