Faithful normal-part transport through a specified GSS homeomorphism

MathlibAnnex.Analysis.CStarAlgebra.exists_faithful_normalPart_transport

theorem

Transports the normal part through one faithful pure-GNS representation and the same preimage map.

Statement

Let be a complex Hilbert space, and let be a nonzero norm-closed complex -subalgebra acting irreducibly on . Let be a complex C*-algebra with its compatible order. Write for the geometric structure space of an algebra , with hull–kernel closure . For each maximal proper face of the closed unit ball of , take the union of the kernels of all bounded complex-linear functionals of norm one that equal on that face. The distinct subsets so obtained are the points of , by the geometric structure definition and the norm-one support characterization.

For a concrete algebra , define

f^D_{x,y}:D\to\mathbb C,\qquad f^D_{x,y}(a)=\langle y,a(x)\rangle, \qquad x,y\in L\setminus\{0\},

and

N(D)=\{I\in S(D):I=\ker f^D_{x,y}\text{ for some }x,y\in L\setminus\{0\}\}.

The inner product is linear in the second variable. Suppose that is a homeomorphism of closure spaces, so that

e(c_A(E))=c_B(e(E))\qquad(E\subseteq S(A)).

Then there are a pure state of and a homeomorphism

r:S(\pi_\varphi(B))\longrightarrow S(B),

where is the GNS representation of this same state, with the following properties:

is faithful.
For its range restriction ,

r(J)=\pi_{\varphi,r}^{-1}(J)\qquad(J\in S(\pi_\varphi(B))). \tag{1}

The inverse of that same homeomorphism satisfies

\pi_{\varphi,r}^{-1}(r^{-1}(I))=I\qquad(I\in S(B)). \tag{2}

The normal parts satisfy

(r^{-1}\circ e)(N(A))=N(\pi_\varphi(B)). \tag{3}

Assumptions

The Hilbert spaces are complete. A pure state is a positive bounded complex-linear functional of norm one that is extreme in the state space for real convexity. Closedness and irreducibility concern the given action of on . The homeomorphism is specified, with continuity for all subsets in both directions. Nonzero and follow from these hypotheses; no extra nontriviality assumption on is imposed.

Conclusion

One faithful pure-GNS representation and one inverse-image homeomorphism satisfy all three formulas. In (3), the same map is followed by . The conclusion identifies the normal parts under this composite; it does not identify a normal part with its entire geometric structure space.

Main citations

Faithful normal-part transport gives all the outputs for the same pure state and the same homeomorphism. The component-density criterion characterizes faithfulness of the pure-GNS representation. The forward preimage formula and inverse preimage formula concern the same range restriction; the normal-part image identity specifies which subset is transported.

Lean source signature (exact)

Exact source and declaration. Only the literal signature is displayed here; the linked source retains the proof.

theorem exists_faithful_normalPart_transport
    (S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (S : Set (H →L[ℂ] H))]
    (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))
    (e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ S)
      (NormedSpace.geometricStructureClosure ℂ B)) :
    ∃ phi : NonUnitalPureState B, Function.Injective phi.gnsRepresentation ∧
      ∃ r : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range phi.gnsRepresentation))
          (NormedSpace.geometricStructureClosure ℂ B),
        (∀ J, (r.toEquiv J).val = (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' J.val) ∧
        (∀ I, (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' (r.toEquiv.symm I).val = I.val) ∧
        (e.trans r.symm).toEquiv '' normalPart S = normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation)

Back to the reading-guide item

In the source, S denotes the algebra used here.

In the source	Mathematical meaning
Original Hilbert space`variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]`Fixed source	The original representation space is a complete complex Hilbert space. It is independent of the GNS space of the state found in the conclusion.
Target algebra`variable {B : Type w} [NonUnitalCStarAlgebra B] variable [PartialOrder B] [StarOrderedRing B]`Fixed source	The complex C*-algebra has its compatible order. No separate nontriviality assumption on appears here.
Concrete irreducible action`(S : NonUnitalStarSubalgebra ℂ (H →L[ℂ] H)) [IsClosed (S : Set (H →L[ℂ] H))] (hS : NonUnitalCStarRepresentation.IsIrreducible (NonUnitalStarSubalgebraClass.subtype S))`Fixed source	The source name is the closed complex -subalgebra . Its inclusion action is nonzero and irreducible.
Given homeomorphism`(e : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ S) (NormedSpace.geometricStructureClosure ℂ B)) :`Fixed source	The input is the specified closure-space homeomorphism . Its domain and codomain use the ambient geometric closures, not closures restricted to normal parts.
One faithful pure-state representation`∃ phi : NonUnitalPureState B, Function.Injective phi.gnsRepresentation ∧`Fixed source	There exists one pure state of whose GNS representation is injective, hence faithful. This same state and representation occur in every subsequent condition.
Homeomorphism from the representation image`∃ r : ClosureSpace.Homeomorph (NormedSpace.geometricStructureClosure ℂ (NonUnitalStarAlgHom.range phi.gnsRepresentation)) (NormedSpace.geometricStructureClosure ℂ B),`Fixed source	There exists one homeomorphism . The range is the actual image algebra of this same representation, not all bounded operators on its GNS space.
Forward preimage formula`(∀ J, (r.toEquiv J).val = (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' J.val) ∧`Fixed source	The underlying bijection of sends every geometric point of the image algebra to $r(J)=\pi_{\varphi,r}^{-1}(J).$ Here is the range restriction. The projections expose the underlying subsets.
Inverse preimage formula`(∀ I, (NonUnitalStarAlgHom.rangeRestrict phi.gnsRepresentation) ⁻¹' (r.toEquiv.symm I).val = I.val) ∧`Fixed source	The inverse of that same bijection satisfies $\pi_{\varphi,r}^{-1}(r^{-1}(I))=I\qquad(I\in S(B)).$ The inverse is not chosen independently.
Transport of normal parts`(e.trans r.symm).toEquiv '' normalPart S = normalPart (NonUnitalStarAlgHom.range phi.gnsRepresentation) := by`Fixed source	Transitivity composes first and second. Taking its underlying bijection and its set image gives $(r^{-1}\circ e)(N(A))=N(\pi_\varphi(B)).$ This identifies the normal parts, not the whole geometric structure spaces.
Same bijection in both continuity fields`structure Homeomorph (c : ClosureSpace α) (d : ClosureSpace β) extends α ≃ β where continuous_toFun : c.Continuous d toFun continuous_invFun : d.Continuous c invFun`Fixed source	For a homeomorphism , the underlying equivalence supplies and its inverse. The fields assert $q(c_X(E))\subseteq c_Y(q(E)),\qquad E\subseteq X,$ $q^{-1}(c_Y(F))\subseteq c_X(q^{-1}(F)),\qquad F\subseteq Y.$ This applies to both and with their displayed domains.

Exact surrounding source context (separate excerpts)

Exact surrounding source:

universe u v w
variable {A : Type u} [NonUnitalCStarAlgebra A] [Nontrivial A]
variable [PartialOrder A] [StarOrderedRing A]
variable {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H] [CompleteSpace H]

attribute [local instance] HomKernelQuotient.imageCStarAlgebra HomKernelQuotient.isClosed_image

Back to the reading-guide item

Exact surrounding source:

variable {B : Type w} [NonUnitalCStarAlgebra B]
variable [PartialOrder B] [StarOrderedRing B]

Back to the reading-guide item

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

Technical documentation