The semilinear factors and their inverses are continuous

MathlibAnnex.Analysis.CStarAlgebra.normalPart_semilinear_factors_continuous

theorem

Establishes continuity of the fixed semilinear factors and their inverses.

Statement

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

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

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

For , give the normal part the relative geometric closure

c_A(\mathcal D)=\{J\in N(A):\bigcap_{I\in\mathcal D}I\subseteq J\}, \tag{1}

and similarly . Let be a specified finite-homeomorphism, that is, a bijection satisfying for every finite . Assume that is infinite-dimensional and that

e\bigl(c_A(\mathcal D)\bigr)\subseteq c_B\bigl(e(\mathcal D)\bigr) \qquad\text{for every }\mathcal D\subseteq N(A). \tag{2}

Let be the semilinear equivalences fixed in the algebraic realization of . Then all four functions

U:H\to K,\quad U^{-1}:K\to H,\quad V:H\to K,\quad V^{-1}:K\to H \tag{3}

are norm continuous. The inverses in (3) are those of the same maps .

Assumptions

The two nonzero concrete -algebras are norm closed and act irreducibly on their respective Hilbert spaces. They need not be unital. The inner product is conjugate-linear in its first variable. The closure on each normal part is the intersection closure displayed above.

For their scalar field automorphisms of , the semilinear maps satisfy and . They are the lifts fixed in the algebraic realization of the given , with one global direct or swapped orientation. The rank theorem supplies the bound required for this realization.

Full continuity is required only in the forward direction for . Neither full continuity of nor initial continuity of the two semilinear maps is assumed.

Conclusion

The two fixed semilinear equivalences are homeomorphisms for the norm topologies. The conclusion states continuity of in this order. It neither replaces the chosen factors nor asserts full continuity of .

Main citations

The four-continuity theorem concerns the factors fixed in the algebraic realization. The first lift and second lift specify the maps. The scalar-type theorem gives the separate scalar alternatives.

Lean source signature (exact)

The preceding variable declarations introduce the spaces, algebras, irreducibility hypotheses, the finite-homeomorphism e, and hdim. They occur in the conclusion through the selected factors. The earlier include hS hT e remains in scope, and include hH hcont additionally retains infinite-dimensionality and forward full continuity as theorem parameters. Thus the absence of an argument list on the next line does not make this an unconditional theorem. These declarations and commands are quoted separately below.

The following contiguous declaration prefix ends before its proof assignment.

theorem normalPart_semilinear_factors_continuous :
    Continuous (normalPartFirstSemilinearEquiv S T hS hT e hdim) ∧
    Continuous (normalPartFirstSemilinearEquiv S T hS hT e hdim).symm ∧
    Continuous (normalPartSecondSemilinearEquiv S T hS hT e hdim) ∧
    Continuous (normalPartSecondSemilinearEquiv S T hS hT e hdim).symm

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 and , called `S`,`T`. The inclusion representations in the last two lines express these irreducible actions.
Finite closure comparison`variable (e : ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))`Fixed source	The same bijection compares the relative closures. For every finite , $e(c_A(\mathcal D))=c_B(e(\mathcal D)).$ Its underlying equivalence is obtained by `toEquiv`; no new map is selected by that projection.
Included geometric inputs`include hS hT e`Fixed source	The two irreducibility hypotheses and are retained as parameters of the later theorem. They also occur as arguments of the selected scalar maps and semilinear maps.
Dimension and forward continuity`variable (hdim : 3 ≤ Module.rank ℂ H) variable (hH : ¬ FiniteDimensional ℂ H) variable (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv) include hH hcont`Fixed source	The bound specifies the selected lifts. Under the present hypotheses it is guaranteed by the rank theorem cited above. The additional hypotheses are infinite-dimensionality of and, for every , $e(c_A(\mathcal D))\subseteq c_B(e(\mathcal D)).$ The final `include` retains these hypotheses. Full continuity of is not assumed.
Inverse scalar structures`local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom := RingHomInvPair.of_ringEquiv σ local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom := RingHomInvPair.of_ringEquiv_symm σ`Fixed source	For a scalar automorphism , these instances pair with its inverse in both orders. They make the inverse of a -semilinear equivalence a -semilinear map; they do not impose .
First selected semilinear equivalence`def normalPartFirstSemilinearEquiv : LinearEquiv (normalPartFirstScalarEquiv S T hS hT e hdim).toRingHom (σ' := (normalPartFirstScalarEquiv S T hS hT e hdim).symm.toRingHom) H K := Classical.choose (Classical.choose_spec (exists_normalPart_first_semilinearEquiv S T hS hT e hdim))`Fixed source	This is the fixed additive bijection with . Its type specifies the inverse scalar map as , so `symm` below is the inverse .
Second selected semilinear equivalence`def normalPartSecondSemilinearEquiv : LinearEquiv (normalPartSecondScalarEquiv S T hS hT e hdim).toRingHom (σ' := (normalPartSecondScalarEquiv S T hS hT e hdim).symm.toRingHom) H K := Classical.choose (Classical.choose_spec (exists_normalPart_second_semilinearEquiv S T hS hT e hdim))`Fixed source	This is the fixed additive bijection with , from the same geometric inputs. Its inverse is , semilinear for .
Continuity of U`Continuous (normalPartFirstSemilinearEquiv S T hS hT e hdim) ∧`Fixed source	is continuous for the norm topologies, the first assertion in (3).
Continuity of the inverse of U`Continuous (normalPartFirstSemilinearEquiv S T hS hT e hdim).symm ∧`Fixed source	is norm continuous, the second assertion in (3). The suffix `symm` takes the inverse of the same selected .
Continuity of V`Continuous (normalPartSecondSemilinearEquiv S T hS hT e hdim) ∧`Fixed source	is norm continuous, the third assertion in (3).
Continuity of the inverse of V`Continuous (normalPartSecondSemilinearEquiv S T hS hT e hdim).symm :=`Fixed source	is norm continuous, the fourth assertion in (3). All four assertions are joined by conjunctions; this is not an assertion of full closure continuity of .

Exact surrounding source context (separate excerpts)

These separate excerpts record inverse scalar instances, the ambient spaces and algebras, and the included hypotheses. They are not spliced into the declaration prefix.

NormalPartSemilinearRegularity.lean — separate exact context:

local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom :=
  RingHomInvPair.of_ringEquiv σ
local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom :=
  RingHomInvPair.of_ringEquiv_symm σ

Back to the reading-guide item

NormalPartSemilinearRegularity.lean — separate exact context:

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

NormalPartSemilinearRegularity.lean — separate exact context:

include hS hT e

Back to the reading-guide item

NormalPartSemilinearRegularity.lean — separate exact context:

variable (hdim : 3 ≤ Module.rank ℂ H)
variable (hH : ¬ FiniteDimensional ℂ H)
variable (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous
  ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv)

include hH hcont

Back to the reading-guide item

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

Technical documentation