Continuity is an operator-inclusion condition

MathlibAnnex.Analysis.CStarAlgebra.continuous_normalPartLinearMap_iff

theorem

Characterizes continuity of a normal-part map by an inclusion 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}

For , the inherited hull–kernel closure is

c_{A}(D)=\left\{I\in N(A):\bigcap_{J\in D}J\subseteq I\right\},

and is defined analogously on subsets of . Let be bounded complex-linear isomorphisms with bounded inverses, and let

F:N(A)\longrightarrow N(B),\qquad F(\ker f^{A}_{x,y})=\ker f^{B}_{Ux,Vy}.

The point-evaluation theorem guarantees this formula for every representative of a normal point. This map satisfies

F\text{ is fully continuous}\quad\Longleftrightarrow\quad V^*B U\subseteq A, \tag{1}

where is the adjoint of and . Here full continuity means

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

Assumptions

The maps and their inverses are bounded. Neither map is assumed unitary, and no intertwining relation is imposed. The operator inclusion in (1) is equivalent to continuity, not an additional hypothesis.

Conclusion

The criterion concerns closure preservation for all subsets of , not just finite subsets. Its right-hand side is an inclusion of subsets of .

Main citations

Exact bounded continuity criterion: continuous_normalPartLinearMap_iff.
General coefficient-transport criterion: continuous_normalPartSemilinearMap_iff, specialized to the identity scalar homomorphism.
arXiv:2504.05551v1, Theorem 6.9: the full-continuity criterion for bounded linear changes of coefficient vectors.
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_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) ↔
      ∀ b : T, InnerProductSpace.adjointSandwich U.toContinuousLinearMap V.toContinuousLinearMap
        (b : K →L[ℂ] K) ∈ S

Back to the reading-guide item

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

In the source	Mathematical meaning
Ambient spaces and 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 and the nonzero norm-closed complex -subalgebras , , acting irreducibly. The source names denote .
Source irreducibility parameter`include hS in`Fixed source	The irreducibility of the action of is retained in this theorem, as well as that of .
Chosen bounded maps`theorem continuous_normalPartLinearMap_iff (U V : H ≃L[ℂ] K) :`Fixed source	The same bounded complex-linear isomorphisms , with bounded inverses, used to define .
Closures and the specified map`((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) (normalPartSemilinearMap S T hT U.toLinearEquiv V.toLinearEquiv) ↔`Fixed source	The relative closures on and on are the source and target of full continuity. Passing to the underlying linear maps does not change or the induced map . Thus the left side of (1) is $F(c_A(D))\subseteq c_B(F(D))\quad(D\subseteq N(A)).$
Full continuity`def Continuous (c : ClosureSpace α) (d : ClosureSpace β) (f : α → β) : Prop := ∀ s : Set α, f '' c.closure s ⊆ d.closure (f '' s)`Fixed source	For arbitrary closure spaces and a map, the image of the closure of every subset lies in the closure of its image. Applied here, the map is and the closures are precisely , not ambient closures on all geometric points.
Operator inclusion`∀ b : T, InnerProductSpace.adjointSandwich U.toContinuousLinearMap V.toContinuousLinearMap (b : K →L[ℂ] K) ∈ S :=`Fixed source	For every , the composite is an element of : $V^bU\in A\quad(b\in B).$ Equivalently, $V^BU\subseteq A.$ Together with the preceding equivalence sign, this is exactly (1).
Adjoint sandwich`def adjointSandwich (U V : H →L[𝕜] K) (b : K →L[𝕜] K) : H →L[𝕜] H := V.adjoint.comp (b.comp U)`Fixed source	The bounded operator . The arguments are the same as functions and the given operator ; their order is unchanged.

The include directive shown separately applies to this theorem alone. It accounts for the source irreducibility parameter in the retained type.

Exact surrounding source context (separate excerpts)

Exact ambient excerpt:

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

Exact ambient excerpt:

include hS in

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