A continuous finite comparison with a compact-operator GSS

ClosureSpace.HasContinuousFiniteCompactComparison

def

Requires a finite homeomorphism to a compact-operator geometric space whose forward map is fully continuous.

Statement

Let be a closure space. A continuous finite compact comparison is the existence of a nonzero complex Hilbert space and a finite homeomorphism from to the geometric structure closure space whose forward map is also fully continuous.

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 .

For closure spaces , full continuity of means for every . Finite continuity requires this only for finite . The condition holds when there exists a bijection such that and are finitely continuous, and additionally

e(c(E))\subseteq c_{\mathcal K(H)}(e(E))\quad(E\subseteq X).

The norm and inner product belong to the same nonzero Hilbert space . Full continuity of is not required by this condition.

Assumptions

The input is an arbitrary closure space. It need not already be presented as a GSS or an operator-algebra normal part. There is no representation of a C*-algebra in the input or conclusion. The model Hilbert space is nonzero; no separability or finite-dimensionality is required.

Conclusion

This is an existence property of a closure space, with forward full continuity added to finite continuity of a bijection and its inverse. No representation range condition is part of this definition.

Main citations

Exact defining expression.
The full-homeomorphism condition, which requires full continuity in both directions.

Lean source signature (exact)

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

def HasContinuousFiniteCompactComparison.{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
          ∃ e : FiniteHomeomorph c
              (NormedSpace.geometricStructureClosure ℂ
                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)),
            c.Continuous (NormedSpace.geometricStructureClosure ℂ
              (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) e.toEquiv

Back to the reading-guide item

In the source	Mathematical meaning
Input closure`def HasContinuousFiniteCompactComparison.{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.
Finite comparison with the compact-operator GSS`∃ e : FiniteHomeomorph c (NormedSpace.geometricStructureClosure ℂ (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)),`Fixed source	There must exist one finite homeomorphism $e:X\to S(\mathcal K(H)).$ The target closure is , the geometric closure of the compact-operator algebra on this same , not a closure on . For every finite , $e(c(F))=c_{\mathcal K(H)}(e(F)).$
Full forward continuity of the same map`c.Continuous (NormedSpace.geometricStructureClosure ℂ (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)) e.toEquiv`Fixed source	`e.toEquiv` is the bijection underlying that same finite homeomorphism. The remaining condition is, for every , $e(c(E))\subseteq c_{\mathcal K(H)}(e(E)).$ It imposes no full-continuity condition on .
Finite continuity in both directions`structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where finitelyContinuous_toFun : c.FinitelyContinuous d toFun finitelyContinuous_invFun : d.FinitelyContinuous c invFun`Fixed source	The inherited equivalence supplies and . The two fields require finite continuity of these maps in opposite directions. Together they give the finite closure equality above; full continuity of the forward map is the extra condition in the preceding row.
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