A specified GSS homeomorphism preserves compact-operator equality

MathlibAnnex.Analysis.CStarAlgebra.eq_compactOperatorStarSubalgebra_iff_of_geometricStructure_homeomorph

theorem

Preserves equality with the compact operators under the specified full geometric homeomorphism.

Statement

Let be complex Hilbert spaces, and let and be nonzero norm-closed complex -subalgebras acting irreducibly on and , respectively. Write for the geometric structure space of , with hull–kernel closure , and write for the algebra of compact operators on .

For each maximal proper face of the closed unit ball of , take the union of the kernels of all bounded complex-linear functionals of norm one that equal on that face. The distinct subsets so obtained are the points of , by the geometric structure definition and the norm-one support characterization.

Suppose that is a homeomorphism of closure spaces. Equivalently, is a bijection preserving closure for all subsets:

e(c_{A_1}(E))=c_{A_2}(e(E))\qquad(E\subseteq S(A_1)). \tag{1}

Then

A_1=\mathcal K(H)\quad\Longleftrightarrow\quad A_2=\mathcal K(K). \tag{2}

Assumptions

The Hilbert spaces are complete. Irreducibility supplies nonzero Hilbert spaces. No separability or finite-dimensionality is assumed. The homeomorphism uses the same and its inverse. In terms of continuity, (1) requires

e(c_{A_1}(E))\subseteq c_{A_2}(e(E))\qquad(E\subseteq S(A_1)),

and

e^{-1}(c_{A_2}(F))\subseteq c_{A_1}(e^{-1}(F))\qquad(F\subseteq S(A_2)).

No hypothesis says that directly maps onto , the normal parts consisting of their coefficient kernels.

Conclusion

The conclusion is equality with the compact-operator algebra on each original Hilbert space, not merely containment or abstract -isomorphism. The specified geometric homeomorphism is not asserted to be induced by a -isomorphism. Finite continuity alone is not the hypothesis.

Main citations

Compact-equality transport is the equality branch for the specified full homeomorphism. It uses faithful normal-part transport, equality transport between normal parts, and equality reflection through a faithful irreducible image. The distinct compact-inclusion, proper-inclusion, and zero-intersection results are not substituted for equality.

Lean source signature (exact)

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

theorem eq_compactOperatorStarSubalgebra_iff_of_geometricStructure_homeomorph :
    S = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ↔
      T = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K

Back to the reading-guide item

In the source, S and T denote the algebras and used here, respectively.

In the source	Mathematical meaning
Hilbert spaces`universe u v w variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]`Fixed source	The complete complex Hilbert spaces may have independent universe levels.
Closed operator algebras`variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K)) variable [IsClosed (S : Set (H →L[ℂ] H))] [IsClosed (T : Set (K →L[ℂ] K))]`Fixed source	The source names denote and . Each is a norm-closed complex -subalgebra.
Irreducible actions`variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) variable (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))`Fixed source	The inclusion representations of on and on are nonzero and irreducible. No finite-dimensionality or separability is assumed.
Specified geometric homeomorphism`variable (e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ S) (NormedSpace.geometricStructureClosure ℂ T))`Fixed source	The same given is a homeomorphism of the ambient geometric closure spaces. It is not assumed to send one normal part directly onto the other.
Inherited algebra and order structures`local instance : NonUnitalCStarAlgebra T := NonUnitalStarSubalgebra.nonUnitalCStarAlgebra T (h_closed := inferInstance) local instance : PartialOrder T := _root_.CStarAlgebra.spectralOrder T local instance : StarOrderedRing T := _root_.CStarAlgebra.spectralOrderedRing T`Fixed source	The closed operator algebra carries its inherited C*-algebra structure and compatible order. These local instances are structures on the same algebra; they add no hypothesis to the displayed theorem.
Effective theorem inputs`include hS hT e in`Fixed source	The two irreducibility assumptions and the specified are included in the theorem even though its displayed conclusion mentions only the algebras and compact operators.
Equality with compact operators`theorem eq_compactOperatorStarSubalgebra_iff_of_geometricStructure_homeomorph : S = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H ↔ T = ContinuousLinearMap.compactOperatorStarSubalgebra ℂ K := by`Fixed source	The conclusion is exactly $A_1=\mathcal K(H)\quad\Longleftrightarrow\quad A_2=\mathcal K(K).$ It concerns equality on the original Hilbert spaces, not merely compact containment or an abstract isomorphism.
Homeomorphism fields`structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where continuous_toFun : c.Continuous d toFun continuous_invFun : d.Continuous c invFun`Fixed source	The underlying equivalence is the same with inverse . The forward continuity field states, for every , $e(c_{A_1}(E))\subseteq c_{A_2}(e(E)).$ The inverse continuity field states, for every , $e^{-1}(c_{A_2}(F))\subseteq c_{A_1}(e^{-1}(F)).$ The inverse is not an independently selected map.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

universe u v w
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]

Back to the reading-guide item

Exact surrounding source:

variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K))
variable [IsClosed (S : Set (H →L[ℂ] H))] [IsClosed (T : Set (K →L[ℂ] K))]
variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))
variable (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))
variable (e : ClosureSpace.Homeomorph
  (NormedSpace.geometricStructureClosure ℂ S)
  (NormedSpace.geometricStructureClosure ℂ T))

local instance : NonUnitalCStarAlgebra T :=
  NonUnitalStarSubalgebra.nonUnitalCStarAlgebra T
    (h_closed := inferInstance)
local instance : PartialOrder T := _root_.CStarAlgebra.spectralOrder T
local instance : StarOrderedRing T := _root_.CStarAlgebra.spectralOrderedRing T

Back to the reading-guide item

Exact surrounding source:

include hS hT e in

Back to the reading-guide item

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

Technical documentation