Characters, eigenvectors and a scalar corner

Scope

Characters of a maximal abelian subalgebra of the unitization extend to pure states. A character distinct from the scalar character yields a joint unit eigenvector in the singleton model. Countability and an isolated non-scalar character then give a nonzero scalar-corner projection and its rank-one image.

11 direct Cards + 8 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: A character becomes a joint unit eigenvector
Key result: A projection represented by a rank-one operator

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: R13 — The scalar character of the unitization · R01 — Maximal abelian -subalgebras · R26 — A maximal abelian subalgebra containing a self-adjoint element · R06 — A character separating a closed ideal · R30 — A character extends to a pure state · R14 — A character becomes a joint unit eigenvector · R33 — The full character space is countable · R21 — An isolated point in a countable Baire space · R27 — An isolated character away from the scalar character · R19 — A nonzero projection with scalar corner · R23 — A projection represented by a rank-one operator

Reused prerequisites: 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 · R20 — The GNS representation of a pure state is irreducible · R24 — Nonzero irreducibility without a unit assumption · R25 — Unitary equivalence of two representations · R32 — Representations without a unit-preservation requirement

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 (6 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 (6 Cards)

An isolated point in a countable Baire space

Maximal abelian -subalgebras

A character separating a closed ideal

The scalar character of the unitization

Pure states as real extreme points

Representations without a unit-preservation requirement

Level 1 (6 Cards)

A character extends to a pure state

An isolated character away from the scalar character

A maximal abelian subalgebra containing a self-adjoint element

The GNS representation of a pure state is irreducible

Unitary equivalence of two representations

Nonzero irreducibility without a unit assumption

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