Two-sided continuity is exact operator equality

MathlibAnnex.Analysis.CStarAlgebra.continuous_normalPartLinearMap_and_inverse_iff

theorem

Characterizes two-sided continuity of a normal-part equivalence by equality of operator sets.

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

\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}

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

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

Let be bounded complex-linear isomorphisms with bounded inverses. The maps on normal points are

\begin{aligned} F:N(A)\longrightarrow N(B),&\qquad F(\ker f^{A}_{x,y})=\ker f^{B}_{Ux,Vy},\\ F^{-1}:N(B)\longrightarrow N(A),&\qquad F^{-1}(\ker f^{B}_{z,w})=\ker f^{A}_{U^{-1}z,V^{-1}w}. \end{aligned} \tag{1}

The normal-part equivalence guarantees that these are inverse bijections, and its point-evaluation theorem guarantees the formulas for every representative. For the inherited hull–kernel closures,

F\text{ and }F^{-1}\text{ are fully continuous} \quad\Longleftrightarrow\quad V^*BU=A. \tag{2}

Here is the adjoint of , and . For , write . For , write . Full continuity of means

F(c_{A}(D))\subseteq c_{B}(F(D))\qquad\text{for every }D\subseteq N(A),

and full continuity of its inverse means

F^{-1}(c_{B}(E))\subseteq c_{A}(F^{-1}(E))\qquad\text{for every }E\subseteq N(B).

Assumptions

Boundedness of the vector maps and their inverses is part of the input, making their adjoints bounded operators in the indicated directions. They are not assumed unitary or assumed to intertwine . The map is the inverse arising from the same , not an independently chosen map. The equality on the right of (2) is a conclusion equivalent to the two continuities, not an additional hypothesis on both sides.

Conclusion

Two-sided full continuity is equivalent to equality of concrete operator sets in . It is stronger than the finite-homeomorphism property obtained from the algebraic vector changes alone. No assertion is made that the operator transport is multiplicative or preserves adjoints.

Main citations

One-direction full continuity: the related inclusion criterion for the same specified forward map.
Exact two-sided bounded criterion: forward and inverse maps use the same bounded equivalences.
arXiv:2504.05551v1, Theorem 6.9: the full-homeomorphism image condition.
The bounded operator transport: adjointSandwich U V b is exactly the composite , from to .
Normal-part point evaluation and its inverse equivalence: the same vector changes define the map and its inverse.

Lean source signature (exact)

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

theorem continuous_normalPartLinearMap_and_inverse_iff (U V : H ≃L[ℂ] K) :
    (((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous
        ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T))
        (normalPartSemilinearMap S T hT U.toLinearEquiv V.toLinearEquiv) ∧
      ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)).Continuous
        ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))
        (normalPartSemilinearMap T S hS U.symm.toLinearEquiv V.symm.toLinearEquiv)) ↔
      InnerProductSpace.adjointSandwich U.toContinuousLinearMap V.toContinuousLinearMap ''
        (T : Set (K →L[ℂ] K)) = (S : Set (H →L[ℂ] H))

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 spaces are complex Hilbert spaces. The source algebras `S`,`T` are and . Closedness and the two inclusion representations express the nonzero norm-closed irreducible actions in the Statement.
Bounded linear isomorphisms`theorem continuous_normalPartLinearMap_and_inverse_iff (U V : H ≃L[ℂ] K) :`Fixed source	The same two bounded complex-linear isomorphisms , with bounded inverses, define and in (1).
Forward closure continuity`(((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) (normalPartSemilinearMap S T hT U.toLinearEquiv V.toLinearEquiv) ∧`Fixed source	The `subspace` arguments give the relative closures on and . The underlying linear equivalences are the same , with their boundedness forgotten only in this map constructor. For every , $F(c_A(D))\subseteq c_B(F(D)).$
Inverse closure continuity`((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)).Continuous ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) (normalPartSemilinearMap T S hS U.symm.toLinearEquiv V.symm.toLinearEquiv)) ↔`Fixed source	The second map uses the actual inverses , with the algebras exchanged. For every , $F^{-1}(c_B(E))\subseteq c_A(F^{-1}(E)).$ These two conditions, joined by conjunction, are the left side of (2).
Adjoint composition`def adjointSandwich (U V : H →L[𝕜] K) (b : K →L[𝕜] K) : H →L[𝕜] H := V.adjoint.comp (b.comp U)`Fixed source	For this is the bounded operator , in exactly that order. The adjoint is taken for the same Hilbert structures.
Equality of operator sets`InnerProductSpace.adjointSandwich U.toContinuousLinearMap V.toContinuousLinearMap '' (T : Set (K →L[ℂ] K)) = (S : Set (H →L[ℂ] H)) :=`Fixed source	The image operation applies to . The right side is $V^BU=\{V^bU:b\in B\}=A.$ The theorem makes this equivalent to both continuity conditions for the same . It does not assert that preserves multiplication or the involution.

The two displayed maps are inverse maps induced by the same bounded equivalences; the later bundled full-homeomorphism definition is not included.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

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))

Back to the reading-guide item

The effective source context uses independent universes for and . The adjoint in is the bounded Hilbert-space adjoint from to . The literal definition is V.adjoint.comp (b.comp U); its order is the same as the operator formula above.

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

Technical documentation