MATHLIBANNEX / CANONICAL DECLARATION CARD

An inequivalent GNS fiber has no residual common range

MathlibAnnex.CStarAlgebra.CAR.selected_commonFixedProjection_eq_zero

theorem

Uses compression and cyclic transport to exclude fixed vectors in every other chosen pure-state class.

Statement

Fix a shell family and indices as below, with . For , let and let be its orthogonal projection. Then , or equivalently .

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. The condition means that the unitary-equivalence classes are distinct, not merely that two state functionals in the same class differ. The selected representation is irreducible and has nonzero Hilbert space because .

Conclusion

The transported flag leaves no nonzero vector fixed in an inequivalent chosen fiber. As a separate consequence of decreasing orthogonal projections, in norm for each fixed . Thus the surviving line in the matching fiber is sharply separated from every other chosen class.

Irreducibility is used to make a nonzero candidate fixed vector cyclic. The conclusion is not asserted for an arbitrary reducible representation or for a different vector state in the same GNS class. The exact source proves equality of projections; strong convergence uses the additional cited projection theorem and does not imply operator-norm convergence.

Proof route

If contained a unit vector , the transported CAR compression estimate , valid for every , would imply . Irreducibility makes cyclic. Equality of this vector state with the state of yields a unitary intertwiner from to , contradicting their distinct classes.

Proof steps

  1. If , choose with and normalize to a unit vector . Since projects onto the common range, every fixes .

  2. Take the matrix coefficient of the represented compression error against . Fixedness and unit norm turn it into the constant ; norm convergence forces this constant to vanish.

  3. The orbit closures of and are their full Hilbert spaces. Equality of vector states gives equality of orbit inner products, so the map extends to a surjective complex-linear isometry that intertwines the representations. This contradicts .

Main citations

Lean source signature (exact)

theorem selected_commonFixedProjection_eq_zero
    (family : RepresentativeShellFamily) {i j : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit}
    (hij : j ≠ i) :
    commonFixedProjection (fun n ↦
      MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState j
        (transportedFlag family i n)) = 0
In the source Mathematical meaning
family; {i j : GNSClass Limit} The fixed CAR shell family, its flag index , and the selected GNS representation index . These indices are unitary-equivalence classes of pure-state GNS representations.
hij : j ≠ i The representing class differs from the flag class. Distinct state functionals in one class would not satisfy this condition.
transportedFlag family i n The projection in , with the flag still indexed by .
selectedRepresentation completedRootPureState j (...) The represented projection on the different selected fiber .
commonFixedProjection (fun n ↦ ...) = 0 The orthogonal projection onto is the zero operator on , equivalently . The quantification is over these selected fibers, not arbitrary reducible representations.

Further source notes: Here Limit is and completedRootPureState is the root state , bundled with its purity proof. The quantified indices range over chosen GNS classes, not over arbitrary vectors or arbitrary representations.

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_zero

Accepted content SHA-256: 7d7c162eb750b8de37d22f76b08d600e65af91db27d0ca9793def297eb6e177f

Accepted source guide SHA-256: 333ba18f04c226451722c428df2d40746ae26500e2cf23d17743089cd60f6b40

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑