MATHLIBANNEX / CANONICAL DECLARATION CARD

Pure-state homogeneity of the completed CAR algebra

MathlibAnnex.CStarAlgebra.CAR.homogeneity

theorem

The constructed inner intertwining sequences discharge the supplier hypothesis and give an approximately inner transporting automorphism.

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. Given any pure states on , there is a complex star automorphism such that for every . For every finite set and every , a unitary can be chosen with for all .

Assumptions

The algebra is the fixed CAR completion, and the functionals are pure states. There is no additional intertwining-sequence hypothesis and no general Kishimoto–Ozawa–Sakai assumption.

Conclusion

The approximately inner automorphism transports to in the direction . It is surjective because the construction controls actual inverse automorphisms as well as forward maps.

This theorem asserts homogeneity for CAR. It does not prove the separately defined statement for all simple separable C*-algebras. Approximate innerness does not assert that the two GNS representations are already unitarily equivalent. The adjacent asymptotically inner result carries extra path data and is not the direct proof used by this declaration.

Proof route

The pure-state sequence theorem provides inner automorphisms with forward and inverse pointwise Cauchy behavior and the transported-state limit. The conditional homogeneity theorem applies its two-sided limit construction to this supplier. These two results are exactly the dependencies composed in the selected proof.

Proof steps

  1. For the chosen pure-state pair, apply the pure-state supplier theorem. Its alternating GNS construction uses the summable budget , which also tends to zero for the state estimates; the route explanation below records where each supporting dense-test estimate enters.

  2. Apply the conditional two-sided-limit theorem to this supplier for all pairs. Forward and actual inverse limits are inverse to one another. Continuity preserves the state equation, and a sufficiently late inner automorphism approximates the limit simultaneously on any finite set.

Main citations

Supporting route explanation

Lean source signature (exact)

theorem homogeneity : PureStateHomogeneity
In the source Mathematical meaning
PureStateHomogeneity The fixed completed CAR algebra has this property: every pair of pure states admits a complex star automorphism with for all .
PureStateHomogeneity The same is approximately inner: for any finite and , some unitary satisfies for every . The choice of precedes these tests.
theorem homogeneity The short signature has no extra supplier or general KOS hypothesis. It proves this CAR property rather than merely defining it.

Further source notes: The short proof passes hasInnerIntertwiningSequence_of_pure to homogeneity_of_innerIntertwiningSequences. It does not call the neighboring homogeneity_from_asymptotic theorem.

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

Accepted content SHA-256: ef48b1d1569542be91e2565f91106dc8c5338ccceecbaa3999c5e4490e6f92c6

Accepted source guide SHA-256: 1170fb89d9e609e1bdbc4ca5c9a6f0bb3d6747927bf59e896aa2f8f351241e97

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑