One-sided compact representability gives GSS rigidity

MathlibAnnex.Analysis.CStarAlgebra.nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_exists_isCompactlyRepresented

theorem

Obtains algebraic rigidity when either side admits a faithful compact action.

Statement

Let be complex C*-algebras. 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 its hull–kernel closure:

c_D(E)=\left\{I\in S(D):\bigcap_{J\in E}J\subseteq I\right\},\qquad E\subseteq S(D).

These are the geometric structure definition and its closure, with the norm-one description justified by the norm-one support characterization. Let denote the algebra of compact operators on a complex Hilbert space .

Assume that at least one of admits a faithful -representation on a complex Hilbert space whose image is contained in . Then and are -isomorphic if and only if and are homeomorphic as closure spaces. Here a closure-space homeomorphism is a bijection satisfying

e(c_A(E))=c_B(e(E)),\qquad E\subseteq S(A).

The equality is required for every subset, not just finite subsets.

Assumptions

A faithful compact-valued representation is required on at least one side. All Hilbert spaces are complex and complete. The algebras and representation spaces may be zero. Representations need not be unital; no separability or countability assumption is imposed.

Conclusion

The equivalence concerns existence of a -algebra isomorphism and existence of a closure-space homeomorphism. It does not require the isomorphism to induce a prescribed homeomorphism, or assert uniqueness.

Main citations

The either-side compact rigidity theorem is the stated equivalence. Rigidity for a given compact action allows an independent Hilbert universe and uses the canonical compact c0-decomposition. The existential representation comparison links the existential condition to the same reduced atomic action.

Lean source signature (exact)

Exact source and declaration. Only the literal signature is displayed here; the linked source retains the proof.

theorem nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_exists_isCompactlyRepresented
    (hCompact :
      (∃ (K : Type u) (normed : NormedAddCommGroup K),
        letI : NormedAddCommGroup K := normed
        ∃ inner : InnerProductSpace ℂ K,
          letI : InnerProductSpace ℂ K := inner
          ∃ complete : CompleteSpace K,
            letI : CompleteSpace K := complete
            ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented) ∨
      (∃ (K : Type v) (normed : NormedAddCommGroup K),
        letI : NormedAddCommGroup K := normed
        ∃ inner : InnerProductSpace ℂ K,
          letI : InnerProductSpace ℂ K := inner
          ∃ complete : CompleteSpace K,
            letI : CompleteSpace K := complete
            ∃ pi : NonUnitalCStarRepresentation B K, pi.IsCompactlyRepresented)) :
    Nonempty (A ≃⋆ₐ[ℂ] B) ↔
      Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A)
        (NormedSpace.geometricStructureClosure ℂ B))

Back to the reading-guide item

In the source	Mathematical meaning
Two C*-algebras`variable {A : Type u} {B : Type v} variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]`Fixed source	The inputs are arbitrary complex C*-algebras, including zero. Their size levels are independent. The nonunital representation type imposes no requirement that either algebra lack a unit.
Representation space on the A side`(∃ (K : Type u) (normed : NormedAddCommGroup K), letI : NormedAddCommGroup K := normed ∃ inner : InnerProductSpace ℂ K, letI : InnerProductSpace ℂ K := inner`Fixed source	The left alternative requires a space with a norm and compatible complex inner product. The source calls it `K`; it is the space of the Statement. Each `letI` makes the chosen structure on that same space available in the next type.
Complete faithful compact action on A`∃ complete : CompleteSpace K, letI : CompleteSpace K := complete ∃ pi : NonUnitalCStarRepresentation A K, pi.IsCompactlyRepresented) ∨`Fixed source	The next existential requires completeness of that space. Its `letI` makes the Hilbert-space representation type available. There must then exist a faithful with . The final disjunction permits the alternative on the side.
Representation space on the B side`(∃ (K : Type v) (normed : NormedAddCommGroup K), letI : NormedAddCommGroup K := normed ∃ inner : InnerProductSpace ℂ K, letI : InnerProductSpace ℂ K := inner`Fixed source	The right alternative has its own existentially quantified normed space and compatible complex inner product, again installed by `letI`. It is not required to be the representation space of the alternative.
Complete faithful compact action on B`∃ complete : CompleteSpace K, letI : CompleteSpace K := complete ∃ pi : NonUnitalCStarRepresentation B K, pi.IsCompactlyRepresented)) :`Fixed source	This space must be complete, and must admit a faithful with . The two complete representation conditions are alternatives, not simultaneous requirements.
Meaning of compact representability`def NonUnitalCStarRepresentation.IsCompactlyRepresented (pi : NonUnitalCStarRepresentation A H) : Prop := Function.Injective pi ∧ ∀ a : A, IsCompactOperator (pi a)`Fixed source	For whichever algebra is represented, injectivity is faithfulness and the second conjunct is compactness of every represented element. Surjectivity onto all of is not required.
Existence of a star-isomorphism`Nonempty (A ≃⋆ₐ[ℂ] B) ↔`Fixed source	`Nonempty` asserts that the type of -algebra isomorphisms has an element. The equivalence relates this existence to the existence in the next row; it selects neither a unique isomorphism nor a prescribed one.
Existence of a closure-space homeomorphism`Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A) (NormedSpace.geometricStructureClosure ℂ B)) := by`Fixed source	The two full arguments are the geometric closures on and on . `Nonempty` requires one homeomorphism between these closure spaces.
The same map and inverse`structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where continuous_toFun : c.Continuous d toFun continuous_invFun : d.Continuous c invFun`Fixed source	The inherited equivalence supplies the bijection and its inverse . The two fields require, for every and respectively, $e(c_A(E))\subseteq c_B(e(E)),$ $e^{-1}(c_B(F))\subseteq c_A(e^{-1}(F)).$ Both use the same ; together they give the closure equality in the Statement.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

universe u v w

variable {A : Type u} {B : Type v}
variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]
variable {H : Type w} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

Back to the reading-guide item

The two existential Hilbert spaces have the fixed size levels of their respective algebras (u for , v for ). The independently sized space in the cited fixed-action theorem does not change these quantifiers.

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

Technical documentation