MATHLIBANNEX / CANONICAL DECLARATION CARD

Every irreducible representation is unitarily equivalent to the inclusion

MathlibAnnex.CStarAlgebra.CAR.ambientInclusion_unitaryEquivalent

theorem

Extends the unitary equivalence from the CAR source to all additional generators and the norm-closed target.

Statement

For the data and assumptions below, there is a complex-linear unitary such that for every and . Equivalently, the inclusion representation is unitarily equivalent to .

Assumptions

Let be the completed CAR algebra, the completion of the matrix stages under . Let be the image of the first diagonal matrix unit, so and decreases through projections. The root state takes the value on each matrix stage.

Choose one pure state from each unitary-equivalence class of pure-state Gelfand-Naimark-Segal (GNS) representations, with root index and . Write for its complete complex GNS space, unital star representation and unit cyclic vector. Set , , and let be the coordinate embedding. No countability of is assumed. Inner products are linear in the second argument.

A supplied shell family consists of unital complex star automorphisms and elements . Put . The identities are , and . At the root, is the identity and . The family is an input, not an existence conclusion.

Let be unitaries on satisfying for all , and assume . Let be the norm-closed unital star algebra they generate. Write as an element of , and for the element represented by . Let be a unital complex star representation on a complete complex Hilbert space, put , and put . Assume is nonzero and irreducible: its only closed reducing subspaces are and . In addition, require for every . These are prescribed links between the selected cyclic vectors. The theorem applies to every complete complex target Hilbert space and every nonzero irreducible on it; no separability or fixed dimension is assumed.

Conclusion

A single unitary intertwines the whole target algebra, including its added generators. This identifies the irreducible representation with the concrete inclusion. Combining it with the construction of the faithful irreducible inclusion gives the fixed-family structural theorem. The family supplying the shell data remains a hypothesis.

Proof route

Use the same surjective isometry supplied by surjective cyclic-sum assembly, now viewed as a unitary. For each generator, shell reconstruction gives a strong shell part and a residual corner on both Hilbert spaces. The source intertwiner compares the finite shell sums and hence their strong limits. The atomic common-range theorem identifies the source residual line, and the cyclic-vector transport identifies the remaining corner. Norm-closed generation extends the resulting generator identities to every element of the target.

Proof steps

  1. Regard the same surjective isometry as a unitary, without changing its underlying map. It satisfies and , where the compatible vectors obey . The normalization yields .

  2. For each , reconstruct on and on . The shell parts are the strong limits of the finite sums of and , respectively. The identity for each source element intertwines the two finite sums. Boundedness of and uniqueness of vector limits give . This compares two constructed limits rather than applying to a strong limit.

  3. Let and be the projections onto the common ranges of the two represented -flags. Unitary source intertwining identifies the fixed subspaces, so . The atomic common range is . If , then . Since and , the prescribed identities and give .

  4. Adding the shell and residual identities yields for every . Together with source intertwining this holds on the algebraic star algebra generated by and the . Adjoint compatibility uses that is unitary. Continuity in operator norm extends the equality to its closure , proving for every .

Main citations

Lean source signature (exact)

theorem ambientInclusion_unitaryEquivalent
    (family : RepresentativeShellFamily)
    (L : MathlibAnnex.CStarAlgebra.PureState.GNSClass Limit →
      MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState)
    (hLunit : ∀ i, L i ∈ unitary
      (MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState →L[ℂ]
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState))
    (hLmap : ∀ 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))
    (hLsource : ∀ i n, (L i).comp (selectedAtomicRepresentation
      (transportedFlag family i n - transportedFlag family i (n + 1))) =
        representedShellLink family i n)
    (hLroot : L completedRootPureState.classOf = 1)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K] (rho : Representation (AtomicTarget L) K)
    (hrho : rho.IsIrreducible) :
    (MathlibAnnex.CStarAlgebra.AtomicConstruction.ambientInclusion selectedAtomicRepresentation L).UnitaryEquivalent
      rho

Here Limit is and completedRootPureState is the root state bundled with its purity proof. SelectedAtomicHilbert ... is , selectedAtomicRepresentation is , and AtomicTarget L is . ambientInclusion selectedAtomicRepresentation L is the inclusion . At source index i, corresponding to , hLmap is , hLsource is the shell equation, and hLroot is . UnitaryEquivalent requires a surjective complex-linear isometry intertwining every target element, not only the CAR source. hrho asserts nonzero irreducibility of . The proof's local E, defined by LinearIsometryEquiv.ofSurjective W hWsurj, has the same underlying map as ; the mathematical exposition keeps the notation .

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

Lean realization notes

The proof forms shell limits independently on and and compares them through a bounded unitary. It does not assume that an arbitrary representation preserves strong-operator limits, and it does not replace strong convergence by operator-norm convergence. The prescribed cyclic-vector action is used for the residual corner; source intertwining alone does not identify the added generators.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

Card UID: lfh:lfh-declaration-card:sha256:eb751b0f22dde8fb7e06ff32bb25d5db1cd55259e2b97594d65e2f3fc7657452

Card revision: 1 · SHA-256: b8dddc74bf9f0654a8de879f783ff7c092ef0d41663280a93568ddb1a007c8ef

Exposition revision: 1 · SHA-256: 9240c79b6251b9028caa42fe8be517775a4e56eb4a6f9cf135d5837c0b0b4e76

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 532afcc9e0aa314e7d4c10cbe74f33d07f2651ed52eef53d2a0c90720616f91c

Back to top ↑