Trace extensions and faithful representations on a separable space

Fix the same and , and first extend the CAR trace to a state on . Existence precedes uniqueness and traciality. In each trace-realizing cyclic representation, the estimates for and kill the residual projections on the source-cyclic subspace. Target cyclicity then proves source cyclicity. The fixed-left-hand-side limit calculation is retained with its full dependence in the pointed-transport Card.

Pointed transport proves uniqueness among all state extensions. Uniqueness gives invariance under source unitaries; their span and the actual represented shell limits put all generators in the closed centralizer. This proves traciality. A different restriction argument then proves uniqueness among all tracial states.

The CAR trace space and the extension-state space are different: the selected unitary points as , and . This is not the capture map . Faithfulness of a representation is distinct from faithfulness of its vector state. The Hilbert spaces are separable here; norm separability of is not assumed.

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.

Search declarations Route 9 declarations

Level 0

Level 0Focus target

Extending the CAR trace to the fixed shell target

MathlibAnnex.CStarAlgebra.CAR.exists_state_extension_trace

The source trace first becomes a state on the existing target algebra.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
The GNS representation of the target trace extension

Open Declaration Card Read exact source

Level 0Focus target

Pointed unitary transport between trace-cyclic target representations

MathlibAnnex.CStarAlgebra.CAR.exists_pointed_unitary_of_trace_of_cyclic

Source cyclicity and strong shell sums extend the canonical CAR orbit isometry to the whole target.

Immediate prerequisites in this Project
None in this scope

Used by in this Project
The unique trace extension is tracial on the whole target, Uniqueness among all state extensions of the CAR trace

Open Declaration Card Read exact source

Level 1

Level 1Focus target

The GNS representation of the target trace extension

MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation

The chosen state on the existing target supplies its cyclic GNS representation.

Immediate prerequisites in this Project
Extending the CAR trace to the fixed shell target

Used by in this Project
The target represented on the CAR trace GNS space, Faithfulness of the target-state GNS representation, The unique trace extension is tracial on the whole target, Uniqueness among all state extensions of the CAR trace

Open Declaration Card Read exact source

Level 2

Level 2Focus target

Uniqueness among all state extensions of the CAR trace

MathlibAnnex.CStarAlgebra.CAR.existsUnique_state_extension_trace

Pointed transport identifies arbitrary state extensions before traciality is proved.

Immediate prerequisites in this Project
The GNS representation of the target trace extension, Pointed unitary transport between trace-cyclic target representations

Used by in this Project
None in this scope

Open Declaration Card Read exact source

Level 2Focus target

The unique trace extension is tracial on the whole target

MathlibAnnex.CStarAlgebra.CAR.traceExtension_mul_comm

Unitary invariance, strong shell sums, and a closed centralizer extend the trace identity beyond the source.

Immediate prerequisites in this Project
The GNS representation of the target trace extension, Pointed unitary transport between trace-cyclic target representations

Used by in this Project
The fixed shell target has a unique tracial state

Open Declaration Card Read exact source

Level 2Focus target

Faithfulness of the target-state GNS representation

MathlibAnnex.CStarAlgebra.CAR.tracialRepresentation_injective

The ideal dichotomy of the same target forces the constructed nonzero representation to be injective.

Immediate prerequisites in this Project
The GNS representation of the target trace extension

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

Open Declaration Card Read exact source

Level 2Focus target

The target represented on the CAR trace GNS space

MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation

A fixed pointed unitary transports the target action onto the Hilbert space constructed from CAR alone.

Immediate prerequisites in this Project
The GNS representation of the target trace extension

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

Open Declaration Card Read exact source

Level 3

Level 3Focus target

The fixed shell target has a unique tracial state

MathlibAnnex.CStarAlgebra.CAR.existsUnique_tracial_state

Every tracial state is forced back to the CAR trace and hence to its unique extension.

Immediate prerequisites in this Project
The unique trace extension is tracial on the whole target

Used by in this Project
None in this scope

Open Declaration Card Read exact source

Level 3Focus target

Faithfulness of the representation on the CAR trace Hilbert space

MathlibAnnex.CStarAlgebra.CAR.traceModelRepresentation_injective

Unitary conjugation preserves injectivity of the target-state representation.

Immediate prerequisites in this Project
The target represented on the CAR trace GNS space, Faithfulness of the target-state GNS representation

Used by in this Project
None in this scope

Open Declaration Card Read exact source