Semilinear vector changes preserve finite normal-part closures

MathlibAnnex.Analysis.CStarAlgebra.normalPartSemilinearFiniteHomeomorph

def

Defines a finite homeomorphism of normal parts from two semilinear vector isomorphisms.

Statement

Let and be norm-closed complex -subalgebras with nonzero irreducible inclusion representations on complete complex Hilbert spaces. Neither algebra needs an identity. Use inner products linear in their second variable. For nonzero vectors, write

f^{A_1}_{x,y}(a)=\langle y,a(x)\rangle\quad(a\in A_1),\qquad f^{A_2}_{z,w}(b)=\langle w,b(z)\rangle\quad(b\in A_2).

Let be the coefficient-kernel normal part, with inherited closure

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

Suppose is a unital ring homomorphism with and for every , and are algebraic -semilinear isomorphisms. The definition equips

F:N(A_1)\longrightarrow N(A_2),\qquad F(\ker f^{A_1}_{x,y})=\ker f^{A_2}_{Ux,Vy} \tag{1}

with finite continuity in both directions. Thus is a finite-homeomorphism: a bijection whose map and inverse preserve membership in closures of finite sets.

Definition

The underlying equivalence sends the coefficient kernel represented by to the kernel represented by . Its inverse is

F^{-1}:N(A_2)\longrightarrow N(A_1),\qquad F^{-1}(\ker f^{A_2}_{z,w})=\ker f^{A_1}_{U^{-1}z,V^{-1}w}. \tag{2}

The semilinear kernel bijection has the forward evaluation for every nonzero representing pair. Its inverse uses the inverses of those same .

The other two fields are the finite-continuity requirements

\begin{aligned} F(c_{A_1}(D))&\subseteq c_{A_2}(F(D)) &&(D\subseteq N(A_1)\text{ finite}),\\ F^{-1}(c_{A_2}(E))&\subseteq c_{A_1}(F^{-1}(E)) &&(E\subseteq N(A_2)\text{ finite}). \end{aligned} \tag{3}

The finite-continuity theorem guarantees these inclusions for and their inverses, respectively. Both inverse maps use the same self-inverse scalar homomorphism .

Assumptions

The same scalar homomorphism governs both vector maps. Its inverse is itself, and it commutes with complex conjugation. are additive bijections with and . They are not assumed bounded, isometric, unitary, or algebra intertwiners. Closedness and irreducibility belong to the two concrete algebras; they guarantee the coefficient-kernel realization and the finite-continuity theorem.

Conclusion

The output is a bijection of the normal parts with finite continuity of the forward map and its inverse, for all finite subsets including the empty set. Full continuity for arbitrary subsets is not a field of this construction.

Main citations

Exact finite-homeomorphism construction: normalPartSemilinearFiniteHomeomorph and its three defining fields.
arXiv:2504.05551v1, Theorem 6.9: the algebraic finite-homeomorphism layer, separated from its bounded full-continuity layer.
normalPartSemilinearMap_point: representative-independent evaluation.
normalPartSemilinearEquiv: the specified bijection.
finitelyContinuous_normalPartSemilinearMap: finite continuity.

Lean source signature (exact)

The complete definition below is copied from the pinned source, including its defining right-hand side.

def normalPartSemilinearFiniteHomeomorph
    (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))
    (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T))
    (hσ : ∀ c : ℂ, σ (star c) = star (σ c)) (U V : H ≃ₛₗ[σ] K) :
    ClosureSpace.FiniteHomeomorph
      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S))
      ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) where
  toEquiv := normalPartSemilinearEquiv S T hS hT hσ U V
  finitelyContinuous_toFun := finitelyContinuous_normalPartSemilinearMap S T hS hT hσ U V
  finitelyContinuous_invFun :=
    finitelyContinuous_normalPartSemilinearMap T S hT hS hσ U.symm V.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
First algebra and Hilbert space`variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H] variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) variable [IsClosed (S : Set (H →L[ℂ] H))]`Fixed source	The complex Hilbert space and the norm-closed complex -subalgebra . The source calls this algebra `S`.
Second algebra and scalar map`variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K] variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K)) variable [IsClosed (T : Set (K →L[ℂ] K))] variable {σ : ℂ →+* ℂ} [RingHomInvPair σ σ]`Fixed source	The complex Hilbert space and the norm-closed algebra , called `T`. The unital scalar homomorphism satisfies ; the inverse vector maps therefore use the same scalar map.
Irreducible actions and semilinear maps`(hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T)) (hσ : ∀ c : ℂ, σ (star c) = star (σ c)) (U V : H ≃ₛₗ[σ] K) :`Fixed source	The two algebras act nontrivially and irreducibly on their respective spaces. The maps are additive bijections satisfying and . The scalar condition is for every . No boundedness is assumed.
Domain and target closures`ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) where`Fixed source	The output is a finite homeomorphism . Each `subspace` restricts the geometric closure to the indicated normal part; these are the relative closures used in (3).
Underlying bijection`toEquiv := normalPartSemilinearEquiv S T hS hT hσ U V`Fixed source	This field uses the bijection induced by the same : $F(\ker f^{A_1}_{x,y})=\ker f^{A_2}_{Ux,Vy}.$ Here . Its inverse is the map in (2).
Forward and inverse maps`def normalPartSemilinearEquiv (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) (hT : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype T)) (hσ : ∀ c : ℂ, σ (star c) = star (σ c)) (U V : H ≃ₛₗ[σ] K) : normalPart S ≃ normalPart T where toFun := normalPartSemilinearMap S T hT U V invFun := normalPartSemilinearMap T S hS U.symm V.symm`Fixed source	The equivalence has forward map and inverse . The inverse uses , so for , $F^{-1}(\ker f^{A_2}_{z,w})=\ker f^{A_1}_{U^{-1}z,V^{-1}w}.$ This excerpt specifies the two maps; the inverse-law proof fields remain in the full source.
Finite forward continuity`finitelyContinuous_toFun := finitelyContinuous_normalPartSemilinearMap S T hS hT hσ U V`Fixed source	The cited result supplies, for every finite , $F(c_{A_1}(D))\subseteq c_{A_2}(F(D)).$ It applies to the same and scalar condition.
Finite inverse continuity`finitelyContinuous_invFun := finitelyContinuous_normalPartSemilinearMap T S hT hS hσ U.symm V.symm`Fixed source	The algebras and irreducibility hypotheses are exchanged, and `symm` takes the actual inverses of . For every finite , $F^{-1}(c_{A_2}(E))\subseteq c_{A_1}(F^{-1}(E)).$ Neither field asserts continuity on arbitrary subsets.

The declaration retains the full three-field right-hand side. The self-inverse scalar condition is in the separately displayed ambient context.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

variable {H : Type u} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]
variable (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H))
variable [IsClosed (S : Set (H →L[ℂ] H))]

Back to the reading-guide item

Exact surrounding source:

variable {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K] [CompleteSpace K]
variable (T : NonUnitalStarSubalgebra ℂ (K →L[ℂ] K))
variable [IsClosed (T : Set (K →L[ℂ] K))]
variable {σ : ℂ →+* ℂ} [RingHomInvPair σ σ]

Back to the reading-guide item

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

Technical documentation