MATHLIBANNEX / CANONICAL DECLARATION CARD

Realizing a shell family by a faithful irreducible operator algebra

MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel

theorem

Constructs unitary links between pure-state summands and an irreducible algebra containing a faithful copy of CAR.

Statement

Let be the completed CAR algebra and fix a shell family as defined below. Let be the Hilbert direct sum of the chosen pure-state Gelfand-Naimark-Segal (GNS) spaces, their representation, and the embedded unit cyclic vectors, where is the selected unit cyclic vector and is coordinate inclusion. There exist unitaries on with , for every , and . The norm-closed unital star algebra in the bounded operators contains an injective copy of and acts irreducibly on .

Assumptions

Let be the completed CAR algebra with matrix stages embedded by . Write for the image of the first diagonal matrix unit, , and for the root state characterized by on each stage, where is its canonical embedding.

Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes , with root index and representative states .

A fixed shell family consists of complex-linear unital star automorphisms and elements satisfying , and .

At the root, is the identity and . The Hilbert spaces are the chosen complete complex GNS spaces. No countability of is assumed. Irreducibility means a nonzero representation with no proper nonzero closed reducing subspace.

Conclusion

The shell identities are realized by actual bounded unitary operators on one Hilbert space. The generated algebra acts irreducibly while retaining the original algebra faithfully; rank-one limiting projections and irreducibility are proved consequences, not fields imposed on the input family.

Proof route

By the atomic common-range theorem, the decreasing projections start at the identity and have common range ; the root flag has common range . The represented links identify their corresponding orthogonal difference shells. The cited atomic-shell construction joins these partial isometries and the map between the one-dimensional residual spaces into unitaries. Its irreducibility argument uses the inequivalent irreducible GNS summands and the links between their cyclic vectors. Faithfulness comes from the faithful root summand of .

Proof steps

  1. The support equations give initial projection and final projection for each represented shell link.

  2. Use the proved common-range identity to identify the residual projections with the rank-one projections onto and . Apply the atomic-shell existence theorem, which supplies the unitaries and irreducibility of the generated algebra.

  3. At the root the constructed link is the identity on every difference shell and on the residual line. These subspaces reconstruct , so . The faithful root summand makes , hence its codomain restriction to , injective.

Main citations

Lean source signature (exact)

theorem exists_completedAtomicShellModel (family : RepresentativeShellFamily) :
    ∃ L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
          MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState,
      (∀ i, L i ∈ unitary
        (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
          MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)) ∧
      (∀ i, L i (MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState i
          (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState i)) =
        MathlibAnnex.CStarAlgebra.PureState.selectedEmbedding completedRootPureState
          completedRootPureState.classOf
          (MathlibAnnex.CStarAlgebra.PureState.selectedVector completedRootPureState
            completedRootPureState.classOf)) ∧
      (∀ i n, (L i).comp (selectedAtomicRepresentation
          (transportedFlag family i n - transportedFlag family i (n + 1))) =
        representedShellLink family i n) ∧
      L completedRootPureState.classOf = 1 ∧
      Function.Injective
        (MathlibAnnex.CStarAlgebra.AtomicConstruction.sourceHom selectedAtomicRepresentation L) ∧
      Representation.IsIrreducible
        (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L)

Here Limit is and completedRootPureState is the root state , bundled with its purity proof. RepresentativeShellFamily is the supplied family , SelectedAtomicHilbert completedRootPureState is , and selectedAtomicRepresentation is . The existentially quantified L gives the unitaries : the conjunction records their action on the cyclic vectors and shells, the identity root link, source injectivity and irreducibility of the generated target. It does not assert existence of the input family.

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

Lean realization notes

This is existence of the operator links for a supplied family. It does not construct that family without hypotheses, nor prove uniqueness of every irreducible representation of . The universal capture theorem supplies that additional conclusion. No generic homogeneity principle is a further hypothesis of this exact theorem.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:1ee4a51c5a889e36f8bce5ebb44b8bdb3f459aa589225113d4e8aa518643807f

Card revision: 1 · SHA-256: ee9b781557606ba28fdda63633cfb3efeb167a9f8fbebfe6a215537bd661711d

Exposition revision: 1 · SHA-256: e7453e7f2b99e61e071902e0d57d9689b7865fdf71f8c305b54ea518732264e5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 5d5ce65469648d7f2076676f11dc16b8e64d9cb1c3a1b1cfc91d8285d7cfae9c

Back to top ↑