MATHLIBANNEX / CANONICAL DECLARATION CARD

No nonzero irreducible representation on a separable Hilbert space

MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

theorem

Rules out irreducible representations of on separable Hilbert spaces by the finite-dimensionality theorem for a single irreducible representation class.

Statement

Let be the completed CAR algebra. Let be the direct sum of one chosen GNS representation from each pure-state GNS equivalence class, and let be the unitaries obtained from the fixed CAR homogeneity and shell construction. Put , and write for the embedding into . For every separable complex Hilbert space , there is no nonzero irreducible -representation Preservation of the identity is not assumed. Here irreducibility means that the only closed subspaces of invariant under every are and ; for a -representation these subspaces also reduce the representation.

Assumptions

The algebra is the particular algebra constructed above, not an arbitrary C*-algebra. Its established properties are infinite dimensionality and a faithful irreducible inclusion to which every nonzero irreducible representation is unitarily equivalent. Separability is required of , not of ; faithfulness and preservation of the identity are not assumptions on .

Conclusion

Every nonzero -representation of on a separable Hilbert space is reducible. This does not rule out irreducible representations on nonseparable spaces: the inclusion is one.

The theorem places no separability restriction on the Hilbert space of another irreducible representation used for comparison. It asserts nonexistence only for the proposed representation on .

Proof route

Suppose that a nonzero irreducible representation exists on a separable . It must preserve the identity. Composing its unitary equivalence with with the equivalence for an arbitrary irreducible representation shows that represents the unique irreducible representation class. The cited finite-dimensionality theorem then contradicts the infinite dimensionality of .

Proof steps

  1. Put . The -representation identities give , , and . Thus is an orthogonal projection with reducing range. Since , one has ; irreducibility therefore forces . The same representation is consequently unital; no new map is introduced.

  2. The classification theorem gives a unitary with . For any nonzero irreducible -representation , the same theorem gives a unitary with . There is no separability assumption on .

  3. Set . For every ,

    Hence every nonzero irreducible representation is unitarily equivalent to .

  4. The cited finite-dimensionality theorem applies to a nonzero unital C*-algebra with exactly one unitary-equivalence class of nonzero irreducible representations, when that class has a representative on a separable Hilbert space. The representation on satisfies precisely these hypotheses, so . But embeds the infinite-dimensional CAR algebra into . This is the contradiction.

Main citations

Supporting route explanation

Lean source signature (exact)

theorem not_isIrreducible_of_separable
    {H : Type v} [NormedAddCommGroup H] [InnerProductSpace ℂ H]
    [CompleteSpace H] [TopologicalSpace.SeparableSpace H]
    (rho : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H)) :
    ¬ rho.IsIrreducible
In the source Mathematical meaning
AtomicCounterexampleAlgebra The one fixed unital shell-generated CAR target , with its established infinite dimension and unique nonzero irreducible representation class.
{H : Type v}; [InnerProductSpace ℂ H]; [CompleteSpace H] An arbitrary complete complex Hilbert space in the independent universe v.
[TopologicalSpace.SeparableSpace H] The space has a countable norm-dense subset. The separability condition belongs to , not to the algebra .
rho : NonUnitalRepresentation (A := AtomicCounterexampleAlgebra) (H := H) Any complex-linear star representation , without an initial unit-preservation or faithfulness requirement. itself is still unital.
¬ rho.IsIrreducible This cannot be both nonzero and irreducible. Here irreducibility includes nonzeroness and absence of proper nonzero closed reducing subspaces. In particular, every nonzero such representation is reducible; the conclusion is not a ban on faithful reducible representations.

Further source notes: NonUnitalRepresentation means a -representation with no requirement that rho 1 = 1; it does not mean that the represented algebra lacks an identity. The local pi := rho.toUnital hrho in the linked proof is the same after has been proved, not the direct-sum representation of CAR. The parameter v allows the Hilbert space to lie in an independent universe; the comparison spaces in that finite-dimensionality theorem lie in the universe of .

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

Accepted content SHA-256: 56b457a745a07c1d9b89ef96a06408fcc196b1a68e62f25848dbc6fe40238e48

Accepted source guide SHA-256: 2931c34cbe7d5f4ac2a273c9f01fa5faea97a4c7a4868bd9743ce52f1b1cb764

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Back to top ↑