MATHLIBANNEX / CANONICAL DECLARATION CARD

Pure CAR states admit two-sided inner intertwining sequences

MathlibAnnex.CStarAlgebra.CAR.hasInnerIntertwiningSequence_of_pure

theorem

Finite-set vector-state transport supplies explicit corrections; their summable conjugation bounds and state estimates yield the required two-sided sequence.

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. For a unitary , write . For every pair of pure states on , there is a sequence such that, for every , both and are norm-Cauchy, and .

Assumptions

The input functionals are pure states on the fixed completed CAR algebra. Their GNS representations and unit cyclic vectors are constructed from these states; no identification of their Hilbert spaces, equivalence of their representations, or initial closeness of the two states is assumed.

Conclusion

The required inner intertwining sequence exists for every pure-state pair. Its inverse condition concerns the actual inverses of the produced automorphisms. This is the supplier used by the separate limit theorem.

Proof route

Use the finite-set vector-state transport theorem to construct unitaries . Put , , and choose a dense sequence . The corrections are chosen to give, for ,

The first estimates make the four sequences pointwise Cauchy. The second gives the state convergence for . The construction below records the local theorem's hypothesis, the correction it supplies, and the inequality that enables the next application.

Proof steps

  1. The local estimate used in every correction. Put . Fix an irreducible representation , a finite set , and . The finite-set transport theorem gives a finite matrix-unit test set and . If is a unit vector state of and is a unit vector state of another representation, its hypothesis is

    Under this hypothesis, for every finite and , it gives a unitary such that

    Here is the state of when is the state of . The tests are chosen before . The path supplied by the theorem is not needed for this sequence conclusion.

  2. The quantities to be constructed and the induction hypothesis. Take the irreducible GNS representations with unit cyclic vectors . Choose a dense sequence in , and put and . For unitaries , write

    These are the vector states of and . To control both an automorphism and its inverse, use

    Apply the local theorem to , obtaining . The induction hypothesis is the explicit inequality

    It enables the local theorem to change toward with any later finite request. Purity is used to make both GNS representations irreducible; they will be used in separate applications of the theorem.

  3. Initialize the induction without assuming that and are close. First obtain from the local theorem for . The unrestricted approximation theorem supplies with

    Now is fixed. Obtain for . The displayed inequality enables the theorem with and . Request and . Its output satisfies

    With , this is exactly the induction hypothesis at .

  4. Construct and obtain the estimate that will imply state convergence. Assume the induction hypothesis at . First obtain from the local theorem for . Apply the already enabled theorem to , , with

    Let be its output, and define

    The theorem gives the two estimates

    In the first line both signs are required. Restricting the second line to gives

    which is precisely the hypothesis for the next application. Restricting it instead to gives

    This second restriction, not merely closeness on the matrix units, will give .

  5. Construct and verify the next induction hypothesis. Since is now fixed, obtain for . Apply the theorem enabled in the preceding step, using

    For its output , set

    The conclusions are

    The second line is the induction hypothesis at . Thus every correction is supplied by the finite-set transport theorem, and every required stage-test hypothesis is the preceding correction's conclusion. The test sets are always chosen before the correction that must meet them.

  6. Derive all four Cauchy estimates. For , protection of and gives, respectively,

    The first equality uses that is isometric. The second explains why was included in . The estimates give the same two bounds for and . Consequently, for any of the four sequences and ,

    For arbitrary , isometry then gives

    First approximate by a fixed , then let . This proves the four pointwise Cauchy assertions. It does not assert norm convergence of the unitaries .

  7. Form the inner automorphisms and check their actual inverses. Define

    The previous step implies pointwise convergence of each of the four sequences, since is complete. To see explicitly that the two compositions are Cauchy, use the following estimate. If are pointwise Cauchy isometries, let and . Then

    Apply this once with and once with . It proves the required Cauchy conditions for and its actual inverse .

  8. Obtain the state convergence by substitution. For , the boxed estimate in the construction of becomes

    This is why the requested set contained and why the output pairs with , rather than with . For every , contractivity of the states and isometry of give

    Density, followed by , yields . Together with innerness and the two Cauchy conditions, this is exactly .

Main citations

Lean source signature (exact)

theorem hasInnerIntertwiningSequence_of_pure
    (phi psi : Limit →L[ℂ] ℂ)
    (hphi : MathlibAnnex.CStarAlgebra.IsPureState Limit phi) (hpsi : MathlibAnnex.CStarAlgebra.IsPureState Limit psi) :
    HasInnerIntertwiningSequence phi psi

Here phi, psi are . In the linked GNS proof, rho, sigma are , and xi, eta are their unit cyclic vectors. In the transition proof, s.move is the local theorem specialized using the displayed induction hypothesis. Its output u is , while hB supplies the output v denoted ; left' = u * s.left and right' = v * s.right are and . The proof hBclose verifies the inequality, and hAclose verifies the next inequality. These names occur in the linked proof, not in the displayed signature. innerAt l is , and outputUnitary n is . The dense-state estimate is obtained by substituting , exactly as displayed above.

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

Lean realization notes

The implementation also records paths for the local corrections, but this selected theorem only concludes the sequence property. Its proof does not presume a transporting endpoint automorphism or a general KOS principle. All choices below are made once within this construction.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: b7e0f73e3b318db4bc9c1cf34d55c3106c4a7e4dde0b330fddafafffc3c3c902

Exposition revision: 1 · SHA-256: 8a6ed21b4319688fca619a236dcd49f2620a74fd07e4ec36b855818b20475d35

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 8d82ab0b3a186480c0fb043e7a0b4c6a465c7a41e37d5cf2a1b13c4e92f38c3b

Back to top ↑