MATHLIBANNEX / CANONICAL DECLARATION CARD

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.

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.

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
  1. 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.

  1. 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.

  1. 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 .

  1. 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.

  2. 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 .

  1. 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.

  1. 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

Supporting route explanation

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)
In the source Mathematical meaning
family : RepresentativeShellFamily The fixed CAR shell family, once-chosen links, target and injective source map . The normalized source trace is .
ρ : Representation (ShellFamilyTarget family) H; σ : Representation (...) K The given unital star representations and , with complete complex Hilbert spaces as in the surrounding source context.
ξ : H; η : K The given vectors and . Their norms equal one as a consequence of the trace conditions at .
hξ : ∀ a, Representation.vectorFunctional (ρ.comp (shellFamilySourceHom family)) ξ a = trace a For every , ; .comp restricts along . Inner products are linear in their second argument.
hη : ∀ a, Representation.vectorFunctional (σ.comp (shellFamilySourceHom family)) η a = trace a For every same source element , .
hρ : DenseRange (fun a ↦ ρ a ξ) The target orbit is dense in . Source-orbit density is derived, not this hypothesis.
hσ : DenseRange (fun a ↦ σ a η) The target orbit is dense in . Neither representation is assumed irreducible.
∃ e : H ≃ₗᵢ[ℂ] K, e ξ = η One surjective complex-linear isometry is produced in this direction and sends the specified to the specified .
∀ a, (e : H →L[ℂ] K).comp (ρ a) = (σ a).comp (e : H →L[ℂ] K) For every target element (source a here), that same satisfies . The casts read the same unitary as a bounded operator. The output intertwines all of , not only its CAR source.

Further source notes: 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.

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

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic

Accepted content SHA-256: 3b4e2554284d889d714ea72fdcfd034197966df38ab4adda67d2f01fe2eb43a1

Accepted source guide SHA-256: 810c986e8b8b361a5dddc8f1b9dfcca446b107231cd986ceb9dd2ea25b6903d2

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑