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.

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

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

NonUnitalRepresentation means a -representation with no requirement that rho 1 = 1; it does not mean that the represented algebra lacks an identity. IsIrreducible here includes nonzeroness. The local pi := rho.toUnital hrho in the linked proof is the same after has been proved, not the direct-sum representation of CAR. hambient_pi and hambient_sigma give and ; hsingleton states that every nonzero irreducible representation is unitarily equivalent to . This is the hypothesis of finiteDimensional_algebra_of_singleton_amongNonUnital. 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

Lean realization notes

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 .

Exact Card identity

Language: en

CARD_CONTENT_COMPLETE

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

Card revision: 2 · SHA-256: ad091ef1bdb46599561192f9b2e32004e2aa24220ab5bf053514f7acb52b56d2

Exposition revision: 3 · SHA-256: 49a354534a5b9d1bbf79c20ced250a9d16874d94f3c28f7f43b29b7d02e0f644

Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73

Header SHA-256: 25c41b07d54cfae7df899e502aa960b59251a1dd4dbadf644a548eab01c341f0

Back to top ↑