MATHLIBANNEX / CANONICAL DECLARATION CARD

Two-sided inner sequences imply pure-state homogeneity

MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences

theorem

The forward and inverse limits close the homogeneity argument once an intertwining sequence is supplied for every pure-state pair.

Statement

Let be the completed CAR algebra, the norm completion of the matrix stages under , with the fixed coordinate reindexing. A state means a positive continuous complex-linear functional taking value at the identity; a pure state is an extreme point of this convex state space. Assume that every pair of pure states admits inner automorphisms such that and are norm-Cauchy for every , and . Then there is an automorphism with , and for every finite and a unitary satisfies for every .

Assumptions

The supplier assumption quantifies over all pure-state pairs and gives the sequence conditions just stated. The theorem is conditional on this supplier. Completeness is a property of the completed CAR algebra, not a claim that a merely dense algebraic union already has these limits.

Conclusion

The algebra has the pure-state homogeneity property. The inverse Cauchy condition is what supplies surjectivity of the limit; approximate innerness then follows by choosing one sufficiently late term for each finite set.

Proof route

Fix a supplied sequence and define and . Operations pass through the limits, and isometry lets the exact inverse identities pass through moving inputs. Thus and are mutually inverse star homomorphisms. Continuity transports the state equation to the limit, and a common late index yields the finite-set approximation.

Proof steps

  1. Each automorphism is an isometry. Norm completeness and the two Cauchy hypotheses therefore give the two pointwise limits. Continuity of addition, multiplication, scalar multiplication, and involution makes the forward limit a unital complex star homomorphism; the inverse limit has the same properties.

  2. For fixed , use . The difference between and this constant value has norm . Passing to the limit at the fixed input gives . Interchanging the two sequences gives . This proves bijectivity rather than only injectivity.

  3. Continuity of gives . The supplied state limit and uniqueness of limits imply .

  4. For a finite set , choose a single index beyond the convergence thresholds for all . If , then on . For the empty set the requirement is vacuous.

Main citations

Lean source signature (exact)

theorem homogeneity_of_innerIntertwiningSequences
    (hlocal : ∀ (phi psi : Limit →L[ℂ] ℂ),
      MathlibAnnex.CStarAlgebra.IsPureState Limit phi → MathlibAnnex.CStarAlgebra.IsPureState Limit psi →
        HasInnerIntertwiningSequence phi psi) :
    PureStateHomogeneity

Here hlocal supplies the sequence for each pair of pure states. In the linked proof, rather than in this signature, f is , and hf, hfinv are its forward and actual inverse Cauchy hypotheses. The exact proof uses twoSidedPointwiseLimit and its state/approximation theorem. Its output PureStateHomogeneity has the composition direction .

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

Lean realization notes

This assembly theorem does not itself construct the sequences. The separate pure-state supplier discharges that hypothesis for CAR. It neither uses nor proves the general all-simple-separable-algebras KOS proposition.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:956c24ba7d52ceb88f40cb266a7aa12df59d518e2c8ddd9a94ef16d312c5c1e1

Card revision: 1 · SHA-256: 31de10b4bf30350d4acecff8e7349eeb3d3aabd7a2a42cbe5a0255bc13a6f18e

Exposition revision: 1 · SHA-256: 89806d19203e218a87f8efb6b7fda4e0e2b9f6dbab26730d939d05b3c4cb2c70

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: d20a03d25f7a75545342d7f67e5ed9c6b05b2a9e7a34bdfa69e5e5ae6a29775c

Back to top ↑