∑math20

Operator algebras · Result 292

Kirchberg's \(\mathcal O_2\) norm-ultrapower embedding problem

1 paperLean

Constructs an explicit separable unital full group C∗-algebra that cannot embed unitally into the norm ultrapower of any fixed nonzero unital nuclear C∗-algebra, for any free ultrafilter on the natural numbers. Taking the target to be \(\mathcal O_2\) answers Kirchberg's norm-ultrapower embedding problem negatively.

Watch

1

The problem

What is being asked, where it comes from, and why it is hard. No proof needed.

▶Introduction to the problemin preparation
2

The solution proposed by OpenAI

How the paper solves it, step by step.

Full explanation
▶The proposed solutionin preparation

Papers 1

First page of An explicit obstruction to nuclear norm-ultrapower embeddings

An explicit obstruction to nuclear norm-ultrapower embeddings

OpenAI · September 23, 2026

We give a negative answer to Kirchberg's norm-ultrapower embedding problem. We construct an explicit separable unital full group C∗-algebra that admits no unital embedding into Bω, for any nonzero unital nuclear C∗-algebra B and any free ultrafilter ω on ℕ. In particular, it does not embed unitally into \(\mathcal O_2^\omega\).

Read PDF Download Source

Cite
@misc{OAI:An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026,
  author = {{OpenAI}},
  title = {{An explicit obstruction to nuclear norm-ultrapower embeddings}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026/paper.pdf}{OAI:An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-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

Kirchberg's norm-ultrapower embedding problem asks whether separable \(C^*\)-algebras embed into norm ultrapowers of nuclear algebras. The formalization constructs an explicit separable unital full group \(C^*\)-algebra that has no unital embedding into \(B^\omega\) for any nonzero unital nuclear \(C^*\)-algebra \(B\) and any free ultrafilter \(\omega\) on \(\mathbb N\). In particular, it does not embed unitally into an ultrapower of the Cuntz algebra \(\mathcal O_2\).

Comparator links

ResultComparator statement
Obstruction to nuclear norm-ultrapower embeddingsNuclearUltrapower.lean

Scope note on GitHub →