Classifying the specified normal-part equivalence with the selected bounded lifts

MathlibAnnex.Analysis.CStarAlgebra.exists_normalPart_selected_classification_eq

theorem

Classifies the given normal-part homeomorphism using its fixed factors and an operator image equality.

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} \tag{1}

The inner product is conjugate-linear in its first variable. For , the relative geometric closure is ; define analogously. Let be a finite-homeomorphism: a bijection satisfying for every finite . Assume is infinite-dimensional and, additionally, both and are fully continuous:

\begin{aligned} e(c_A(\mathcal D))&\subseteq c_B(e(\mathcal D)) &&(\mathcal D\subseteq N(A)),\\ e^{-1}(c_B(\mathcal E))&\subseteq c_A(e^{-1}(\mathcal E)) &&(\mathcal E\subseteq N(B)). \end{aligned} \tag{2}

Let and be the semilinear lifts and scalar automorphisms selected in the algebraic realization of this , using the dimension bound guaranteed by infinite-dimensionality. Thus and for and . Then . There exist either two continuous complex-linear equivalences , or two continuous conjugate-linear equivalences , such that

\begin{aligned} U_c(x)&=U(x),&V_c(x)&=V(x)&&(x\in H),\\ U_c^{-1}(z)&=U^{-1}(z),&V_c^{-1}(z)&=V^{-1}(z)&&(z\in K). \end{aligned} \tag{3}

For either common scalar type, one of the following global orientation branches holds. Write for the normal-part equivalence given by . Let be the closure-space homeomorphism induced by the involution, so that .

Direct branch. The specified equivalence is . For every and ,

\begin{aligned} e(\ker f^A_{x,y})&=\ker f^B_{U_cx,V_cy},\\ e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}z,V_c^{-1}w}. \end{aligned} \tag{4}

Swapped branch. The specified equivalence is . For every and ,

\begin{aligned} e(\ker f^A_{x,y})&=\ker f^B_{V_cy,U_cx},\\ e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}w,V_c^{-1}z}. \end{aligned} \tag{5}

The kernels on each side are subsets of the corresponding algebra. The forward and inverse formulas use the same branch and the same maps in (3). In either orientation, the common scalar type determines the operator-set equality

\begin{cases} V_c^*BU_c=A,&U_c,V_c\text{ complex-linear},\\ V_c^\dagger BU_c=A,&U_c,V_c\text{ conjugate-linear}. \end{cases} \tag{6}

Here , and similarly for . In the second case, the conjugate adjoint is characterized by for and . For each , the corresponding product or is a bounded complex-linear operator on .

Assumptions

The two nonzero concrete -algebras are norm closed and act irreducibly on their respective Hilbert spaces. Neither algebra is assumed unital. The source space is infinite dimensional.

Both full-continuity conditions (2) are required, in addition to finite continuity in both directions. Continuity of the semilinear factors, equality of their scalar types, and the four identities (3) are conclusions.

Conclusion

The given has one common scalar type and one global direct or swapped orientation. The same maps and their inverses satisfy all point and kernel formulas. Their underlying functions are precisely those fixed by the algebraic realization of .

In either scalar case the corresponding operator-set equality (6) holds. This is equality of concrete operator sets; it does not assert that , that either map is unitary, or that the transformation is a multiplicative -isomorphism.

Main citations

The selected classification theorem gives the common scalar type, the four function identities, both orientations, all coefficient-kernel formulas and the operator image equality. The algebraic realization fixes the underlying maps. The linear and conjugate-linear operator criteria specify the two transformations.

Lean source signature (exact)

The preceding variable declarations introduce , the algebras S, T, the irreducibility hypotheses and the finite-homeomorphism . Their occurrence in the arguments and conclusion makes them theorem parameters. The three arguments displayed below are infinite-dimensionality and the two directions of full continuity. In the conclusion type, the three let bindings name the rank bound and the selected maps ; they are not proof steps or a second choice of maps.

The following contiguous literal signature ends immediately before the final proof assignment. The full source retains the proof, and the surrounding declarations are quoted separately below.

theorem exists_normalPart_selected_classification_eq
    (hH : ¬ FiniteDimensional ℂ H)
    (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous
      ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv)
    (hcontInv : ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)).Continuous
      ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) e.toEquiv.symm) :
    let hd := (three_le_rank_of_normalPart_finiteHomeomorph S T hS hT e hH).1
    let U := normalPartFirstSemilinearEquiv S T hS hT e hd
    let V := normalPartSecondSemilinearEquiv S T hS hT e hd
    normalPartFirstScalarEquiv S T hS hT e hd =
      normalPartSecondScalarEquiv S T hS hT e hd ∧
    (
    (∃ Uc Vc : H ≃L[ℂ] K,
      (∀ x, Uc x = U x) ∧ (∀ x, Vc x = V x) ∧
      (∀ z, Uc.symm z = U.symm z) ∧ (∀ z, Vc.symm z = V.symm z) ∧
      (((e.toEquiv = normalPartSemilinearEquiv S T hS hT (fun _ => rfl)
            Uc.toLinearEquiv Vc.toLinearEquiv) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          e.toEquiv (normalPartPoint S hS x y hx hy) =
            normalPartPoint T hT (Uc x) (Vc y)
              (by simpa only [map_zero] using Uc.injective.ne hx)
              (by simpa only [map_zero] using Vc.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 (Uc.symm z) (Vc.symm w)
              (by simpa only [map_zero] using Uc.symm.injective.ne hz)
              (by simpa only [map_zero] using Vc.symm.injective.ne hw)) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val =
            {b : T | inner ℂ (Vc y) ((b : K →L[ℂ] K) (Uc x)) = 0}) ∧
        (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
          (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val =
            {a : S | inner ℂ (Vc.symm w) ((a : H →L[ℂ] H) (Uc.symm z)) = 0})) ∨
       ((e.toEquiv = (normalPartSemilinearEquiv S T hS hT (fun _ => rfl)
            Uc.toLinearEquiv Vc.toLinearEquiv).trans (normalPartStarHomeomorph T hT).toEquiv) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          e.toEquiv (normalPartPoint S hS x y hx hy) =
            normalPartPoint T hT (Vc y) (Uc x)
              (by simpa only [map_zero] using Vc.injective.ne hy)
              (by simpa only [map_zero] using Uc.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 (Uc.symm w) (Vc.symm z)
              (by simpa only [map_zero] using Uc.symm.injective.ne hw)
              (by simpa only [map_zero] using Vc.symm.injective.ne hz)) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val =
            {b : T | inner ℂ (Uc x) ((b : K →L[ℂ] K) (Vc y)) = 0}) ∧
        (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
          (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val =
            {a : S | inner ℂ (Vc.symm z) ((a : H →L[ℂ] H) (Uc.symm w)) = 0}))) ∧
      InnerProductSpace.adjointSandwich Uc.toContinuousLinearMap Vc.toContinuousLinearMap ''
        (T : Set (K →L[ℂ] K)) = (S : Set (H →L[ℂ] H))) ∨
    (∃ Uc Vc : H ≃SL[starRingEnd ℂ] K,
      (∀ x, Uc x = U x) ∧ (∀ x, Vc x = V x) ∧
      (∀ z, Uc.symm z = U.symm z) ∧ (∀ z, Vc.symm z = V.symm z) ∧
      (((e.toEquiv = normalPartSemilinearEquiv S T hS hT (fun _ => rfl)
            Uc.toLinearEquiv Vc.toLinearEquiv) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          e.toEquiv (normalPartPoint S hS x y hx hy) =
            normalPartPoint T hT (Uc x) (Vc y)
              (by simpa only [map_zero] using Uc.injective.ne hx)
              (by simpa only [map_zero] using Vc.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 (Uc.symm z) (Vc.symm w)
              (by simpa only [map_zero] using Uc.symm.injective.ne hz)
              (by simpa only [map_zero] using Vc.symm.injective.ne hw)) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val =
            {b : T | inner ℂ (Vc y) ((b : K →L[ℂ] K) (Uc x)) = 0}) ∧
        (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
          (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val =
            {a : S | inner ℂ (Vc.symm w) ((a : H →L[ℂ] H) (Uc.symm z)) = 0})) ∨
       ((e.toEquiv = (normalPartSemilinearEquiv S T hS hT (fun _ => rfl)
            Uc.toLinearEquiv Vc.toLinearEquiv).trans (normalPartStarHomeomorph T hT).toEquiv) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          e.toEquiv (normalPartPoint S hS x y hx hy) =
            normalPartPoint T hT (Vc y) (Uc x)
              (by simpa only [map_zero] using Vc.injective.ne hy)
              (by simpa only [map_zero] using Uc.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 (Uc.symm w) (Vc.symm z)
              (by simpa only [map_zero] using Uc.symm.injective.ne hw)
              (by simpa only [map_zero] using Vc.symm.injective.ne hz)) ∧
        (∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0),
          (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val =
            {b : T | inner ℂ (Uc x) ((b : K →L[ℂ] K) (Vc y)) = 0}) ∧
        (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0),
          (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val =
            {a : S | inner ℂ (Vc.symm z) ((a : H →L[ℂ] H) (Uc.symm w)) = 0}))) ∧
      InnerProductSpace.conjugateAdjointSandwich Uc.toContinuousLinearMap Vc.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
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 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 same bijection and its actual inverse, with finite continuity for the relative closures in both directions.
Full continuity hypotheses`(hH : ¬ FiniteDimensional ℂ H) (hcont : ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)).Continuous ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)) e.toEquiv) (hcontInv : ((NormedSpace.geometricStructureClosure ℂ T).subspace (normalPart T)).Continuous ((NormedSpace.geometricStructureClosure ℂ S).subspace (normalPart S)) e.toEquiv.symm) :`Fixed source	The infinite-dimensionality of , and both full-continuity inclusions in (2), for arbitrary subsets and . The functions supplied are the given and its inverse.
Derived rank and selected maps`let hd := (three_le_rank_of_normalPart_finiteHomeomorph S T hS hT e hH).1 let U := normalPartFirstSemilinearEquiv S T hS hT e hd let V := normalPartSecondSemilinearEquiv S T hS hT e hd`Fixed source	The rank theorem supplies under the stated hypotheses. It is not an additional assumption. The same and this bound select the same used in the Statement.
Common scalar type`normalPartFirstScalarEquiv S T hS hT e hd = normalPartSecondScalarEquiv S T hS hT e hd ∧`Fixed source	The two scalar automorphisms of the selected lifts agree: $\sigma_1=\sigma_2.$ The alternatives that follow classify their common type; they do not allow a mixed linear/conjugate-linear pair.
Complex-linear realization`(∃ Uc Vc : H ≃L[ℂ] K, (∀ x, Uc x = U x) ∧ (∀ x, Vc x = V x) ∧ (∀ z, Uc.symm z = U.symm z) ∧ (∀ z, Vc.symm z = V.symm z) ∧`Fixed source	Continuous complex-linear isomorphisms have the same functions and the same inverses as the selected lifts: $\begin{aligned}U_c(x)&=U(x),&V_c(x)&=V(x)\quad(x\in H),\\U_c^{-1}(z)&=U^{-1}(z),&V_c^{-1}(z)&=V^{-1}(z)\quad(z\in K).\end{aligned}$
Complex-linear direct map`(((e.toEquiv = normalPartSemilinearEquiv S T hS hT (fun _ => rfl) Uc.toLinearEquiv Vc.toLinearEquiv) ∧`Fixed source	The direct branch identifies the given map with the transport by these same : $e=F_{U_c,V_c}.$ Taking underlying linear or semilinear maps changes no function.
Complex-linear direct forward point`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (Uc x) (Vc y) (by simpa only [map_zero] using Uc.injective.ne hx) (by simpa only [map_zero] using Vc.injective.ne hy)) ∧`Fixed source	For every , the first equation of (4): $e(\ker f^A_{x,y})=\ker f^B_{U_cx,V_cy}.$
Complex-linear direct inverse point`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (Uc.symm z) (Vc.symm w) (by simpa only [map_zero] using Uc.symm.injective.ne hz) (by simpa only [map_zero] using Vc.symm.injective.ne hw)) ∧`Fixed source	For every , the second equation of (4): $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}z,V_c^{-1}w}.\end{aligned}$
Complex-linear direct underlying sets`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val = {b : T \| inner ℂ (Vc y) ((b : K →L[ℂ] K) (Uc x)) = 0}) ∧ (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val = {a : S \| inner ℂ (Vc.symm w) ((a : H →L[ℂ] H) (Uc.symm z)) = 0})) ∨`Fixed source	The same two equalities are also equalities of subsets of and , respectively, with the same nonzero-vector quantifiers: $\begin{aligned}e(\ker f^A_{x,y})&=\ker f^B_{U_cx,V_cy},\\e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}z,V_c^{-1}w}.\end{aligned}$ The projections expose the underlying kernel sets, not different points.
Complex-linear swapped map`((e.toEquiv = (normalPartSemilinearEquiv S T hS hT (fun _ => rfl) Uc.toLinearEquiv Vc.toLinearEquiv).trans (normalPartStarHomeomorph T hT).toEquiv) ∧`Fixed source	The other orientation composes with the target star map: $e=s_B\circ F_{U_c,V_c}.$ Here . The disjunction selects one orientation for all vectors.
Complex-linear swapped forward point`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (Vc y) (Uc x) (by simpa only [map_zero] using Vc.injective.ne hy) (by simpa only [map_zero] using Uc.injective.ne hx)) ∧`Fixed source	For every , the first equation of (5): $e(\ker f^A_{x,y})=\ker f^B_{V_cy,U_cx}.$
Complex-linear swapped inverse point`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (Uc.symm w) (Vc.symm z) (by simpa only [map_zero] using Uc.symm.injective.ne hw) (by simpa only [map_zero] using Vc.symm.injective.ne hz)) ∧`Fixed source	For every , the second equation of (5): $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}w,V_c^{-1}z}.\end{aligned}$
Complex-linear swapped underlying sets`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val = {b : T \| inner ℂ (Uc x) ((b : K →L[ℂ] K) (Vc y)) = 0}) ∧ (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val = {a : S \| inner ℂ (Vc.symm z) ((a : H →L[ℂ] H) (Uc.symm w)) = 0}))) ∧`Fixed source	The underlying subsets satisfy the same two equations in (5), for all the same nonzero pairs: $\begin{aligned}e(\ker f^A_{x,y})&=\ker f^B_{V_cy,U_cx},\\e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}w,V_c^{-1}z}.\end{aligned}$ The orientation and actual inverse are unchanged.
Complex-linear operator image`InnerProductSpace.adjointSandwich Uc.toContinuousLinearMap Vc.toContinuousLinearMap '' (T : Set (K →L[ℂ] K)) = (S : Set (H →L[ℂ] H))) ∨`Fixed source	In either orientation of the complex-linear case, $\begin{aligned}V_c^BU_c&=\{V_c^bU_c:b\in B\}\\&=A\subseteq\mathcal B(H).\end{aligned}$ This is equality, not just inclusion, and uses the bounded Hilbert-space adjoint.
Conjugate-linear realization`(∃ Uc Vc : H ≃SL[starRingEnd ℂ] K, (∀ x, Uc x = U x) ∧ (∀ x, Vc x = V x) ∧ (∀ z, Uc.symm z = U.symm z) ∧ (∀ z, Vc.symm z = V.symm z) ∧`Fixed source	Continuous conjugate-linear isomorphisms instead realize the selected lifts, again with the same inverse functions: $\begin{aligned}U_c(x)&=U(x),&V_c(x)&=V(x)\quad(x\in H),\\U_c^{-1}(z)&=U^{-1}(z),&V_c^{-1}(z)&=V^{-1}(z)\quad(z\in K).\end{aligned}$ This is the other scalar-type alternative, not a second choice within the complex-linear case.
Conjugate-linear direct map`(((e.toEquiv = normalPartSemilinearEquiv S T hS hT (fun _ => rfl) Uc.toLinearEquiv Vc.toLinearEquiv) ∧`Fixed source	The direct branch identifies the given map with the transport by these same : $e=F_{U_c,V_c}.$ Taking underlying linear or semilinear maps changes no function.
Conjugate-linear direct forward point`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (Uc x) (Vc y) (by simpa only [map_zero] using Uc.injective.ne hx) (by simpa only [map_zero] using Vc.injective.ne hy)) ∧`Fixed source	For every , the first equation of (4): $e(\ker f^A_{x,y})=\ker f^B_{U_cx,V_cy}.$
Conjugate-linear direct inverse point`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (Uc.symm z) (Vc.symm w) (by simpa only [map_zero] using Uc.symm.injective.ne hz) (by simpa only [map_zero] using Vc.symm.injective.ne hw)) ∧`Fixed source	For every , the second equation of (4): $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}z,V_c^{-1}w}.\end{aligned}$
Conjugate-linear direct underlying sets`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val = {b : T \| inner ℂ (Vc y) ((b : K →L[ℂ] K) (Uc x)) = 0}) ∧ (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val = {a : S \| inner ℂ (Vc.symm w) ((a : H →L[ℂ] H) (Uc.symm z)) = 0})) ∨`Fixed source	The same two equalities are also equalities of subsets of and , respectively, with the same nonzero-vector quantifiers: $\begin{aligned}e(\ker f^A_{x,y})&=\ker f^B_{U_cx,V_cy},\\e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}z,V_c^{-1}w}.\end{aligned}$ The projections expose the underlying kernel sets, not different points.
Conjugate-linear swapped map`((e.toEquiv = (normalPartSemilinearEquiv S T hS hT (fun _ => rfl) Uc.toLinearEquiv Vc.toLinearEquiv).trans (normalPartStarHomeomorph T hT).toEquiv) ∧`Fixed source	The other orientation composes with the target star map: $e=s_B\circ F_{U_c,V_c}.$ Here . The disjunction selects one orientation for all vectors.
Conjugate-linear swapped forward point`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), e.toEquiv (normalPartPoint S hS x y hx hy) = normalPartPoint T hT (Vc y) (Uc x) (by simpa only [map_zero] using Vc.injective.ne hy) (by simpa only [map_zero] using Uc.injective.ne hx)) ∧`Fixed source	For every , the first equation of (5): $e(\ker f^A_{x,y})=\ker f^B_{V_cy,U_cx}.$
Conjugate-linear swapped inverse point`(∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), e.toEquiv.symm (normalPartPoint T hT z w hz hw) = normalPartPoint S hS (Uc.symm w) (Vc.symm z) (by simpa only [map_zero] using Uc.symm.injective.ne hw) (by simpa only [map_zero] using Vc.symm.injective.ne hz)) ∧`Fixed source	For every , the second equation of (5): $\begin{aligned}e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}w,V_c^{-1}z}.\end{aligned}$
Conjugate-linear swapped underlying sets`(∀ (x y : H) (hx : x ≠ 0) (hy : y ≠ 0), (e.toEquiv (normalPartPoint S hS x y hx hy)).val.val = {b : T \| inner ℂ (Uc x) ((b : K →L[ℂ] K) (Vc y)) = 0}) ∧ (∀ (z w : K) (hz : z ≠ 0) (hw : w ≠ 0), (e.toEquiv.symm (normalPartPoint T hT z w hz hw)).val.val = {a : S \| inner ℂ (Vc.symm z) ((a : H →L[ℂ] H) (Uc.symm w)) = 0}))) ∧`Fixed source	The underlying subsets satisfy the same two equations in (5), for all the same nonzero pairs: $\begin{aligned}e(\ker f^A_{x,y})&=\ker f^B_{V_cy,U_cx},\\e^{-1}(\ker f^B_{z,w})&=\ker f^A_{U_c^{-1}w,V_c^{-1}z}.\end{aligned}$ The orientation and actual inverse are unchanged.
Conjugate-linear operator image`InnerProductSpace.conjugateAdjointSandwich Uc.toContinuousLinearMap Vc.toContinuousLinearMap '' (T : Set (K →L[ℂ] K)) = (S : Set (H →L[ℂ] H)))) := by`Fixed source	In either orientation of the conjugate-linear case, $\begin{aligned}V_c^\dagger BU_c&=\{V_c^\dagger bU_c:b\in B\}\\&=A\subseteq\mathcal B(H).\end{aligned}$ The dagger denotes the conjugate adjoint. Each displayed composite is a bounded complex-linear operator.
Adjoint composite`def adjointSandwich (U V : H →L[𝕜] K) (b : K →L[𝕜] K) : H →L[𝕜] H := V.adjoint.comp (b.comp U)`Fixed source	The composite in the complex-linear case.
Conjugate-adjoint composite`def conjugateAdjointSandwich (U V : H →L⋆[𝕜] K) (b : K →L[𝕜] K) : H →L[𝕜] H := (conjugateAdjoint V).comp (b.comp U)`Fixed source	The composite in the conjugate-linear case, with the same order of factors.

Exact surrounding source context (separate excerpts)

The following are separate exact ambient excerpts, not lines spliced into the signature. The local inverse-pair instances express genuine inverse scalar maps, not an assumption that every field automorphism is involutive.

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

The ambient declarations are active here. The local scalar variables of the earlier Evaluation and SameFunctions sections have gone out of scope before the selected theorem; they are not additional inputs.

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

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

Technical documentation