A two-sided inner intertwining sequence for two states

MathlibAnnex.CStarAlgebra.CAR.HasInnerIntertwiningSequence

def

An inner sequence records both forward and actual inverse convergence data before any limiting automorphism is constructed.

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. For a unitary , write . Given continuous complex-linear functionals , an inner intertwining sequence is a sequence of complex star automorphisms with the following properties. For every , both and are Cauchy in norm. Each for some unitary , and for every .

Definition

Choose the automorphisms first and require the four conditions for those choices. Innerness is expressed as existence of an implementing unitary for each index. Norm completeness supplies pointwise limits from the two Cauchy conditions, while the exact inverse identities allow the two limits to be proved inverse to each other.

Assumptions

Only continuity and complex linearity of the two functionals are inputs to this definition. Positivity, normalization, and purity are not required here. The inverse in the second Cauchy condition is the inverse of that same .

Conclusion

The datum is a sequence with four requirements: forward Cauchy behavior, inverse Cauchy behavior, innerness of each term, and pointwise convergence of the transported functional. A limiting automorphism is a later construction, not an additional field of the datum.

Two unrelated Cauchy sequences do not meet the inverse requirement. No convergence of itself is asserted; the relevant convergence is of their conjugation actions on individual algebra elements.

Supporting route explanation

def HasInnerIntertwiningSequence (phi psi : Limit →L[ℂ] ℂ) : Prop :=
  ∃ f : ℕ → StarAlgEquiv ℂ Limit Limit,
    (∀ a, CauchySeq (fun n => f n a)) ∧
    (∀ a, CauchySeq (fun n => (f n).symm a)) ∧
    (∀ n, ∃ u : unitary Limit,
      f n = Unitary.conjStarAlgAut ℂ Limit u) ∧
    ∀ a, Tendsto (fun n => phi (f n a)) atTop (nhds (psi a))

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

Earlier published Card and PDF