Pointed unitary transport between trace-cyclic target representations

MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic

theorem

Source cyclicity and strong shell sums extend the canonical CAR orbit isometry to the whole target.

Statement

Let be the completed CAR algebra, the completion of the matrix system , and let be its normalized trace. Fix a representative shell family: for each chosen pure-GNS class it specifies an automorphism and partial isometries between the transported and root shells. Fix the links chosen by this family in the selected atomic representation . Throughout this Card,

Thus is the already constructed concrete unital C*-algebra, and is its injective source map. The links and target are kept fixed. A state means a positive continuous complex linear functional taking to . Let and be unital star representations on complex Hilbert spaces. Suppose and have dense target orbits and realize the same source trace:

There exists a unitary with and for every .

Assumptions

Both Hilbert spaces are complete. The source trace identities and density of the two target orbits are the hypotheses. The vectors automatically have norm by taking . No irreducibility of either representation and no norm separability of is required.

Conclusion

The resulting unitary is pointed and intertwines the entire fixed target. Source intertwining is obtained first; intertwining the added generators is a separate strong-limit step.

Proof route

Trace estimates kill the residual flag projections on the source-cyclic subspace. Reduction and target cyclicity make this subspace the entire Hilbert space. Pointed CAR transport can then be passed through the shell limits and extended by norm generation.

Proof steps

Write for the decreasing root projections, , and for the automorphism selected for class . The shell operators satisfy and . The normalized source trace has . Traciality on these supports gives

Together with , this yields , as recorded by the transported-flag trace theorem.
Put . For every fixed , apply the projection-orbit estimate separately to the root projection and the transported projection :

Both right-hand sides tend to zero as . These estimates use the tracial source vector state ; no traciality of a state on is used.
Actual-target shell reconstruction provides strong limits of the represented shell and adjoint-shell sums, intersection projections for the transported and root flags, and a residual operator , with

where . For every , the intersection projection satisfies . Hence, for every fixed ,

The left-hand side is independent of , so . Using and the root-projection estimate gives as well. Continuity extends both equalities to , so . Therefore ; taking adjoints of the support relation gives and .
The closed subspace reduces the source action. Both the shell sums and their adjoints preserve it, so their strong limits preserve it as well. The preceding residual equalities show and . Hence reduces all generators, and therefore the norm-closed algebra they generate. It contains and thus the entire target orbit. Target cyclicity forces . The same argument gives . These are the conclusions of reduces_cyclicSubspace_of_trace and denseRange_source_orbit_of_trace_of_cyclic.
For , equality of source vector states gives the Gram identity

The pointed cyclic transport theorem applies to the two now-dense source orbits. The orbit isometry extends onto and yields a unitary such that and for every .
Set . Since the source-cyclic spaces are the whole spaces, reconstruction gives, in each representation,

strongly, as well as the corresponding adjoint limits. For , source intertwining at every finite sum reads

Continuity of and the two displayed limits yield . This is the limit passage in the linked proof of the stated theorem.
Conjugation gives two continuous star homomorphisms and on the same concrete . They agree on and every , hence on the algebraic star algebra generated by them and then its norm closure. The exact supplier intertwines_of_source_of_generators yields for all .

Main citations

Lean source signature (exact)

theorem exists_pointed_unitary_of_trace_of_cyclic
    (family : RepresentativeShellFamily)
    (ρ : Representation (ShellFamilyTarget family) H)
    (σ : Representation (ShellFamilyTarget family) K) (ξ : H) (η : K)
    (hξ : ∀ a, Representation.vectorFunctional
      (ρ.comp (shellFamilySourceHom family)) ξ a = trace a)
    (hη : ∀ a, Representation.vectorFunctional
      (σ.comp (shellFamilySourceHom family)) η a = trace a)
    (hρ : DenseRange (fun a ↦ ρ a ξ)) (hσ : DenseRange (fun a ↦ σ a η)) :
    ∃ e : H ≃ₗᵢ[ℂ] K, e ξ = η ∧
      ∀ a, (e : H →L[ℂ] K).comp (ρ a) = (σ a).comp (e : H →L[ℂ] K)

family fixes and . The two Representation arguments are and their vectors are . hξ and hη are equality of the source vector functionals with trace; The arguments hρ and hσ concern target orbits. The returned e points from the first Hilbert space to the second. The linked proof's source restrictions, source-density facts and shell-sum limits are proof-local names; the displayed signature retains the full quantified conclusion. In continuous-operator source, † is the adjoint written in the mathematics.

Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF

Lean realization notes

All shell convergence used below is proved inside each actual representation. The argument does not pass strong convergence through an arbitrary star homomorphism. A star on a bounded operator denotes its Hilbert adjoint, corresponding to Lean's postfix dagger on continuous linear operators.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:c41bda62e5281a979102c633562d73a42b5079e8eeef6d65928a8701f3d3ae23

Card revision: 1 · SHA-256: 19aada20d6485c9f12877628bd41c79977e2de0905d433433abf4d900666fe90

Exposition revision: 1 · SHA-256: 64d1456f00ba8382c30c40f6939320ee9b8e42154829d0731c19baaecee17d2e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: c28a4fd8225b7394196a2df449909a32ae606f8887236aefe96e5adbc682f14c