we-solve (beta)

Math-3028 · mathematics · Topology

Thomason structures in all strict categorical dimensions

Status OpenLLM status Open unverified

Statement

Definitions and mathematical statement

Statement recorded in the supplied source.
For every positive finite n and for strict infinity-categories, does the Thomason adjunction $c_n$ $Sd^{2}$ $\dashv $ $Ex^{2}$ $N_n$ supply a proper combinatorial model structure on strict n-categories with weak equivalences detected by the nerve, and a Quillen equivalence with the Kan–Quillen model category of simplicial sets?

Short English statement

For every positive finite n and for strict infinity-categories, does the Thomason adjunction $c_n$ $Sd^{2}$ $\dashv $ $Ex^{2}$ $N_n$ supply a proper combinatorial model structure on strict n-categories with weak equivalences detected by the nerve, and a Quillen equivalence with the Kan–Quillen model category of simplicial sets?

Sources

Statement licence: CC-BY-4.0 · Source file

Contributions 1

Math-3028-A1 · Literature report · LLM-generated · unknown ·

OpenAI claim summary for Math-3028

Manuscript 1 (family 317, 2026-09-25): The problem selects the mathematical statement summarized here, including its stated hypotheses and parameter range. The cited theorem gives a claimed proof of that assertion in full.

Thomason structures in all strict categorical dimensions

OpenAI's claim

Strict globular n-categories are claimed to admit proper combinatorial Thomason model structures for every positive finite n and n=infinity, Quillen equivalent to spaces with fibrations detected by $\operatorname{Ex}^2$ of the Street nerve. The cited manuscript argues for that result; its relation to this problem is specified below.

Mathematical statement of the claimed result

Mathematical claim 1.
For every positive integer $n$ and $n=\infty$, let $n\mathrm{Cat}$ be strict higher categories and $N_nX$ the Street nerve with simplices $\operatorname{Hom}(\mathcal O_m,X)$ from orientals. Let $c_n$ be its left adjoint and set $L_n=c_n\operatorname{Sd}^2$, $R_n=\operatorname{Ex}^2N_n$. OpenAI claims a proper combinatorial cofibrantly generated model structure with \[ W_n=R_n^{-1}(\text{weak homotopy equivalences}),\quad F_n=R_n^{-1}(\text{Kan fibrations}),\quad C_n={}^{\perp}(F_n\cap W_n). \] The generators are $L_n(\partial\Delta[m]\hookrightarrow\Delta[m])$ and $L_n(\Lambda^k[m]\hookrightarrow\Delta[m])$, and $L_n\dashv R_n$ is a Quillen equivalence with Kan--Quillen simplicial sets. Here left orthogonality is the lifting property, and subdivision and extension are the usual simplicial functors.

Outline of the argument

Manuscript 1 (family 317, 2026-09-25): Positive-chain prisms construct strict Gray cylinders that remain stationary on old cells during arbitrary attachments. Relative cover and sieve calculations compare categorical pushouts with nerve pushouts, supplying the transfer condition without assuming a free target. Finite orientals control the infinite-dimensional case, while reflection and smallness arguments give the model axioms and properness in each finite dimension.

Formal verification

For family 317, the scope page documents the following selections. The selections give Thomason model structures for every positive finite strict dimension and dimension omega, with Street-nerve detection and the stated Quillen comparison to simplicial sets. The documented statement covers the main claim of manuscript 1. Its selected declaration also covers the clause used for this problem. Comparator files: ThomasonModelStructures.lean. Declarations: OAI.Thomason.main, OAI.Thomason.nerveDetection_allDimensions.

This site has not executed the Lean files or checked their dependencies. These descriptions report the scope of the linked declarations, rather than a new verification of the proofs.

Status caveat

OpenAI attributes these results to an internal model. Its release notice cautions that results lacking full formalization can contain mistakes. This site has not independently assessed the proofs; a solved label records the scope of the reported claim.

Sources

Go to contribution →