Forward continuity of normal parts preserves Hilbert-basis cardinality

MathlibAnnex.Analysis.CStarAlgebra.hilbertBasis_lift_mk_eq_of_normalPart_continuous

theorem

Preserves Hilbert-basis cardinality under forward full continuity of a finite normal-part homeomorphism.

Statement

Let be complex Hilbert spaces. Let and be nonzero norm-closed complex -subalgebras acting irreducibly on and , respectively. No unit is required. The inner product is linear in its second variable. For and , define the bounded linear functionals and by and . Their kernels form the normal parts

N(A_1)=\{\ker f^{A_1}_{x,y}:x,y\in H\setminus\{0\}\},\qquad N(A_2)=\{\ker f^{A_2}_{z,w}:z,w\in K\setminus\{0\}\}. \tag{1}

Write and for the relative geometric closures on these normal parts. Thus, for , , and similarly for . Let be a bijection satisfying for every finite . This is the finite-homeomorphism condition. Assume in addition that its forward map is fully continuous:

e(c_{A_1}(\mathcal D))\subseteq c_{A_2}(e(\mathcal D)) \qquad(\mathcal D\subseteq N(A_1)). \tag{2}

For any Hilbert bases of and of , their index cardinalities satisfy

|\iota|=|\kappa|. \tag{3}

The invariant is Hilbert-basis index cardinality, not the cardinality of the vector spaces as sets and not their Hamel dimension.

Assumptions

The bases are arbitrary complete orthonormal families. They need not be countable, and neither space is assumed separable. No infinite-dimensionality, same-type condition on two projective factors, or full continuity of is assumed. Dimensions one and two are included through the finite-dimensional branch. The inclusion representations are nonzero and irreducible, and the algebras are norm closed; unitality is not added.

Conclusion

Forward full continuity preserves Hilbert-basis index cardinality, without assuming full continuity of the inverse. The conclusion neither chooses a basis-to-basis map nor asserts an isometry.

Main citations

The normal-part definition and coefficient-kernel membership theorem identify (1) under the stated closedness and irreducibility assumptions.

The Hilbert-dimension theorem gives (3) from forward full continuity. The related results are the finite-dimensional comparison, the continuous first lift and its inverse, and Hilbert-basis comparison.

Lean source signature (exact)

The preceding variable declarations introduce the two Hilbert spaces, the closed algebras, their irreducible actions, and e. The include hS hT in at the effective inclusion retains the irreducibility assumptions for this theorem. The map e is also a parameter because it occurs in hcont; e.toEquiv is the same bijection with its finite-continuity fields omitted. The following contiguous prefix ends before the proof assignment.

theorem hilbertBasis_lift_mk_eq_of_normalPart_continuous
    (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous
      ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv)
    (b : HilbertBasis ι ℂ H) (c : HilbertBasis κ ℂ K) :
    Cardinal.lift.{uJ} (#ι) = Cardinal.lift.{uI} (#κ)

Back to the reading-guide item

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

In the source	Mathematical meaning
Two Hilbert spaces and basis indices`universe u v uI uJ variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] variable {ι : Type uI} {κ : Type uJ}`Fixed source	The spaces are complex Hilbert spaces, including completeness. The sets index their Hilbert bases.
Closed irreducible 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))] variable (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) variable (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))`Fixed source	The algebras are norm-closed complex -subalgebras of . Their inclusion representations are nonzero and irreducible. No unit is required.
The same finite comparison of normal parts`variable (e : ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))`Fixed source	The relative closures are those on , rather than on the whole geometric structure spaces. One bijection satisfies, for every finite , $e(c_{A_1}(\mathcal D))=c_{A_2}(e(\mathcal D)).$
Effective irreducibility assumptions`include hS hT in`Fixed source	The preceding inclusion retains both irreducibility assumptions as theorem parameters. The already declared is also a parameter because it occurs in the following continuity assumption.
Forward continuity for all subsets`(hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv)`Fixed source	The same bijection is fully continuous in the forward direction: for every , $e(c_{A_1}(\mathcal D))\subseteq c_{A_2}(e(\mathcal D)).$ This is (2); full continuity of is not an input.
Arbitrary Hilbert bases`(b : HilbertBasis ι ℂ H) (c : HilbertBasis κ ℂ K) :`Fixed source	The bases are of and of : arbitrary complete orthonormal families.
Equality of basis-index cardinalities`Cardinal.lift.{uJ} (#ι) = Cardinal.lift.{uI} (#κ) := by`Fixed source	The two basis-index sets have the same cardinality: $\|\iota\|=\|\kappa\|,$ as in (3). The lifts allow Lean to compare cardinalities belonging to different universes. This is Hilbert-basis cardinality, not Hamel dimension or the cardinality of the vector spaces as sets.
Finite continuity of the map and its inverse`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 gives and . Its fields require finite continuity in both directions: for finite and finite , respectively, $e(c_{A_1}(\mathcal D))\subseteq c_{A_2}(e(\mathcal D)),$ $e^{-1}(c_{A_2}(\mathcal E))\subseteq c_{A_1}(e^{-1}(\mathcal E)).$ This is the finite-homeomorphism condition used in the Statement.

Exact surrounding source context (separate excerpts)

NormalPartHilbertDimension.lean:

universe u v uI uJ
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
variable {ι : Type uI} {κ : Type uJ}
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.FiniteHomeomorph
  ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))
  ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))

Back to the reading-guide item

NormalPartHilbertDimension.lean:

include hS hT in

Back to the reading-guide item

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

Technical documentation