MATHLIBANNEX / CANONICAL DECLARATION CARD

The matching GNS fiber retains exactly its cyclic line

MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_rankOne

theorem

Identifies the residual projection of a transported CAR flag in its matching pure-state representation.

Statement

For the fixed shell family and index described below, set and . The orthogonal projection onto satisfies for every . In particular, .

Assumptions

Let be the completed CAR algebra, the completion of the matrix stages under . Write for the image of the first diagonal matrix unit. These are decreasing projections with . Write for the canonical embedding of stage . The root state is determined by on every stage.

Choose one pure state from each unitary-equivalence class of pure-state Gelfand-Naimark-Segal (GNS) representations, retaining at the root index . Write for its complete complex GNS space, unital star representation and unit cyclic vector. Thus , and the vectors are dense in . Inner products are linear in the second argument.

A fixed shell family supplies unital complex star automorphisms and elements with , , and . At the root, is the identity and . Fix and put . The family is supplied; its existence is not an extra conclusion here.

Conclusion

The one-dimensional common range is a proved property of the transported flag, not a field imposed on the shell family. Since are decreasing orthogonal projections, the cited decreasing-projection theorem also gives in norm for each fixed .

The exact declaration identifies the common fixed projection. The pointwise convergence just stated is a consequence using the separately cited decreasing-projection theorem. Neither statement asserts operator-norm convergence, and no strong limit is transported through a representation of a different algebra.

Proof route

The state identity gives , so every fixes . The transported CAR compression estimate gives for each . Contractivity of and fixedness of vectors in yield . Applying this to determines on its dense cyclic orbit and hence on all of .

Proof steps

  1. For a projection , the identity implies . Therefore .

  2. On vectors fixed by every , the matrix coefficient of the represented compression error is independent of and tends to zero. This proves the displayed compressed-operator identity. The source error converges in the norm of .

  3. Consequently . Both sides are continuous linear maps of the orbit vector, and that orbit is dense. The unit norm of identifies the resulting rank-one map as an orthogonal projection.

Main citations

Lean source signature (exact)

theorem selected_commonFixedProjection_eq_rankOne
    (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :
    commonFixedProjection (fun n ↦
      MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState i
        (transportedFlag family i n)) =
      InnerProductSpace.rankOne ℂ
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)
In the source Mathematical meaning
family : RepresentativeShellFamily; i : GNSClass Limit The fixed shell family for CAR and its chosen pure-GNS class , giving and the selected GNS data for the matching state . The root is the bundled pure state completedRootPureState.
selectedRepresentation completedRootPureState i (transportedFlag family i n) The orthogonal projection on the matching fiber .
commonFixedProjection (fun n ↦ ...) The orthogonal projection onto , equivalently onto vectors fixed by every .
selectedVector completedRootPureState i The unit cyclic vector of the same selected GNS representation.
InnerProductSpace.rankOne ℂ (...) (...) Both arguments are that same . The operator sends to , with inner product linear in its second entry.
commonFixedProjection (...) = InnerProductSpace.rankOne ℂ ... ... The conclusion identifies with this rank-one operator, hence . The separate strong-convergence consequence in the text is not an additional filter statement in this signature.

Further source notes: Here Limit is and completedRootPureState is the root state , bundled with its purity proof. The equality itself is not a filter-limit statement.

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.selected_commonFixedProjection_eq_rankOne

Accepted content SHA-256: 592494ead91c6e58a7191a41c23cfeadeaf4d5be767542f719be4bc348994b40

Accepted source guide SHA-256: 7c1c4f170c5476575fcb7c1b1e4b7da8b955aa88da1f8a0c63dc9a0204f8d1b3

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑