Semilinear factors recover all coefficient kernels

MathlibAnnex.Analysis.CStarAlgebra.normalPart_semilinear_factors_evaluation

theorem

Evaluates a normal-part finite-homeomorphism and its inverse using the same semilinear factors.

Statement

Let be complex Hilbert spaces. Let and be nonzero norm-closed complex -subalgebras acting irreducibly on and , respectively. Units are not required. 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

N(A)=\{\ker f^A_{x,y}:x,y\in H\setminus\{0\}\},\qquad N(B)=\{\ker f^B_{z,w}:z,w\in K\setminus\{0\}\}.

For , let , and define similarly. Let be a finite-homeomorphism: it is a bijection and for every finite . Suppose

3\le\operatorname{rank}_{\mathbb C}H,\tag{1}

where rank is cardinal-valued algebraic dimension.

Let be the projective factors associated with by the projective factorization. Here is the space of one-dimensional complex subspaces of . The semilinear realization theorem provides lifts of both factors. Use the lifts fixed by the first and second definitions:

\begin{aligned} \sigma_1,\sigma_2 &: \mathbb C\longrightarrow\mathbb C &&\text{field automorphisms},\\ U &:H\longrightarrow K &&\text{a }\sigma_1\text{-semilinear equivalence},\\ V &:H\longrightarrow K &&\text{a }\sigma_2\text{-semilinear equivalence}. \end{aligned}\tag{2}

Thus and for every nonzero representative. The same maps are used for all points. For these fixed , one of the following two alternatives holds globally:

\begin{aligned} e(\ker f^A_{x,y})&=\ker f^B_{Ux,Vy} &&(x,y\ne0),\\ e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U^{-1}z,V^{-1}w} &&(z,w\ne0); \end{aligned}\tag{3}

\begin{aligned} e(\ker f^A_{x,y})&=\ker f^B_{Vy,Ux} &&(x,y\ne0),\\ e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U^{-1}w,V^{-1}z} &&(z,w\ne0). \end{aligned}\tag{4}

Each alternative includes both of its universally quantified equations. Here is the inverse of the given bijection.

Assumptions

The normal-part bijection and its inverse satisfy finite continuity. The spaces are complex Hilbert spaces, and the two norm-closed -subalgebras act nontrivially and irreducibly. The algebraic dimension of is at least three; it may be infinite.

The two projective factors come from the same factorization of . Their semilinear lifts may have different scalar automorphisms. Neither those automorphisms nor the lifts are assumed continuous or bounded.

Conclusion

One of the alternatives (3) and (4) holds for every nonzero pair of vectors, in both directions. These are equalities of points of the normal parts and hence of their coefficient kernels. The orientation is fixed globally, and the formulas use the same and their inverses throughout. Continuity on arbitrary subsets and boundedness of the lifts are not conclusions of this theorem.

Main citations

The projective factorization and its evaluation formulas specify the two factors of the given map. The semilinear realization theorem gives lifts on every projective line. The evaluation theorem states (3) or (4) for the lifts fixed by the definitions of the first lift and second lift. The retained paper's Theorem 6.18 gives the broader context.

Lean source signature (exact)

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

Here is a parameter declared earlier by variable, not a map constructed by this theorem. Lean adds the section parameters used in the statement as theorem parameters. The first two let expressions name the semilinear maps chosen from this same ; e.toEquiv is the given bijection , and e.toEquiv.symm is . The four equations are identified individually in the table below.

theorem normalPart_semilinear_factors_evaluation :
    let U := normalPartFirstSemilinearEquiv S T hS hT e hdim
    let V := normalPartSecondSemilinearEquiv S T hS hT e hdim
    ((∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
      e.toEquiv (normalPartPoint S hS x y hx hy) =
        normalPartPoint T hT (U x) (V y)
          (by simpa only [map_zero] using U.injective.ne hx)
          (by simpa only [map_zero] using V.injective.ne hy)) ∧
     (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
      e.toEquiv.symm (normalPartPoint T hT z w hz hw) =
        normalPartPoint S hS (U.symm z) (V.symm w)
          (by simpa only [map_zero] using U.symm.injective.ne hz)
          (by simpa only [map_zero] using V.symm.injective.ne hw))) ∨
    ((∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
      e.toEquiv (normalPartPoint S hS x y hx hy) =
        normalPartPoint T hT (V y) (U x)
          (by simpa only [map_zero] using V.injective.ne hy)
          (by simpa only [map_zero] using U.injective.ne hx)) ∧
     (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
      e.toEquiv.symm (normalPartPoint T hT z w hz hw) =
        normalPartPoint S hS (U.symm w) (V.symm z)
          (by simpa only [map_zero] using U.symm.injective.ne hw)
          (by simpa only [map_zero] using V.symm.injective.ne hz)))

Back to the reading-guide item

In the four equation rows below, and are arbitrary.

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 irreducible complex -subalgebras , denoted in the source.
Given finite homeomorphism`variable (e : ClosureSpace.FiniteHomeomorph ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)))`Fixed source	The given bijection and its actual inverse, with finite continuity for the relative closures in both directions.
Finite homeomorphism`structure FiniteHomeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where finitelyContinuous_toFun : c.FinitelyContinuous d toFun finitelyContinuous_invFun : d.FinitelyContinuous c invFun`Fixed source	One equivalence together with finite continuity of its forward map and its inverse. Here its underlying equivalence is , and its inverse is ; these are not newly chosen maps.
Dimension input`variable (hdim : 3 ≤ Module.rank ℂ H)`Fixed source	The bound in (1), allowing infinite dimension.
The selected lifts`let U := normalPartFirstSemilinearEquiv S T hS hT e hdim let V := normalPartSecondSemilinearEquiv S T hS hT e hdim`Fixed source	The maps in (2) are chosen from this same , the two algebras, their irreducibility, and the dimension bound. Their scalar automorphisms are ; no equality of these automorphisms is asserted.
Coefficient-kernel point`def normalPartPoint (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S)) (x y : H) (hx : x ≠ 0) (hy : y ≠ 0) : normalPart S := ⟨restrictedMatrixCoefficientKernel S hS x y hx hy, ⟨x, y, hx, hy, rfl⟩⟩`Fixed source	The point for ; using gives . The displayed nonzero conditions ensure that these are normal-part points.
Direct forward equation`((∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (U x) (V y) (by simpa only [map_zero] using U.injective.ne hx) (by simpa only [map_zero] using V.injective.ne hy)) ∧`Fixed source	For every , the first equation of (3): $e(\ker f^A_{x,y})=\ker f^B_{Ux,Vy}.$
Direct inverse equation`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (U.symm z) (V.symm w) (by simpa only [map_zero] using U.symm.injective.ne hz) (by simpa only [map_zero] using V.symm.injective.ne hw))) ∨`Fixed source	For every , the second equation of (3), for the inverse of the same : $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U^{-1}z,V^{-1}w}.\end{aligned}$ The disjunction following this pair separates the two global orientations.
Swapped forward equation`((∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (V y) (U x) (by simpa only [map_zero] using V.injective.ne hy) (by simpa only [map_zero] using U.injective.ne hx)) ∧`Fixed source	For every , the first equation of (4): $e(\ker f^A_{x,y})=\ker f^B_{Vy,Ux}.$
Swapped inverse equation`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (U.symm w) (V.symm z) (by simpa only [map_zero] using U.symm.injective.ne hw) (by simpa only [map_zero] using V.symm.injective.ne hz))) := by`Fixed source	For every , the second equation of (4): $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U^{-1}w,V^{-1}z}.\end{aligned}$ Each branch joins its two universally quantified equations; one orientation holds for the entire map.
Inverse scalar maps`local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.toRingHom σ.symm.toRingHom := RingHomInvPair.of_ringEquiv σ local instance (σ : ℂ ≃+* ℂ) : RingHomInvPair σ.symm.toRingHom σ.toRingHom := RingHomInvPair.of_ringEquiv_symm σ`Fixed source	The scalar maps and their actual inverses compose to the identity in either order. This does not assert or .

The short proof terms attached to transported vectors only certify that those vectors are nonzero, so that their coefficient kernels define the displayed normal-part points.

The declaration prefix includes both internal let assignments and all four universally quantified equations. It ends before the proof assignment. The surrounding context below is quoted separately.

Exact surrounding source context (separate excerpts)

Exact ambient excerpt:

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

Exact ambient excerpt:

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)))
variable (hdim : 3 ≤ Module.rank ℂ H)

Back to the reading-guide item

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

Technical documentation