∑math20

Operator algebras · Result 299

The Kirchberg–Rørdam character criterion and infinite tensor-power Jiang–Su stability

1 paperLean

A nonzero unital separable complex C∗-algebra is Jiang–Su stable exactly when its norm central-sequence algebra has no characters, for every free ultrafilter. This answers the Kirchberg–Rørdam character question. Also, the infinite minimal tensor power of every such algebra without characters is Jiang–Su stable, answering the Dadarlat–Toms question.

Watch

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

Papers 1

First page of The Kirchberg–Rørdam character criterion

The Kirchberg–Rørdam character criterion

OpenAI · September 25, 2026

We prove the Kirchberg–Rørdam character criterion: for every free ultrafilter on ℕ, a nonzero unital separable complex C∗-algebra absorbs the Jiang–Su algebra if and only if its norm central-sequence algebra has no characters. We also prove that the infinite minimal tensor power of every nonzero unital separable complex C∗-algebra without characters is \(\mathcal Z\)-stable and contains a unital copy of \(\mathcal Z\).

Read PDF Download Source

Cite
@misc{OAI:The-Kirchberg-Rordam-character-criterion-September-25-2026,
  author = {{OpenAI}},
  title = {{The Kirchberg--R\o rdam character criterion}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-Kirchberg-Rordam-character-criterion-September-25-2026/paper.pdf}{OAI:The-Kirchberg-Rordam-character-criterion-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 Kirchberg–Rørdam criterion relates Jiang–Su absorption to characters of the central-sequence algebra. The formalized result proves that, for every nonzero unital separable complex \(C^*\)-algebra \(A\) and every free ultrafilter on \(\mathbb N\), the norm central-sequence algebra has no nonzero character exactly when \(A\cong A\otimes_{\min}\mathcal Z\). No nuclearity, simplicity, trace, or comparison hypothesis is imposed.

Comparator links

ResultComparator statement
Kirchberg–Rørdam character criterionCharacterCriterion.lean

Scope note on GitHub →