MATHLIBANNEX / CANONICAL DECLARATION CARD

Unitary equivalence without an initial unitality assumption

MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital

theorem

Shows why allowing nonunital input representations does not enlarge the irreducible representation class of the shell-generated algebra.

Statement

Let be the fixed shell-generated algebra below. If is a nonzero irreducible complex-linear star representation, then a surjective complex-linear isometry satisfies for every and . Preservation of the unit is a consequence, not an additional hypothesis 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 .

Let be the Hilbert direct sum of these GNS spaces, their representation of , and its embedded unit cyclic vector, where is the selected unit cyclic vector and is coordinate inclusion.

Choose once a family of unitary operators from the construction of the shell unitaries: , , and . Here denotes the bounded complex-linear operators on .

Put , the norm-closed unital star algebra generated by these operators. Let be with its codomain restricted to , and let be inclusion.

The space is any complete complex Hilbert space in an independent universe. Irreducibility here explicitly includes and the assertion that its closed reducing subspaces are only and . Nontriviality of alone is not a replacement for .

Conclusion

The intertwining equation uses the original map . All its represented operators are retained when one regards it as a unital representation. Thus the displayed inclusion represents every such irreducible class up to unitary equivalence.

Proof route

Put . It is an idempotent, and its range is closed and reducing for . Nonzeroness makes this range nonzero, so irreducibility makes it all of ; an idempotent is the identity on its range, giving . The unital capture theorem applies to the same operators, since the unit law has just been established. Its unitary intertwiner therefore satisfies the equation for the original map.

Proof steps

  1. For every , . Star preservation also controls adjoints, so the range of is reducing.

  2. If , then every is zero. Irreducibility therefore forces the closed range of this nonzero idempotent to be , whence .

  3. Use the theorem identifying every unital irreducible representation with the fixed inclusion. Rebundling as unital changes no operator, so its resulting unitary equivalence is exactly the claimed one.

Main citations

Lean source signature (exact)

theorem shellFamilyInclusion_unitaryEquivalent_nonUnital
    (family : RepresentativeShellFamily)
    {K : Type v} [NormedAddCommGroup K] [InnerProductSpace ℂ K]
    [CompleteSpace K]
    (rho : NonUnitalRepresentation
      (A := ShellFamilyTarget family) (H := K))
    (hrho : rho.IsIrreducible) :
    ∃ U :
        MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K,
      ∀ (a : ShellFamilyTarget family)
        (x : MathlibAnnex.CStarAlgebra.PureState.SelectedAtomicHilbert completedRootPureState),
        U (shellFamilyInclusion family a x) = rho a (U x)

Here completedRootPureState is the root state , bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is . ShellFamilyTarget family is and shellFamilyInclusion family is . NonUnitalRepresentation means a complex-linear star representation without a required unit law. Its IsIrreducible predicate includes and the closed reducing-subspace condition. The existential quantifier supplies the unitary in the Statement; the proof first derives .

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

Lean realization notes

The result imposes no separability restriction and does not claim that all representations are irreducible. The shell family is fixed before is chosen. The zero representation is excluded by the exact irreducibility predicate.

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 1 · SHA-256: 5e8723732f99734ed20d9eebcec120288986b4189609f25f82176fc458697e28

Exposition revision: 1 · SHA-256: 7cbb07e920950cd3b18272c6d1b936beb2676c8a58df3a9c409cd4ef9323f300

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 8ed71093dcf51bf4181d65871e97a8aff0675699fe53fe257407a7239d1483c0

Back to top ↑