GSS rigidity when either algebra is finite-dimensional

MathlibAnnex.Analysis.CStarAlgebra.nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_finiteDimensional_or

theorem

Obtains algebraic rigidity when either algebra is finite-dimensional.

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.

Assume that at least one of is finite-dimensional as a complex vector space. 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

Finite-dimensionality is required on at least one side, not on both as an input. The algebras may be zero. No nonzero, unitality, separability, or prescribed dimension hypothesis 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 finite-dimensional theorem uses the finite separating GNS representation theorem and rigidity for a given compact action. The finite separating family and compact action are supplied by these results, not additional hypotheses.

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_finiteDimensional_or
    (hfinite : FiniteDimensional ℂ A ∨ FiniteDimensional ℂ B) :
    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 source type allows unital algebras but does not require a unit.
Finite-dimensionality on either side`(hfinite : FiniteDimensional ℂ A ∨ FiniteDimensional ℂ B) :`Fixed source	The disjunction requires or . One side suffices, and no particular dimension or positivity condition is imposed.
Existence of a star-isomorphism`Nonempty (A ≃⋆ₐ[ℂ] B) ↔`Fixed source	`Nonempty` says that the type of -algebra isomorphisms has an element. The outer equivalence relates this existence to the existence in the next row, not to a choice of a prescribed map.
Existence of a closure-space homeomorphism`Nonempty (ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ A) (NormedSpace.geometricStructureClosure ℂ B)) := by`Fixed source	The complete arguments are 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 first field requires, for every , $e(c_A(E))\subseteq c_B(e(E)).$ The second requires, for every , $e^{-1}(c_B(F))\subseteq c_A(e^{-1}(F)).$ Both concern the same and together express the closure equality in the Statement.
Continuity for arbitrary subsets`def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	For a map , continuity means $r(c(E))\subseteq d(r(E))\quad(E\subseteq X).$ In the preceding row this definition is applied first to and then to , with the domain and target closures interchanged.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

universe u v w z

variable {A : Type u} {B : Type v}
variable [NonUnitalCStarAlgebra A] [NonUnitalCStarAlgebra B]

Back to the reading-guide item

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

Technical documentation