A full homeomorphism to a compact-operator GSS

ClosureSpace.HasCompactOperatorHomeomorph

def

Requires a full homeomorphism to the geometric structure space of a compact-operator algebra.

Statement

Let be a closure space. The compact-operator homeomorphism condition holds when is fully homeomorphic to for some nonzero complex Hilbert space .

Definition

Here denotes the algebra of compact operators on . For a complex normed space , consists of the unions of kernels of norm-one bounded complex-linear functionals supporting each maximal proper face of its closed unit ball. Faces use real convexity. The support-functional norm theorem justifies the norm-one description for these nonempty faces. Its closure is .

The condition requires a nonzero complex Hilbert space and a closure-space homeomorphism

e:(X,c)\longrightarrow S(\mathcal K(H)).

This is a bijection with full continuity in both directions. Explicitly, the required inclusions are for every , and for every target subset . The inverse is the inverse of the same bijection. Existence is required; no preferred homeomorphism is selected.

Assumptions

Only the input closure space is given. The Hilbert space and its structures are existential data. Nonzero is required; separability and finite dimension are not. The definition uses arbitrary-set closure and does not replace it by finite closure.

Conclusion

This condition requires a full geometric model, with both directions referring to the same bijection. A continuous finite comparison is a separate condition; it does not contain the inverse full-continuity field required here. No statement about an irreducible representation image is included in this definition.

Main citations

Lean source signature (exact)

Exact source and declaration. The complete defining right-hand side is included.

def HasCompactOperatorHomeomorph.{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
          Nonempty (Homeomorph c
            (NormedSpace.geometricStructureClosure ℂ
              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))

Back to the reading-guide item

In the source	Mathematical meaning
Input closure`def HasCompactOperatorHomeomorph.{uH, uX} {X : Type uX} (c : ClosureSpace X) : Prop :=`Fixed source	The input is the closure on . The following existential statement defines the requested model condition; it does not select a preferred model or map.
One normed model space`∃ (H : Type uH) (instN : NormedAddCommGroup H), letI := instN`Fixed source	There must exist one normed additive group . The first `letI` installs that chosen normed structure on for the inner-product type that follows.
Complex inner product on that model`∃ instI : InnerProductSpace ℂ H, letI := instI`Fixed source	The same must have a compatible complex inner product. This `letI` installs it for the later Hilbert-space and operator-algebra types.
Completeness of that model`∃ instC : CompleteSpace H, letI := instC`Fixed source	The same normed space must be complete. The next `letI` installs this completeness, used in the compact-operator algebra on this Hilbert space.
A nonzero model`∃ instT : Nontrivial H, letI := instT`Fixed source	The same must be nonzero. Its `letI` makes this nontriviality available in the remaining conditions; it does not introduce another space.
Existence of a homeomorphism to the same model`Nonempty (Homeomorph c (NormedSpace.geometricStructureClosure ℂ (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))`Fixed source	`Nonempty` requires an element of the displayed homeomorphism type: one bijection $e:X\to S(\mathcal K(H))$ with continuity in both directions. The complete target argument is the geometric closure on the compact-operator algebra of the same used in all preceding conditions.
The homeomorphism and its 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 gives and its inverse . For every and , the two fields require, respectively, $e(c(E))\subseteq c_{\mathcal K(H)}(e(E)),$ $e^{-1}(c_{\mathcal K(H)}(F))\subseteq c(e^{-1}(F)).$ Both use the same model and the same map; the definition does not choose separate forward and inverse maps.
Continuity for all subsets`def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	For , the definition requires $r(d(E))\subseteq k(r(E))\quad(E\subseteq Y).$ There is no finiteness restriction in this condition.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

namespace ClosureSpace

open MathlibAnnex.Analysis.CStarAlgebra
attribute [local instance] ContinuousLinearMap.isClosed_compactOperatorStarSubalgebra

Back to the reading-guide item

The model-space level uH and the input-space level uX are independent fixed parameters. All model structures and conditions above refer to the same quantified .

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

Technical documentation