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.

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.

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)
In the source Mathematical meaning
family : RepresentativeShellFamily; ShellFamilyTarget family The supplied normalized CAR shell family fixes once the links and target . The algebra itself is unital.
K; [InnerProductSpace ℂ K]; [CompleteSpace K] Any complete complex Hilbert space in the independently quantified universe, without a separability or dimension restriction.
rho : NonUnitalRepresentation (A := ShellFamilyTarget family) (H := K) The complex-linear star representation is not initially required to preserve the unit.
hrho : rho.IsIrreducible The original is nonzero and has only and as closed reducing subspaces. Merely assuming would not exclude the zero representation.
∃ U : SelectedAtomicHilbert completedRootPureState ≃ₗᵢ[ℂ] K One surjective complex-linear isometry is produced, where is the fixed selected atomic Hilbert sum.
∀ (a : ShellFamilyTarget family) (x : SelectedAtomicHilbert ...), U (shellFamilyInclusion family a x) = rho a (U x) For every (source a) and , the same obeys , with literal inclusion. The equation retains the original map ; its unit law is derived, not an extra input.

Further source notes: Here completedRootPureState is the root state , bundled with its purity proof, and SelectedAtomicHilbert completedRootPureState is . NonUnitalRepresentation means a complex-linear star representation without a required unit law. 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 · Back to Project

Earlier published Card and PDF

Exact content identity

Declaration: MathlibAnnex.CStarAlgebra.CAR.shellFamilyInclusion_unitaryEquivalent_nonUnital

Accepted content SHA-256: 9ccca95e51c9bdacad23db01a1474366457f1521344494fe88e86bb61d253564

Accepted source guide SHA-256: 364d0e7448478c612f3b2ea0dab183963b09ddfaef729286f33e05ecd7fd1eb7

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑