GSS rigidity from a full bounded-operator model

MathlibAnnex.Analysis.CStarAlgebra.nonempty_starAlgEquiv_iff_nonempty_geometricStructure_homeomorph_of_exists_boundedOperatorEquiv

theorem

Obtains algebraic rigidity from an actual full bounded-operator model on either side.

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 all bounded complex-linear operators on a complex Hilbert space . Assume that at least one of is -isomorphic to for some such . 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

The bounded-operator model is required on at least one side. It is an isomorphism onto all of , not onto a proper subalgebra. The Hilbert space is complex and complete; it and the algebras may be zero. No nonzero, unitality, separability, countability, or finite-dimensionality 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 bounded-operator model theorem uses the specified left-model equivalence and specified right-model equivalence. The full-range model predicate requires faithfulness and range equal to all bounded operators. The zero-model equivalence retains the zero case. No abstract type-I factor classification is claimed.

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_boundedOperatorEquiv
    (hModel :
      (∃ (L : Type w) (normed : NormedAddCommGroup L),
        letI : NormedAddCommGroup L := normed
        ∃ inner : InnerProductSpace ℂ L,
          letI : InnerProductSpace ℂ L := inner
          ∃ complete : CompleteSpace L,
            letI : CompleteSpace L := complete
            Nonempty (A ≃⋆ₐ[ℂ] (L →L[ℂ] L))) ∨
      (∃ (L : Type z) (normed : NormedAddCommGroup L),
        letI : NormedAddCommGroup L := normed
        ∃ inner : InnerProductSpace ℂ L,
          letI : InnerProductSpace ℂ L := inner
          ∃ complete : CompleteSpace L,
            letI : CompleteSpace L := complete
            Nonempty (B ≃⋆ₐ[ℂ] (L →L[ℂ] L)))) :
    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} [NonUnitalCStarAlgebra A] variable {B : Type v} [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.
Normed model on the A side`(∃ (L : Type w) (normed : NormedAddCommGroup L), letI : NormedAddCommGroup L := normed`Fixed source	This alternative requires a normed additive group, called `L` in the source and in the Statement. The first `letI` installs this chosen normed structure on the same space for the inner-product type that follows.
Complex inner product on the A model`∃ inner : InnerProductSpace ℂ L, letI : InnerProductSpace ℂ L := inner`Fixed source	The same model must have a compatible complex inner product. This `letI` installs that inner product, so subsequent Hilbert-space operator types use this structure, not a separately chosen one.
Complete A model and isomorphism`∃ complete : CompleteSpace L, letI : CompleteSpace L := complete Nonempty (A ≃⋆ₐ[ℂ] (L →L[ℂ] L))) ∨`Fixed source	The model must be complete; the last `letI` installs this completeness for its operator algebra. `Nonempty` requires a -isomorphism onto the entire operator algebra. The two model branches are alternatives; their spaces are quantified separately and may be zero.
Normed model on the B side`(∃ (L : Type z) (normed : NormedAddCommGroup L), letI : NormedAddCommGroup L := normed`Fixed source	This alternative requires a normed additive group, called `L` in the source and in the Statement. The first `letI` installs this chosen normed structure on the same space for the inner-product type that follows.
Complex inner product on the B model`∃ inner : InnerProductSpace ℂ L, letI : InnerProductSpace ℂ L := inner`Fixed source	The same model must have a compatible complex inner product. This `letI` installs that inner product, so subsequent Hilbert-space operator types use this structure, not a separately chosen one.
Complete B model and isomorphism`∃ complete : CompleteSpace L, letI : CompleteSpace L := complete Nonempty (B ≃⋆ₐ[ℂ] (L →L[ℂ] L)))) :`Fixed source	The model must be complete; the last `letI` installs this completeness for its operator algebra. `Nonempty` requires a -isomorphism onto the entire operator algebra. The two model branches are alternatives; their spaces are quantified separately and may be zero.
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} [NonUnitalCStarAlgebra A]
variable {B : Type v} [NonUnitalCStarAlgebra B]
variable {H : Type w} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {K : Type z} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

local instance instSpectralOrderBoundedOperatorModel : PartialOrder A :=
  _root_.CStarAlgebra.spectralOrder A
local instance instSpectralOrderedRingBoundedOperatorModel : StarOrderedRing A :=
  _root_.CStarAlgebra.spectralOrderedRing A

Back to the reading-guide item

The model spaces in the two alternatives have the fixed independent source levels w and z; the algebra levels are u and v. The source names for those model spaces are local to their respective existential branches. No additional ambient Hilbert space is an input to this equivalence.

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

Technical documentation