# Kirchberg's $`\mathcal O_2`$ norm-ultrapower embedding problem

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

- [An explicit obstruction to nuclear norm-ultrapower embeddings](../../preprints/An-explicit-obstruction-to-nuclear-norm-ultrapower-embeddings-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Obstruction to nuclear norm-ultrapower embeddings | [NuclearUltrapower.lean](../ComparatorChallenges/NuclearUltrapower.lean) |