Back to Project mathematical routes
The preimage ideal of compact operators and a separating character exclude a noncompact represented image. The contradiction uses the same projection while forcing the character to take both zero and one.
7 direct Cards + 14 reused prerequisites = 21 unique Cards. This count is a selected Card closure, not a source-declaration count.
Route reading PDF · Preserved source exploration
Read this route with prerequisites
Direct references: R16 — The preimage ideal of the compact operators · R01 — Maximal abelian -subalgebras · R26 — A maximal abelian subalgebra containing a self-adjoint element · R06 — A character separating a closed ideal · R14 — A character becomes a joint unit eigenvector · R23 — A projection represented by a rank-one operator · R17 — Every operator in a singleton image is compact
Reused prerequisites: R04 — Every rank-one operator has an algebra preimage · 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 · 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 · 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
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.
No Cards match this search. Clear search to recover this reading scope.
Defines maximality by inclusion among commutative unital -subalgebras.
MathlibAnnex.Analysis.CStarAlgebra.IsMaximalAbelian
Immediate Card prerequisites: None in this selected scope
Used by in this scope: A maximal abelian subalgebra containing a self-adjoint element
Defines the two-sided ideal .
MathlibAnnex.CStarAlgebra.compactPreimageIdeal
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Every operator in a singleton image is compact
Finds one character which kills a closed ideal and detects a specified element outside it.
MathlibAnnex.Analysis.CStarAlgebra.exists_character_annihilating_closedIdeal_of_not_mem
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Every operator in a singleton image is compact
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
Defines purity inside the normalized positive state space.
MathlibAnnex.Analysis.CStarAlgebra.IsPureState
Immediate Card prerequisites: None in this selected scope
Used by in this scope: The GNS representation of a pure state is irreducible · A character extends to a pure state
Names -representations of a complex -algebra on a Hilbert space when no unit equation is required.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation
Immediate Card prerequisites: None in this selected scope
Used by in this scope: Nonzero irreducibility without a unit assumption · Unitary equivalence of two representations
Starts with the algebra generated by the given element and extends it by inclusion-maximality.
MathlibAnnex.Analysis.CStarAlgebra.exists_maximalAbelian_containing_isSelfAdjoint
Immediate Card prerequisites: Maximal abelian -subalgebras
Used by in this scope: A nonzero projection with scalar corner
Applies the cyclic pure-state criterion to the space and vector constructed from the same state.
MathlibAnnex.Analysis.CStarAlgebra.isIrreducible_pureState_gnsStarAlgHom
Immediate Card prerequisites: Pure states as real extreme points
Used by in this scope: Faithfulness from a unique irreducible class · A character becomes a joint unit eigenvector
Chooses an extreme state in the compact face of all extensions of one prescribed character.
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_extension
Immediate Card prerequisites: Pure states as real extreme points
Used by in this scope: A pure state detects a nonzero square · A character becomes a joint unit eigenvector
Defines equivalence by one surjective isometry intertwining all algebra actions.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.UnitaryEquivalent
Immediate Card prerequisites: Representations without a unit-preservation requirement
Used by in this scope: A representative of the unique irreducible class
Finds an isolated point in the open complement of the distinguished scalar character.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_isolated_character_ne_infinity
Immediate Card prerequisites: An isolated point in a countable Baire space
Used by in this scope: A nonzero projection with scalar corner
Requires nonzero action as well as the absence of proper closed reducing subspaces.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsIrreducible
Immediate Card prerequisites: Representations without a unit-preservation requirement
Used by in this scope: A representative of the unique irreducible class
Defines when one nonzero irreducible -representation represents the sole unitary-equivalence class of such representations.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.IsSingletonIrreducibleModel
Immediate Card prerequisites: Nonzero irreducibility without a unit assumption · Unitary equivalence of two representations
Used by in this scope: Faithfulness from a unique irreducible class · A character becomes a joint unit eigenvector
Detects a nonzero element through its positive square without an algebra separability assumption.
MathlibAnnex.Analysis.CStarAlgebra.exists_pureState_nonzero_on_star_mul_self
Immediate Card prerequisites: A character extends to a pure state
Used by in this scope: Faithfulness from a unique irreducible class
Transfers a normalized GNS eigenvector to the given representation through a unitary with a specified direction.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_unit_eigenvector_of_character_ne_infinity
Immediate Card prerequisites: A representative of the unique irreducible class · The GNS representation of a pure state is irreducible · A character extends to a pure state
Used by in this scope: The full character space is countable
Uses a pure state on the unitization to detect any hypothetical nonzero element of the kernel.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.injective_of_singleton
Immediate Card prerequisites: A representative of the unique irreducible class · A pure state detects a nonzero square · The GNS representation of a pure state is irreducible
Used by in this scope: A projection represented by a rank-one operator
Uses separated unit eigenvectors to count the non-scalar characters, then restores the one scalar character.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.countable_characterSpace_of_nonUnital_singleton
Immediate Card prerequisites: A character becomes a joint unit eigenvector
Used by in this scope: A nonzero projection with scalar corner
Constructs a projection in the original algebra from an isolated non-scalar character of a unitization subalgebra.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_scalar_corner
Immediate Card prerequisites: A maximal abelian subalgebra containing a self-adjoint element · An isolated character away from the scalar character · The full character space is countable
Used by in this scope: A projection represented by a rank-one operator
Obtains all projection, normalization, image and compactness conditions on the same witnesses.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_nonzero_projection_rankOne_map
Immediate Card prerequisites: Faithfulness from a unique irreducible class · A nonzero projection with scalar corner
Used by in this scope: Every rank-one operator has an algebra preimage
Turns one represented rank-one projection into every rank-one operator using dense orbits and a closed range.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.exists_preimage_rankOne_of_singleton
Immediate Card prerequisites: A projection represented by a rank-one operator
Used by in this scope: Every operator in a singleton image is compact
Excludes a noncompact image by making one separating character take both zero and one on the same projection.
MathlibAnnex.Analysis.CStarAlgebra.NonUnitalCStarRepresentation.isCompactOperator_map_of_singleton
Immediate Card prerequisites: Every rank-one operator has an algebra preimage · A character separating a closed ideal · The preimage ideal of the compact operators
Used by in this scope: None in this selected scope