Compact-operator models and unital consequences

Scope

Faithfulness and both compact-image inclusions identify the nonunital compact-operator model in an unbundled sense. In the unital singleton case the identity becomes compact, yielding finite dimension and the exact full-operator image consequences.

12 direct Cards + 20 reused prerequisites = 32 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 singleton model is faithful and exactly compact-valued
Unital consequence: Finite-dimensional algebra in the unital singleton case

Read this route with prerequisites

Reference index: direct Cards and reused prerequisites

Direct references: R09 — A compact-operator model for a representation · R12 — Faithfulness from a unique irreducible class · R02 — Compact operators lie in a singleton representation range · R17 — Every operator in a singleton image is compact · R10 — A singleton model is faithful and exactly compact-valued · R11 — Singleton condition tested against all irreducible representations · R15 — Compact-operator conclusion for the unital singleton condition · R18 — A unital singleton model acts in finite dimension · R31 — Finite-dimensional representation space in the unital singleton case · R29 — Finite-dimensional algebra in the unital singleton case · R22 — Full operator image in finite dimension · R28 — An infinite-dimensional unital algebra has no separable singleton model

Reused prerequisites: R01 — Maximal abelian -subalgebras · R03 — A faithful singleton model forces simplicity · R04 — Every rank-one operator has an algebra preimage · R05 — A representative of the unique irreducible class · R06 — A character separating a closed ideal · R07 — A pure state detects a nonzero square · R08 — Pure states as real extreme points · R14 — A character becomes a joint unit eigenvector · R16 — The preimage ideal of the compact operators · 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 · R23 — A projection represented by a rank-one operator · 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 32 Cards

Level 0 (9 Cards)

Level 0

Full operator image in finite dimension

Constructs a preimage of an arbitrary operator by separately lifting its self-adjoint real and imaginary parts.

MathlibAnnex.Analysis.CStarAlgebra.Representation.surjective_of_irreducible_of_finiteDimensional

Immediate Card prerequisites: None in this selected scope

Used by in this scope: Compact-operator conclusion for the unital singleton condition

Scope

Cards in this route

Dependency-first reading route

Level 0 (9 Cards)

Full operator image in finite dimension

Singleton condition tested against all irreducible representations

A compact-operator model for a representation

An isolated point in a countable Baire space

Maximal abelian -subalgebras

Pure states as real extreme points

The preimage ideal of the compact operators

A character separating a closed ideal

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

A representative of the unique irreducible class

A pure state detects a nonzero square

A faithful singleton model forces simplicity

Level 3 (3 Cards)

Faithfulness from a unique irreducible class

A unital singleton model acts in finite dimension

A character becomes a joint unit eigenvector

Level 4 (4 Cards)

Compact-operator conclusion for the unital singleton condition

Finite-dimensional representation space in the unital singleton case

Finite-dimensional algebra in the unital singleton case

The full character space is countable

Level 5 (2 Cards)

An infinite-dimensional unital algebra has no separable singleton model

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

Every operator in a singleton image is compact

Compact operators lie in a singleton representation range

Level 9 (1 Card)

A singleton model is faithful and exactly compact-valued