Trace extensions and faithful representations on a separable space

Scope

The CAR trace extends uniquely to a state on the same shell-generated target, and that extension is tracial. Pointed transport supplies faithful representations on separable trace spaces; representation faithfulness is distinct from faithfulness of a vector state.

9 direct Cards + 30 reused prerequisites = 39 unique Cards. This count is a selected Card closure, not a source-declaration count.

Route reading PDF · Preserved source exploration

Cards in this route

Key result: Uniqueness among all state extensions of the CAR trace
Key result: Faithfulness of the representation on the CAR trace Hilbert space

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: 51 — Extending the CAR trace to the fixed shell target · 59 — Pointed unitary transport between trace-cyclic target representations · 55 — The GNS representation of the target trace extension · 52 — Uniqueness among all state extensions of the CAR trace · 53 — The unique trace extension is tracial on the whole target · 56 — Faithfulness of the target-state GNS representation · 57 — The target represented on the CAR trace GNS space · 54 — The fixed shell target has a unique tracial state · 58 — Faithfulness of the representation on the CAR trace Hilbert space

Reused prerequisites: 38 — The atomic common range is one embedded GNS line · 43 — The ambient inclusion of the fixed shell-family target · 3 — The product-vector state on the completed CAR algebra · 10 — Root compression becomes scalar in norm · 27 — The selected GNS representation of a pure-state class · 36 — The matching GNS fiber retains exactly its cyclic line · 28 — Distinct GNS classes have no unitary intertwiner · 29 — The atomic direct sum of the selected CAR representations · 46 — Every irreducible representation is unitarily equivalent to the inclusion · 33 — Realizing a shell family by a faithful irreducible operator algebra · 42 — The CAR source map into the fixed shell-family target · 34 — Shell matching fixes the trace of transported flags · 1 — The normalized trace on a finite CAR stage · 35 — Transported flags vanish on vectors generated by a trace vector · 9 — The decreasing root projections in the CAR completion · 48 — Closed-ideal simplicity of the shell-generated algebra · 4 — Purity of the completed root state · 30 — An irreducible operator algebra constructed from projection shells · 7 — Constructing the normalized trace on the completed CAR algebra · 2 — The CAR algebra as a completion of finite matrix stages · 37 — An inequivalent GNS fiber has no residual common range · 8 — Normalization and the trace identity determine the CAR trace · 40 — An irreducible target representation has a surviving fixed space · 39 — Reconstructing a represented unitary from its shells and residual corner · 25 — A fixed representative family of CAR shell data · 31 — The atomic-shell construction on selected pure-GNS fibers · 32 — The closed operator algebra generated by a representation and extra operators · 45 — The cyclic sum fills every irreducible target representation · 41 — A common root vector realizes every selected state through the generators · 44 — Assembling selected GNS cyclic subspaces into an isometric source representation

Detailed route conditions

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.

Reference index: exact Card references

Exact Card references

Dependency-first reading route

Read selected Card prerequisites before their uses. Levels are recomputed from the selected reachability-preserving projection; omitted source helpers remain traceable in the source exploration.

Search Cards Route 39 Cards

Level 0 (5 Cards)

Level 0

The selected GNS representation of a pure-state class

A choice of representative pure states, fixed literally at a root, gives one concrete GNS representation per equivalence class.

MathlibAnnex.CStarAlgebra.PureState.selectedRepresentation

Immediate Card prerequisites: None in this selected scope

Used by in this scope: The matching GNS fiber retains exactly its cyclic line · Distinct GNS classes have no unitary intertwiner · The atomic direct sum of the selected CAR representations

Scope

Cards in this route

Detailed route conditions

Exact Card references

Dependency-first reading route

Level 0 (5 Cards)

The selected GNS representation of a pure-state class

The CAR algebra as a completion of finite matrix stages

A fixed representative family of CAR shell data

The closed operator algebra generated by a representation and extra operators

The normalized trace on a finite CAR stage

Level 1 (5 Cards)

Constructing the normalized trace on the completed CAR algebra

The product-vector state on the completed CAR algebra

An irreducible operator algebra constructed from projection shells

Distinct GNS classes have no unitary intertwiner

The decreasing root projections in the CAR completion

Level 2 (5 Cards)

Root compression becomes scalar in norm

Purity of the completed root state

Normalization and the trace identity determine the CAR trace

The atomic-shell construction on selected pure-GNS fibers

Shell matching fixes the trace of transported flags

Level 3 (4 Cards)

The atomic direct sum of the selected CAR representations

The matching GNS fiber retains exactly its cyclic line

Transported flags vanish on vectors generated by a trace vector

An inequivalent GNS fiber has no residual common range

Level 4 (3 Cards)

The atomic common range is one embedded GNS line

Assembling selected GNS cyclic subspaces into an isometric source representation

Reconstructing a represented unitary from its shells and residual corner

Level 5 (2 Cards)

Realizing a shell family by a faithful irreducible operator algebra

An irreducible target representation has a surviving fixed space

Level 6 (3 Cards)

A common root vector realizes every selected state through the generators

The CAR source map into the fixed shell-family target

The ambient inclusion of the fixed shell-family target

Level 7 (3 Cards)

Pointed unitary transport between trace-cyclic target representations

Extending the CAR trace to the fixed shell target

The cyclic sum fills every irreducible target representation

Level 8 (2 Cards)

The GNS representation of the target trace extension

Every irreducible representation is unitarily equivalent to the inclusion

Level 9 (4 Cards)

The target represented on the CAR trace GNS space

Uniqueness among all state extensions of the CAR trace

The unique trace extension is tracial on the whole target

Closed-ideal simplicity of the shell-generated algebra

Level 10 (2 Cards)

The fixed shell target has a unique tracial state

Faithfulness of the target-state GNS representation

Level 11 (1 Card)

Faithfulness of the representation on the CAR trace Hilbert space