∑math20

Topology · Result 317

Thomason model structures in all strict higher dimensions

1 paperLean

Resolves the Ara–Maltsiniotis conjecture: for every n ≥ 1 and n = ω, small strict globular n-categories admit proper combinatorial Thomason model structures Quillen equivalent to simplicial sets. Thus strict higher categories model the homotopy theory of spaces in every stated dimension.

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 Thomason Model Structures in Every Strict Higher Dimension

Thomason Model Structures in Every Strict Higher Dimension

OpenAI · September 25, 2026

We prove the higher-dimensional Thomason model-structure conjecture of Ara and Maltsiniotis. For every \(1\le n\le\infty\), the category of small strict globular n-categories admits a proper combinatorial model structure that is Quillen equivalent to simplicial sets. Its weak equivalences and fibrations are detected by the twice-extended Street nerve \(\mathrm{Ex}^2N_n\), and the Quillen equivalence is given by \(c_n\mathrm{Sd}^2\dashv\mathrm{Ex}^2N_n\). Thus strict higher categories model the homotopy theory of spaces in every positive finite dimension and in dimension ω.

Read PDF Download Source

Cite
@misc{OAI:Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026,
  author = {{OpenAI}},
  title = {{Thomason Model Structures in Every Strict Higher Dimension}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-September-25-2026/paper.pdf}{OAI:Thomason-Model-Structures-in-Every-Strict-Higher-Dimension-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 the higher-dimensional Thomason model-structure theorem for small strict globular \(n\)-categories in every positive finite dimension and in dimension \(\omega\). Each category has the stated proper combinatorial model structure, Quillen equivalent to simplicial sets through the twice-subdivided categorification and twice-extended Street nerve adjunction.

The selected statements also identify weak equivalences by the Street nerve in all these dimensions. Thus the constructions model the homotopy theory of spaces throughout the stated range.

Comparator links

ResultComparator statement
Thomason model structures and nerve detection in all positive strict dimensionsThomasonModelStructures.lean

Scope note on GitHub →