MATHLIBANNEX / CANONICAL DECLARATION CARD

The atomic common range is one embedded GNS line

MathlibAnnex.CStarAlgebra.CAR.iInf_range_atomic_transportedFlag_eq_span

theorem

Assembles the matching and inequivalent fiber calculations in an arbitrary Hilbert direct sum.

Statement

For a fixed shell family and as below, let and . Denote the coordinate embedding by . Then , where .

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 Hilbert direct sum consists of square-summable families , and acts coordinatewise. No countability of is assumed. The coordinate embedding is isometric, so is a unit vector.

Conclusion

The orthogonal projection onto this common range is the rank-one map . The decreasing-projection theorem therefore gives strong convergence of to this map. In the construction of the shell unitaries, this is the one-dimensional residual space joined to the root residual line when the difference-shell maps are completed to a unitary.

The exact declaration is the equality of subspaces, and its identity remains separate from the two fiber declarations. The rank-one and strong-limit assertions are explained consequences. The coordinate proof works for an arbitrary index set; it does not exchange an uncountable sum with a limit or assert operator-norm convergence.

Proof route

A vector is in the range of an orthogonal projection exactly when that projection fixes it. Thus a vector belongs to the common range exactly when every coordinate is fixed by all . The matching-fiber common-range theorem forces to be a scalar multiple of , while the inequivalent-fiber common-range theorem forces for . Conversely, the embedded vector and all its scalar multiples are fixed by every .

Proof steps

  1. For a vector in the common range, apply each coordinate evaluation to . This gives fixedness in every fiber without a sum-limit argument.

  2. The common projection in fiber sends to ; since is fixed it equals that value. For , the common projection is zero, so fixedness gives . Therefore .

  3. Every flag projection fixes in the matching fiber. Acting coordinatewise therefore fixes every scalar multiple of , proving the reverse inclusion. The unit norm then identifies the projection onto the resulting line.

Main citations

Lean source signature (exact)

theorem iInf_range_atomic_transportedFlag_eq_span
    (family : RepresentativeShellFamily) (i : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit) :
    (⨅ n, (atomicRepresentation
      (MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation completedRootPureState)
      (transportedFlag family i n)).range) =
      ℂ ∙ MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
        (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)
In the source Mathematical meaning
family; i : GNSClass Limit The fixed CAR shell family and flag class , with .
atomicRepresentation (selectedRepresentation completedRootPureState) The coordinatewise representation on . The index set need not be countable.
(atomicRepresentation ... (transportedFlag family i n)).range The linear subspace of the atomic Hilbert space.
⨅ n, (...).range The intersection of those subspaces over all natural stages: .
selectedEmbedding completedRootPureState i (selectedVector completedRootPureState i) The vector , where is the selected unit cyclic vector and embeds it in coordinate .
ℂ ∙ ... The one-dimensional complex span of that vector. The whole equality says the common range is exactly this line, not the entire fiber .

Further source notes: Here Limit is and completedRootPureState is the root state , bundled with its purity proof. The right side ℂ ∙ ... is its complex linear span, not the entire -th GNS fiber.

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

Accepted content SHA-256: d818b9e9438681168b843bf6da06bd7fcced608354bbee6789c028f530cc3fbe

Accepted source guide SHA-256: 9ce6ca9d690304828da3587072e1ca48d4efc889bdb6fe28a41a830dae1e8104

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑