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.

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.

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

Supporting route explanation

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
In the source Mathematical meaning
hlocal : ∀ (phi psi : Limit →L[ℂ] ℂ), ... The input is a supplier for every pair of pure states on the fixed completed CAR algebra .
IsPureState Limit phi → IsPureState Limit psi → The supplier applies when both functionals are positive normalized extreme points of the real convex state space.
HasInnerIntertwiningSequence phi psi It supplies one sequence of inner automorphisms with and norm-Cauchy for each , and . These are hypotheses furnished by hlocal, not properties of a limiting map assumed in advance.
PureStateHomogeneity The output says that for every pure-state pair there is an automorphism with and, for every finite and , a unitary such that for all . The same meets the state equation and all finite-test requests.

Further source notes: 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.homogeneity_of_innerIntertwiningSequences

Accepted content SHA-256: 9d39da76b45ea1078f777c8f3b580d700e08440140502d9bc4ab0f385760bf8d

Accepted source guide SHA-256: 832ce53cff998750706bf07c3fb3f7cc61bd334be9358103bfbe869b1bcc373e

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑