Direct sums of GNS representations and shell unitaries

Scope

Inequivalent pure-GNS classes form the atomic direct sum. Generic shell theorems and the CAR realization supply faithful irreducible operator models, with the required residual-line hypotheses discharged in their appropriate specialization.

7 direct Cards + 9 reused prerequisites = 16 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: Realizing a shell family by a faithful irreducible operator algebra
Key result: An irreducible operator algebra constructed from projection shells

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: 27 — The selected GNS representation of a pure-state class · 32 — The closed operator algebra generated by a representation and extra operators · 28 — Distinct GNS classes have no unitary intertwiner · 29 — The atomic direct sum of the selected CAR representations · 30 — An irreducible operator algebra constructed from projection shells · 31 — The atomic-shell construction on selected pure-GNS fibers · 33 — Realizing a shell family by a faithful irreducible operator algebra

Reused prerequisites: 38 — The atomic common range is one embedded GNS line · 3 — The product-vector state on the completed CAR algebra · 10 — Root compression becomes scalar in norm · 36 — The matching GNS fiber retains exactly its cyclic line · 9 — The decreasing root projections in the CAR completion · 4 — Purity of the completed root state · 2 — The CAR algebra as a completion of finite matrix stages · 37 — An inequivalent GNS fiber has no residual common range · 25 — A fixed representative family of CAR shell data

Detailed route conditions

Let denote pure-GNS equivalence classes and the root-preserving selected data. Distinct classes, not merely distinct state functionals, give inequivalent representations. Their direct sum is on . Write and .

The generic atomic-shell theorem takes the rank-one limiting defects as hypotheses. The pure-GNS specialization discharges irreducibility, inequivalence and normalization, while retaining the shell hypotheses. The separate CAR realization proves the required residual-line identities. It chooses unitary links once. The generic generated algebra permits arbitrary bounded extra operators and does not itself assert the CAR consequences.

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 16 Cards

Level 0 (4 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 (4 Cards)

The selected GNS representation of a pure-state class

The closed operator algebra generated by a representation and extra operators

The CAR algebra as a completion of finite matrix stages

A fixed representative family of CAR shell data

Level 1 (4 Cards)

An irreducible operator algebra constructed from projection shells

Distinct GNS classes have no unitary intertwiner

The product-vector state on the completed CAR algebra

The decreasing root projections in the CAR completion

Level 2 (3 Cards)

The atomic-shell construction on selected pure-GNS fibers

Root compression becomes scalar in norm

Purity of the completed root state

Level 3 (3 Cards)

The atomic direct sum of the selected CAR representations

The matching GNS fiber retains exactly its cyclic line

An inequivalent GNS fiber has no residual common range

Level 4 (1 Card)

The atomic common range is one embedded GNS line

Level 5 (1 Card)

Realizing a shell family by a faithful irreducible operator algebra