A finite-dimensional compact model with a dimension condition

ClosureSpace.HasFiniteDimensionalCompactHomeomorph

def

Requires a finite-dimensional compact model satisfying a specified condition on its dimension.

Statement

Let be a closure space and let be a condition on a natural number . The finite-dimensional compact-homeomorphism condition holds when there exist a nonzero finite-dimensional complex Hilbert space satisfying and a full homeomorphism .

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 .

All the following data refer to the same : its norm, complex inner product and completeness, nontriviality, finite-dimensionality, the truth of , and a full closure-space homeomorphism

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

Full continuity applies to arbitrary subsets in both directions. Finite-dimensionality is required separately from the condition on its finite complex dimension.

Assumptions

The input consists only of and . The condition requires the existence of the Hilbert space, its finite-dimensionality, and the stated dimension condition. Nonzero is explicit in the literal right-hand side. No separability hypothesis is added. Here the natural number dimension is finite complex vector-space dimension; later infinite-dimensional comparisons use Hilbert-basis cardinality separately.

Conclusion

One finite-dimensional Hilbert space must satisfy both the dimension condition and the homeomorphism requirement. Taking to be specifies an exact dimension; taking it to be specifies an upper bound. Neither choice replaces the explicit finite-dimensionality and nonzero-model conditions.

Main citations

Lean source signature (exact)

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

def HasFiniteDimensionalCompactHomeomorph.{uH, uX} {X : Type uX}
    (c : ClosureSpace X) (P : ℕ → Prop) : Prop :=
  ∃ (H : Type uH) (instN : NormedAddCommGroup H),
    letI := instN
    ∃ instI : InnerProductSpace ℂ H,
      letI := instI
      ∃ instC : CompleteSpace H,
        letI := instC
        ∃ instT : Nontrivial H,
          letI := instT
          FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) ∧
            Nonempty (Homeomorph c
              (NormedSpace.geometricStructureClosure ℂ
                (ContinuousLinearMap.compactOperatorStarSubalgebra ℂ H)))

Back to the reading-guide item

In the source	Mathematical meaning
Input closure and dimension condition`def HasFiniteDimensionalCompactHomeomorph.{uH, uX} {X : Type uX} (c : ClosureSpace X) (P : ℕ → Prop) : Prop :=`Fixed source	The input is the closure on . The second input is the condition on a natural number . 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-dimensionality and its dimension condition`FiniteDimensional ℂ H ∧ P (Module.finrank ℂ H) ∧`Fixed source	The same must be finite-dimensional, and its finite complex dimension must satisfy . These are two conditions. The finite-dimensionality requirement is not replaced by a condition on `finrank`.
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

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