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.

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.

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

The support equations give initial projection and final projection for each represented shell link.
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.
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)

In the source	Mathematical meaning
`family : RepresentativeShellFamily`	The supplied family for the completed CAR algebra , root state , root index , and projections . It satisfies , , , and the stated root normalization. Its existence is not this theorem’s conclusion.
`GNSClass Limit; SelectedAtomicHilbert completedRootPureState`	The index set of pure-GNS unitary-equivalence classes and the Hilbert sum of selected GNS spaces. The selected unit vectors are , their coordinate inclusions , and . No countability is imposed.
`∃ L : ... → ... →L[ℂ] ...`	There is one family of bounded complex-linear operators satisfying all six following clauses simultaneously.
`∀ i, L i ∈ unitary (...)`	First, every is unitary on : .
`∀ i, L i (selectedEmbedding ... i (selectedVector ... i)) = ...`	Second, each same sends to the root vector ; the fully qualified names in the signature select exactly these vectors and inclusions.
`∀ i n, (L i).comp (selectedAtomicRepresentation (transportedFlag family i n - transportedFlag family i (n + 1))) = representedShellLink family i n`	Third, for every , . Here , `transportedFlag` is , and `.comp` applies the rightmost operator first.
`L completedRootPureState.classOf = 1`	Fourth, the root member is .
`Function.Injective (AtomicConstruction.sourceHom selectedAtomicRepresentation L)`	Fifth, the codomain restriction , , is injective, for built from this same .
`Representation.IsIrreducible (AtomicConstruction.ambientInclusion selectedAtomicRepresentation L)`	Sixth, the inclusion representation of that same generated algebra is nonzero and has no proper nonzero closed reducing subspace. This is distinct from injectivity of .
Further source notes: Here `Limit` is and `completedRootPureState` is the root state , bundled with its purity proof. It does not assert existence of the input family.

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

Accepted content SHA-256: b3c1c2a0e02b60f44fcfa567e146983edcace16a3b6335e6d9a480c3e4c5709b

Accepted source guide SHA-256: c1b8891ddbdfcf047307b402e9786f0c45d608a23e6b1b34592e4149ce7d68d5

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73