Every compact operator has a preimage

Scope

One represented rank-one projection yields every rank-one operator using dense orbits. Closed-range and compact approximation arguments put all compact operators in the image of the original algebra.

3 direct Cards + 16 reused prerequisites = 19 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: Compact operators lie in a singleton representation range
Key result: Every rank-one operator has an algebra preimage

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: R23 — A projection represented by a rank-one operator · R04 — Every rank-one operator has an algebra preimage · R02 — Compact operators lie in a singleton representation range

Reused prerequisites: R01 — Maximal abelian -subalgebras · R05 — A representative of the unique irreducible class · R07 — A pure state detects a nonzero square · R08 — Pure states as real extreme points · R12 — Faithfulness from a unique irreducible class · R14 — A character becomes a joint unit eigenvector · R19 — A nonzero projection with scalar corner · R20 — The GNS representation of a pure state is irreducible · R21 — An isolated point in a countable Baire space · R24 — Nonzero irreducibility without a unit assumption · R25 — Unitary equivalence of two representations · R26 — A maximal abelian subalgebra containing a self-adjoint element · R27 — An isolated character away from the scalar character · R30 — A character extends to a pure state · R32 — Representations without a unit-preservation requirement · R33 — The full character space is countable

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

Level 0 (4 Cards)

Level 0

An isolated point in a countable Baire space

Applies the Baire property to the closed cover by singletons.

MathlibAnnex.Topology.exists_isOpen_singleton

Immediate Card prerequisites: None in this selected scope

Used by in this scope: An isolated character away from the scalar character

Scope

Cards in this route

Dependency-first reading route

Level 0 (4 Cards)

An isolated point in a countable Baire space

Maximal abelian -subalgebras

Pure states as real extreme points

Representations without a unit-preservation requirement

Level 1 (6 Cards)

The GNS representation of a pure state is irreducible

A character extends to a pure state

Unitary equivalence of two representations

An isolated character away from the scalar character

Nonzero irreducibility without a unit assumption

A maximal abelian subalgebra containing a self-adjoint element

Level 2 (2 Cards)

A representative of the unique irreducible class

A pure state detects a nonzero square

Level 3 (2 Cards)

A character becomes a joint unit eigenvector

Faithfulness from a unique irreducible class

Level 4 (1 Card)

The full character space is countable

Level 5 (1 Card)

A nonzero projection with scalar corner

Level 6 (1 Card)

A projection represented by a rank-one operator

Level 7 (1 Card)

Every rank-one operator has an algebra preimage

Level 8 (1 Card)

Compact operators lie in a singleton representation range