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.

Main citations

Lean source signature (exact)

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))

Here f n is and (f n).symm is its actual inverse. CauchySeq requires the indicated sequence to be Cauchy in the norm of . Unitary.conjStarAlgAut ... u is , and the final Tendsto is . The declaration has no pure-state hypotheses.

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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:3a00c38e5cfbc169199899139bb5af496a1cb4605988028033c5f4205c31c152

Card revision: 1 · SHA-256: c12901c424aeb424e93bca7877c15915eedc9859c2ffe83ba67265c5b22a7dd0

Exposition revision: 1 · SHA-256: 38a7fba1be45ea9bd4b71934ec7089d0e47e498e279d7a6d738f9e8076c7cbd7

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 9aa21c856a50f60729adb14adbbda9a5a36c1ee80ef79c0b631292ae55e1ebf5