MathlibAnnex.CStarAlgebra.CAR.isSimpleCStarAlgebra_shellFamilyTarget
Uses a faithful irreducible representation in the unique unitary-equivalence class to rule out proper nonzero closed two-sided ideals.
Statement
For the fixed algebra
Assumptions
Let
Index chosen pure-state Gelfand-Naimark-Segal (GNS) representations by their unitary-equivalence classes
A fixed shell family consists of complex-linear unital star automorphisms
At the root,
Let
Choose once a family of unitary operators
Put
The ideals in this assertion are two-sided algebraic ideals whose underlying sets are norm closed. The family is supplied as input. The shell-model realization theorem provides the faithful source representation and irreducible inclusion; the universal capture theorem identifies every irreducible class with that inclusion.
Conclusion
The conclusion is simplicity with respect to closed two-sided ideals. It is not a claim that every algebraic ideal, with no closure hypothesis, is trivial.
Proof route
Let
Proof steps
If
there is nothing to prove. Otherwise use a pure GNS representation with for every . Choose the unitary
from the faithful inclusion to . For , for all . Injectivity of
gives ; injectivity of gives . Nonzeroness of follows from its embedded copy of .
Main citations
- Exact declaration and proof · Exact source
- MathlibAnnex.CStarAlgebra.CAR.RepresentativeShellFamily · Exact source
- MathlibAnnex.CStarAlgebra.CAR.exists_completedAtomicShellModel · Exact source
- MathlibAnnex.CStarAlgebra.CAR.isUniqueIrreducibleModel_shellFamilyInclusion · Exact source
- MathlibAnnex.CStarAlgebra.CAR.shellFamilySourceHom_injective · Exact source
- MathlibAnnex.CStarAlgebra.isSimpleCStarAlgebra_of_uniqueIrreducibleModel · Exact source
Lean source signature (exact)
theorem isSimpleCStarAlgebra_shellFamilyTarget (family : RepresentativeShellFamily) :
MathlibAnnex.CStarAlgebra.IsSimpleCStarAlgebra (ShellFamilyTarget family)Here ShellFamilyTarget family is IsSimpleCStarAlgebra means that
Read exact source with highlighted declaration · Raw UTF-8 source · Card PDF
Lean realization notes
The proof uses capture for the Hilbert spaces of canonical pure GNS representations, which lie in the source-algebra universe. The stronger universe-polymorphic capture result supplies this case. Faithfulness is essential: uniqueness of an irreducible class without a faithful representation would not justify this argument.
Exact Card identity
Language: en
CARD_CONTENT_COMPLETE
Card UID: lfh:lfh-declaration-card:sha256:2f74196f22042b6e02ddfbd323ee500f1cd0f3bc297f30b91ccaed55116f7c26
Card revision: 1 · SHA-256: 12b80e1f736ab61c746ad43545eeac483af19f4bccd6ea10d04993b56aef591b
Exposition revision: 1 · SHA-256: 005b0ef073045c52c392495d5e4a3ee8cd3df099dfa9b8d3e4a9c7911e96ad05
Source commit: 437e6e46228bbb8e91211ebded349d7a30020e73
Header SHA-256: 11ce02f9ecd62e77a48900b052502494bc3255c31ea40339b246ccee1f615d77