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.

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)

Here Limit is and completedRootPureState is the root state , bundled with its purity proof. atomicRepresentation is the coordinatewise representation on . The infimum ⨅ n is the intersection of the represented ranges. selectedEmbedding completedRootPureState i is , and selectedVector completedRootPureState i is . 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

Lean realization notes

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.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:33faef4a7aeea0e449fc97d78875cdf9559b511956c357898bd723b6e6b9090e

Card revision: 1 · SHA-256: 583e915df94134f418287efe8d437652571bc470104d1a618ad60ac1b218045e

Exposition revision: 1 · SHA-256: 55df6b0835b24b50e04e3d553336bb1567747701688653c043731d7d192026a9

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 7e3d59bec6490bf3ab31476e239758a101bd1379bc8b7168dd1874f68976cf91

Back to top ↑