∑math20

Operator algebras · Result 303

Weak pure infiniteness and Cuntz-algebra absorption

1 paperLean

Resolves the ordinary-to-strong pure-infiniteness question of Kirchberg and Rørdam for complex C∗-algebras. For exact algebras, proper infiniteness of one fixed finite amplification of every positive element also suffices. Consequently, every separable nuclear algebra with this property absorbs \(\mathcal O_\infty\), without unitality or simplicity assumptions.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 1

First page of Weak pure infiniteness and O-infinity absorption

Weak pure infiniteness and O-infinity absorption

OpenAI · September 25, 2026

We prove that every complex C∗-algebra in which each positive element is properly infinite is strongly purely infinite. This answers the ordinary-to-strong part of Kirchberg–Rørdam's comparison question. For exact algebras, we also prove that proper infiniteness of one fixed finite amplification of every positive element implies proper infiniteness of each positive element. Consequently, every separable nuclear algebra with this fixed-amplification property absorbs \(\mathcal O_\infty\), without assumptions of unitality or simplicity.

Read PDF Download Source

Cite
@misc{OAI:Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026,
  author = {{OpenAI}},
  title = {{Weak pure infiniteness and $\mathcal{O}_{\infty}$ absorption}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026/paper.pdf}{OAI:Weak-pure-infiniteness-and-O-infinity-absorption-September-25-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalization proves that a complex \(C^*\)-algebra in which every positive element is properly infinite is strongly purely infinite, with the full positive-element diagonalization property. No exactness, nuclearity, unitality, or simplicity assumption is needed for this implication.

For exact algebras, proper infiniteness of one fixed finite amplification of every positive element already implies individual proper infiniteness and strong pure infiniteness.

Comparator links

ResultComparator statement
Fixed-amplification pure infiniteness for exact algebrasExactInfiniteness.lean
Individual proper infiniteness implies strong pure infinitenessIndividualStrongInfiniteness.lean

Scope note on GitHub →