Finite-homeomorphisms detect finite dimension

MathlibAnnex.Analysis.CStarAlgebra.finite_and_finrank_eq_of_normalPart_finiteHomeomorph

theorem

Recovers finite dimensionality and equal dimensions from a finite-homeomorphism of normal parts.

Statement

Let be complex Hilbert spaces. Let and be nonzero norm-closed complex -subalgebras acting irreducibly on and , respectively. Neither algebra is assumed unital. For and , define the coefficient functionals

\begin{aligned} f^A_{x,y}:A\to\mathbb C,&\qquad f^A_{x,y}(a)=\langle y,a(x)\rangle,\\ f^B_{z,w}:B\to\mathbb C,&\qquad f^B_{z,w}(b)=\langle w,b(z)\rangle. \end{aligned}

The inner products are conjugate-linear in the first variable. The normal parts are

\begin{aligned} N(A)&=\{\ker f^A_{x,y}:x,y\in H\setminus\{0\}\},\\ N(B)&=\{\ker f^B_{z,w}:z,w\in K\setminus\{0\}\}. \end{aligned}\tag{1}

Give the two normal parts their inherited hull–kernel closures . For , write , and define analogously.

Suppose is a finite-homeomorphism, that is, a bijection satisfying

e(c_A(D))=c_B(e(D))\qquad\text{for every finite }D\subseteq N(A).

If either or is finite dimensional, then both are finite dimensional and

\dim_{\mathbb C}H=\dim_{\mathbb C}K.\tag{2}

Assumptions

The given finite-homeomorphism is a bijection whose map and inverse preserve closure on finite subsets. Continuity on arbitrary subsets is not assumed. The nonzero norm-closed -subalgebras act irreducibly on , respectively.

Finite dimensionality is required on at least one side. There is no dimension-at-least-three hypothesis: dimensions one and two are included. The nonzero actions exclude the zero Hilbert space.

Conclusion

Both spaces are finite dimensional, and their complex dimensions agree. The conclusion asserts finite dimensionality as well as equality of dimensions.

Main citations

The normal-part dimension theorem gives both finite-dimensionality assertions and equality of dimensions. Its algebraic input is the finite-incidence dimension theorem. The finite-homeomorphism definition specifies the two finite-continuity conditions. See also the retained paper's Theorem 6.18, pages 42–45.

Lean source signature (exact)

The declaration prefix below is a contiguous source excerpt, ending before its proof assignment.

The parameter is declared earlier by variable, rather than repeated after the theorem name. Immediately before this declaration, include hS hT e in tells Lean to add the two irreducibility hypotheses and as parameters of this theorem. Thus the theorem takes the given finite-homeomorphism as an input, although its conclusion mentions only the dimensions of and . The exact variable and include declarations are quoted in the source context below.

theorem finite_and_finrank_eq_of_normalPart_finiteHomeomorph
    (hfinite : Module.Finite ℂ H ∨ Module.Finite ℂ K) :
    Module.Finite ℂ H ∧ Module.Finite ℂ K ∧ Module.finrank ℂ H = Module.finrank ℂ 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 and irreducible algebrasvariable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] 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 complex Hilbert spaces carry the nonzero norm-closed irreducible algebras , called `S`,`T` in the source. Completeness belongs to each Hilbert structure. No unit is required.
Finite-homeomorphism input`variable (e : ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))`Fixed source	The parameter is a bijection , with the induced closures on these normal parts. For every finite , $e(c_A(D))=c_B(e(D)).$ This is an input, not a map obtained in the conclusion.
Parameters retained by include`include hS hT e in`Fixed source	The command retains the previously declared irreducibility hypotheses and the same as parameters of this theorem, although the displayed conclusion concerns only dimensions.
One finite-dimensional space`(hfinite : Module.Finite ℂ H ∨ Module.Finite ℂ K) :`Fixed source	The hypothesis is that or is finite-dimensional over . It is a disjunction, not a requirement that both are already known to be finite-dimensional.
Both dimensions and their equality`Module.Finite ℂ H ∧ Module.Finite ℂ K ∧ Module.finrank ℂ H = Module.finrank ℂ K :=`Fixed source	The conclusion has three conjuncts: is finite-dimensional, is finite-dimensional, and $\dim_{\mathbb C}H=\dim_{\mathbb C}K.$ The numerical equality is additional to the two finite-dimensionality assertions; no lower dimension bound is imposed.

The displayed declaration prefix and the following ambient context are separate excerpts. The next include and comment in the source are not part of this declaration.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

universe u v
variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
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

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