MATHLIBANNEX / PROJECT LFH

One C*-algebra and its representation-theoretic properties

Specialize the supplied family to the once-chosen homogeneity family. The algebra remains , with inclusion . The structural theorem gives its faithful irreducible inclusion and the unique nonzero irreducible representation class, including possibly nonunital inputs.

The same acts faithfully on the separable CAR trace space by . It has no nonzero irreducible representation on a separable Hilbert space. The proof first establishes unit preservation and composes the two classification unitaries in the direction before applying the finite-dimensionality theorem. This does not rule out its irreducible inclusion on the nonseparable atomic space.

Exact Card references

Boundary Inputs

The displayed edges preserve dependency paths through omitted helpers. Levels count selected predecessors within this scope. Mathematical citations remain distinct from formal dependencies.

Exact source and provider boundary · Earlier 466-declaration Project view and PDF

Dependency-first reading route

Levels belong to this reading scope. Follow prerequisites or uses to focus the route.

7 declarations

Level 0

Level 0Focus target

The C*-algebra generated by the CAR representation and the shell unitaries

MathlibAnnex.CStarAlgebra.CAR.AtomicCounterexampleAlgebra

Defines the single algebra used in the irreducible and separable faithful representations.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
The fixed algebra on the CAR trace Hilbert space, The ambient representation of the fixed algebra

Open Declaration CardRead exact source
Level 0Focus target

A simple C*-algebra with a unique irreducible representation class

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint

Establishes the properties that make the fixed algebra a counterexample to Naimark's problem.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
No nonzero irreducible representation on a separable Hilbert space

Open Declaration CardRead exact source

Level 1

Level 1Focus target

The ambient representation of the fixed algebra

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleRepresentation

Defines the inclusion representation .

Immediate prerequisites in this Project
The C*-algebra generated by the CAR representation and the shell unitaries

Used by in this Project
No nonzero irreducible representation on a separable Hilbert space

Open Declaration CardRead exact source
Level 1Focus target

The fixed algebra on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation

Defines a representation of the same algebra on the GNS Hilbert space of the CAR trace.

Immediate prerequisites in this Project
The C*-algebra generated by the CAR representation and the shell unitaries

Used by in this Project
Faithfulness of the representation on the CAR trace Hilbert space

Open Declaration CardRead exact source

Level 2

Level 2Focus target

Faithfulness of the representation on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.separableCounterexampleRepresentation_injective

Proves that the representation is injective.

Immediate prerequisites in this Project
The fixed algebra on the CAR trace Hilbert space

Used by in this Project
A separably represented C*-algebra with no separable irreducible representation

Open Declaration CardRead exact source
Level 2Focus target

No nonzero irreducible representation on a separable Hilbert space

MathlibAnnex.CStarAlgebra.CAR.not_isIrreducible_of_separable

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

Immediate prerequisites in this Project
The ambient representation of the fixed algebra, A simple C*-algebra with a unique irreducible representation class

Used by in this Project
A separably represented C*-algebra with no separable irreducible representation

Open Declaration CardRead exact source

Level 3

Level 3Focus target

A separably represented C*-algebra with no separable irreducible representation

MathlibAnnex.CStarAlgebra.CAR.atomicCounterexampleEndpoint_and_exists_separable_faithful_representation_and_no_separable_irreducible_representation

The same algebra has a faithful representation on a separable Hilbert space, but no nonzero irreducible representation on any separable Hilbert space.

Immediate prerequisites in this Project
No nonzero irreducible representation on a separable Hilbert space, Faithfulness of the representation on the CAR trace Hilbert space

Used by in this Project
None in this scope

Open Declaration CardRead exact source
Back to top ↑