Compact inclusion in every irreducible image

MathlibAnnex.Analysis.CStarAlgebra.forall_irreducible_compact_le_iff_component_compact_comparison

theorem

Characterizes compact containment in every irreducible image by forward-continuous component comparisons.

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 ,

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

For every , there are a nonzero complex Hilbert space and a bijection such that, for every finite subset ,

e(c_{C_A(I)}(F))=c_{\mathcal K(K)}(e(F)),\tag{2}

and, for the same ,

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

Condition (2) says that is a finite homeomorphism. Condition (3) is its forward continuity for arbitrary subsets; continuity of for arbitrary subsets is not required. Both and may depend on . Here and below, 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. No separability or finite-dimensionality is assumed. The component carries the closure induced from .

Conclusion

Compact containment in every irreducible image is equivalent to the component comparisons (2)–(3). The arbitrary-set condition concerns only the forward map. Equality with the compact operators and inverse continuity are the stronger conditions in the compact-image equality characterization.

Main citations

The compact-inclusion characterization states the equivalence. The forward-continuity comparison condition requires one nonzero compact target, finite continuity both ways and full continuity only forward. The pure-state comparison theorem and transport to an independently specified Hilbert space supply the representation correspondence. This is the compact-inclusion condition; identifying it with another abstract definition of Type I remains an external classification boundary, not an additional conclusion here.

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_compact_le_iff_component_compact_comparison :
    (∀ (K : Type u) [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K],
      ∀ pi : NonUnitalCStarRepresentation A K, pi.IsIrreducible →
        ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K ≤ (NonUnitalStarAlgHom.range pi)) ↔
    ∀ I : NormedSpace.GeometricStructureSpace ℂ A,
      ClosureSpace.HasContinuousFiniteCompactComparison.{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 HasContinuousFiniteCompactComparison.{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
          ∃ e : FiniteHomeomorph c
              (NormedSpace.geometricStructureClosure ℂ
                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)),
            c.Continuous (NormedSpace.geometricStructureClosure ℂ
              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) e.toEquiv

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 `ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K ≤ (NonUnitalStarAlgHom.range pi)) ↔`	The compact operators are contained in the image of this same representation: $\mathcal K(H)\subseteq\pi(A).$ This is (1), not image equality. 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.HasContinuousFiniteCompactComparison.{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 Finite comparison map `∃ e : FiniteHomeomorph c` `(NormedSpace.geometricStructureClosure ℂ` `(ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)),`	There exists a finite homeomorphism . The second closure argument is on the geometric structure of the compact-operator algebra on this same model , not a closure on the vectors of . The finite-homeomorphism fields below give $e(c_{C_A(I)}(F))=c_{\mathcal K(K)}(e(F))$ for every finite , as in (2).
Exact declaration Forward continuity of the same map `c.Continuous (NormedSpace.geometricStructureClosure ℂ` `(ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) e.toEquiv`	`e.toEquiv` denotes this same bijection . This condition is $e(c_{C_A(I)}(E))\subseteq c_{\mathcal K(K)}(e(E))$ for every , as in (3). There is no additional arbitrary-set continuity condition on .
Exact declaration Finite-continuity definition `def FinitelyContinuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop :=` `∀ s : Set α, s.Finite → f '' c.closure s ⊆ d.closure (f '' s)`	For a map between closure spaces, the condition is $r(c_Y(F))\subseteq c_Z(r(F))$ for finite . Here source `α`, `β`, `c`, `d`, `f` denote . The double prime denotes the set image .
Exact declaration Finite-homeomorphism fields `structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where` `finitelyContinuous_toFun : c.FinitelyContinuous d toFun` `finitelyContinuous_invFun : d.FinitelyContinuous c invFun`	`extends α ≃ β` supplies a bijection and its inverse. With and , `toFun` and `invFun` are and . The two fields impose the finite-set condition in the preceding row on these same maps in opposite directions. Together they express the finite 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