Compact equality in every irreducible image

MathlibAnnex.Analysis.CStarAlgebra.forall_irreducible_range_eq_compact_iff_component_compact_homeomorph

theorem

Characterizes equality with the compact operators by full component homeomorphisms.

Statement

Let be a nonzero complex C*-algebra.

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 :

c_B(\mathcal U)=\left\{J\in S(B):\bigcap_{L\in\mathcal U}L\subseteq J\right\}, \qquad \mathcal U\subseteq S(B).

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

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. This uses the linked-pair relation and its generated components, rather than topological connectedness. Give the induced closure

c_{C_A(I)}(E)=C_A(I)\cap c_A(E),\qquad E\subseteq C_A(I).

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:

For every irreducible -representation on a complex Hilbert space ,

\pi(A)=\mathcal K(H).\tag{1}

For every , there are a nonzero complex Hilbert space and a bijection satisfying

e(c_{C_A(I)}(E))=c_{\mathcal K(K)}(e(E)) \quad(E\subseteq C_A(I)).\tag{2}

Thus is a homeomorphism of closure spaces: the same and its inverse are continuous for arbitrary subsets. Both and may depend on . The equality in (2) applies to all subsets, not only finite ones; denotes the image of a set.

Assumptions

The algebra is nonzero. Representations are -homomorphisms into bounded operators; a unit is not required, and the source does not impose preservation of a unit. The Hilbert spaces are complete over . Irreducibility includes a nonzero action, but does not require faithfulness. Neither separability nor finite-dimensionality is assumed. The component closure is induced from .

Conclusion

The CCR image condition is equivalent to homeomorphisms of the components onto compact-operator geometric structure spaces. The image equality is inside . In contrast, the forward-continuity criterion characterizes only .

Main citations

The compact-image equality characterization states the equivalence. The full compact-homeomorphism condition requires full continuity in both directions. The pure-state equality theorem and equality transport to an independently specified Hilbert space apply to the same representation images. The forward-only characterization instead detects inclusion, not equality.

The finite-homeomorphism fields, closure continuity, and homeomorphism fields specify the map conditions used here. The closure-transport identity expresses a homeomorphism by equality of closures of arbitrary sets.

Lean source signature (exact)

The preceding variable declaration introduces and its nontriviality. The local spectral order is used for positivity and pure states. The include hA in retains nonzero among this theorem's parameters, although the main excerpt does not repeat these ambient binders. Both separate excerpts are shown in the source context below.

GCRCharacterization.lean. The contiguous declaration prefix ends before the proof assignment.

theorem forall_irreducible_range_eq_compact_iff_component_compact_homeomorph :
    (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K],
      ∀ pi : NonUnitalCStarRepresentation A K, pi.IsIrreducible →
        (NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K) ↔
    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,
      ClosureSpace.HasCompactOperatorHomeomorph.{u, u}
        ((NormedSpace.geometricStructureClosure ℂ A).subspace
          ((NormedSpace.geometricStructureClosure ℂ A).component I))

The component condition uses the following separate exact definition, including its complete right-hand side: GCRCharacterization.lean.

def HasCompactOperatorHomeomorph.{uH, uX} {X : Type uX}
    (c : ClosureSpace X) : Prop :=
  ∃ (H : Type uH) (instN : NormedAddCommGroup H),
    letI := instN
    ∃ instI : InnerProductSpace ℂ H,
      letI := instI
      ∃ instC : CompleteSpace H,
        letI := instC
        ∃ instT : Nontrivial H,
          letI := instT
          Nonempty (Homeomorph c
            (NormedSpace.geometricStructureClosure ℂ
              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))

In the source	Mathematical meaning
Exact declaration Ambient inputs `variable {A : Type u} [NonUnitalCStarAlgebra A] [hA : Nontrivial A]` `attribute [local instance] _root_.CStarAlgebra.spectralOrder` `_root_.CStarAlgebra.spectralOrderedRing`	The nonzero complex C*-algebra . The two local instances give its compatible spectral order, used for positivity and pure states. They do not introduce another choice of order. The separate `include hA in` shown below retains nontriviality in this theorem; no unit is required.
Exact declaration Representation quantifiers `(∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K],` `∀ pi : NonUnitalCStarRepresentation A K, pi.IsIrreducible →`	Every complex Hilbert space and every irreducible -representation . Here source `K` is the representation space called in the Statement. Its norm, complex inner product and completeness are required by the three bracketed inputs. Irreducibility includes a nonzero action, not faithfulness.
Exact declaration Representation condition `(NonUnitalStarAlgHom.range pi) = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K) ↔`	The image of this same representation is exactly the compact-operator algebra: $\pi(A)=\mathcal K(H).$ This is (1). The outer `↔` relates the universal representation condition to the component condition on its right.
Exact declaration Component quantifier `∀ I : NormedSpace.GeometricStructureSpace ℂ A,`	Every point . The model space and comparison map required after this quantifier may depend on .
Exact declaration Comparison applied to the component `ClosureSpace.HasCompactOperatorHomeomorph.{u, u}` `((NormedSpace.geometricStructureClosure ℂ A).subspace` `((NormedSpace.geometricStructureClosure ℂ A).component I))`	Apply the displayed comparison definition to the closure induced on . `geometricStructureClosure ℂ A` is the closure on ; its `component I` is the point set . `subspace` makes that set a closure space, with $c_{C_A(I)}(E)=C_A(I)\cap c_A(E)$ for . This closure is the argument `c` of the definition above, and its underlying set is `X`.
Exact declaration Model and inner product `∃ (H : Type uH) (instN : NormedAddCommGroup H),` `letI := instN` `∃ instI : InnerProductSpace ℂ H,` `letI := instI`	The condition requires a model space , called `H` in this definition, with the following structures. `instN` gives its normed additive group, and `instI` its complex inner product. Each following `letI` uses that choice on the same space, first to form `InnerProductSpace ℂ H`, then to interpret the remaining Hilbert-space conditions.
Exact declaration Completeness and nonzero model `∃ instC : CompleteSpace H,` `letI := instC` `∃ instT : Nontrivial H,` `letI := instT`	`instC` requires this same to be complete; `instT` requires . Their `letI` declarations retain these structures when forming bounded operators, the compact-operator algebra and its geometric closure. They do not choose a second space.
Exact declaration Homeomorphism existence `Nonempty (Homeomorph c` `(NormedSpace.geometricStructureClosure ℂ` `(ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))`	`Nonempty` requires an element of this `Homeomorph` type: one bijection with both continuity fields below. Its target closure is on the geometric structure of the compact-operator algebra on the same model , not on itself.
Exact declaration Homeomorphism and forward field `structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where` `continuous_toFun : c.Continuous d toFun`	`extends α ≃ β` supplies the bijection, extracted as `e.toEquiv`. Its forward map `toFun` is . In this application, and , so the first field says $e(c_{C_A(I)}(E))\subseteq c_{\mathcal K(K)}(e(E))$ for every .
Exact declaration Inverse field of the same homeomorphism `continuous_invFun : d.Continuous c invFun`	`invFun`, also written `e.toEquiv.symm`, is the inverse of that same . The second field says $e^{-1}(c_{\mathcal K(K)}(F))\subseteq c_{C_A(I)}(e^{-1}(F))$ for every . Together the two fields give the arbitrary-set closure equality (2).
Exact declaration Continuity definition `def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=` `∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`	For a map , continuity means $r(c_Y(E))\subseteq c_Z(r(E))$ for every . Source `α`, `β`, `c`, `d`, `f` denote ; the double prime denotes the set image . Unlike `FinitelyContinuous`, this definition has no finiteness restriction.

Size scope: the principal equivalence fixes the universe of and quantifies both representation spaces and compact-model spaces in that same universe. The separately cited transport theorem allows an independently specified Hilbert-space universe; it does not change the quantifiers of this declaration.

Exact surrounding source context (separate excerpts)

GCRCharacterization.lean.

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

GCRCharacterization.lean.

include hA in

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

Technical documentation