Thomason structures: strict higher categories and stationary prisms

Source and verification

This article explains family 317 of the October 6, 2026 OpenAI collection. Research conclusions are attributed to its manuscripts. The review covers statements, introductions, and selected proof mechanisms; it is not an independent verification of the complete proofs.

Strict higher categories can encode the homotopy theory of spaces even when their positive-dimensional cells are not invertible. Family 317 claims a proper combinatorial model structure on small strict globular $n$-categories for every positive finite $n$ and for $n=\omega$. The central issue is controlling attachments to arbitrary categories: an attaching map may identify old objects and cells, creating new composites. (OpenAI, 2026)

🏷️ Preliminaries: strict cells, nerves, and model structures

A strict globular category has objects, arrows between objects, two-cells between parallel arrows, and successively higher cells with source and target. Composition, units, associativity, and interchange hold as literal equalities. A strict $n$-category has only identity cells above dimension $n$; an $\omega$-category permits all finite cell dimensions. No invertibility is imposed.

The Street nerve turns such a category $X$ into a simplicial set. Its $m$-simplices are strict functors from the oriental ${\mathcal{O}}_m$, the directed higher category generated by the faces and coherences of an $m$-simplex. Write $N_n$ for this nerve and $c_n$ for its left adjoint, which freely assembles orientals from a simplicial set.

A weak homotopy equivalence of simplicial sets is a map inducing the usual homotopy-group equivalences after realization. A Kan fibration has fillers for every horn lifting problem. The barycentric subdivision functor $\mathrm{Sd}$ has a right adjoint $\mathrm{Ex}$. The proposed adjunction is

$$\begin{array}{c}{L}_n=c_n{\mathrm{Sd}}^2,R_n={\mathrm{Ex}}^2{N}_n,\\ L_n⊣R_n.\end{array}$$

A model structure organizes weak equivalences together with cofibrations and fibrations. Every map has two compatible factorizations, and the associated lifting properties allow homotopy constructions. It is combinatorial when the underlying category is locally presentable and these factorizations are generated by sets of maps. It is proper when weak equivalences survive pushout along cofibrations and pullback along fibrations.

Manuscript's higher Thomason theorem

For every positive finite $n$ and for $n=\omega$, strict globular $n$-categories admit a proper combinatorial model structure with weak equivalences detected by $N_n$, fibrations detected by $R_n$, and a Quillen equivalence $L_n⊣R_n$ with simplicial sets. (OpenAI, 2026)

A Quillen equivalence says that the adjunction respects the model structures and presents the same homotopy theory after the appropriate replacements. The theorem supplies unrestricted model factorizations on all objects. It is stronger than identifying the homotopy category alone, and concerns globular categories rather than iterated internal, or $n$-fold, categories.

🏷️ The attachment problem and stationary cylinders

For a poset $E$, put $U_E=c_{n}N(E)$, using its ordinary nerve inside the categorification. A full subposet $A\subset E$ is a sieve if it is downward closed. Its inclusion has a right adjoint retraction $r$ when

$$\begin{array}{c}a\le e⟺a\le r(e),a\in A,\\ r{|}_A=\mathrm{id}.\end{array}$$

In particular $r(e)\le e$. The key claim is that, for every attaching functor $U_A\to X$, the map

$$X⟶X{⨿}_{U_A}{U}_E$$

is a Street-nerve weak equivalence. This property is called couniversality: the equivalence survives every pushout. The target $X$ need not be free or cofibrant, and the attaching map need not be injective.

A homotopy fixing the entire old subcategory is what permits this arbitrary attachment. The proof uses a right Gray cylinder $B\otimes D_1$, a directed higher-categorical interval construction. “Stationary on $U_A$” means equality with the constant cylinder on every old cell, not merely equality on objects or a homotopy between endpoint restrictions. Transposing through the right internal hom then glues it to the constant cylinder on $X$ by the pushout universal property.

🏷️ A positive prism with restricted hypotheses

Suppose monotone maps $f,g:E\to E$ satisfy $f\le g$, agree on the sieve $A$, and $g$ is constant on $E\setminus A$. For a normalized increasing tuple, define the interval component by

$$\begin{array}{rl}& [w_0,\dots ,w_p]\otimes u\\ & ⟼[f{w}_0,\dots ,f{w}_p,g{w}_p].\end{array}$$

The interval is the right tensor factor, with $du=e_1-e_0$. Repeated entries mean zero. Because the old vertices form a prefix and the new $g$-images are all equal, the output is an increasing tuple or zero, hence a positive chain rather than a signed formal combination of directed cells.

The chain identity reduces to a cancellation at the last two vertices. If the penultimate vertex is old, one term has a repetition and the other is the full $g$-image. If it is new, the last two $g$-images coincide. Both cases give the required difference of endpoint chains with the tensor differential sign $(-1{)}^p$.

The formula also respects degeneracies: a repeated selected index creates a repeated image in every endpoint or interval tuple. Thus it is compatible with all simplex operators, not only face maps. The directed-chain comparison turns these whole chain maps into strict cylinders. On the old sieve, the whole chain map factors through the interval augmentation, including its lower boundary data. The repeated-entry calculation supplies this full factorization; a zero top chain alone would not establish stationarity, since it could still be an identity on a nonidentity lower cell. The construction descends to finite $n$ by the appropriate reflection and internal-hom compatibility. (OpenAI, 2026)

The constancy hypothesis on the upper map is essential to this explicit formula. The source does not assert that every order homotopy automatically supplies such a stationary strict cylinder.

🏷️ Local contractions and gluing without compatible choices

Suppose $E\setminus A$ has greatest element $x$, and put $t=r(x)$. Define $k$ to fix $A$ and send every new element to $t$; define $g$ to fix $A$ and send every new element to $x$. Then

$${\mathrm{id}}_E\le g,k\le g.$$

The maps $k$ and the identity need not be comparable. The two prisms supply a zigzag of cylinders, stationary on $A$. After attaching, $k$ factors through a retraction onto $X$, and the zigzag proves a homotopy equivalence of realized nerves. Reversing one ordinary realized homotopy is legitimate; no reversed directed Gray cylinder is claimed.

For finite $E$ without a greatest new element, delete two distinct maximal new elements separately. The two resulting subposets are sieves covering $E$, and their intersection has a smaller new part. Induction applies to their attachments to the same $X$.

One must still identify these pieces inside the actual categorical pushout. Labels to the interval category do this: zero-fibers are full sieves, one-fibers are full cosieves, and the fiber construction preserves the relevant pushout. Maximum and minimum of two labels identify intersections. The object set is the old object set of $X$ together with the new elements of $E\setminus A$, even when the attaching map identifies old objects.

The nerves of a two-sieve cover form an ordinary simplicial pushout. An oriental simplex belongs to any sieve containing its last vertex, because it has arrows from every earlier vertex to the last. For cosieves use the first vertex instead. Fullness includes all higher cells, so this is a cover of whole simplices.

The gluing legs are monomorphisms. Simplicial homotopy gluing therefore combines the local weak equivalences; it does not require the independently chosen contractions to agree on intersections.

For arbitrary $E$, use finite full subsets stable under $ir$. Any finite subset $T$ is contained in $T\cup ir(T)$, so these subsets form a filtered system. Their attachments all retain the same fixed copy of $X$. Street nerve and weak equivalences preserve this filtered colimit without requiring injective transition maps. This completes couniversality.

🏷️ Why two subdivisions enter

Take a generating boundary or horn inclusion $K\hookrightarrow \Delta [m]$. Let $P$ be the poset of nonempty faces of the simplex, and $P_K$ the faces lying in $K$. Two subdivisions give the nerve of a poset $B$ of nonempty chains in $P$. The subposet $A$ consists of chains lying entirely in $P_K$ and is a sieve.

Its upward closure is

$$Z=\{\sigma \in B:\sigma \cap P_K\ne \varnothing \}.$$

The right adjoint retraction is the explicit intersection $r(\sigma )=\sigma \cap P_K$. For a boundary, remove the full face from $P$; for a horn, remove the full face and its missing facet. The zero-dimensional boundary has $A=Z=\varnothing$ and causes no exception to the argument. There is no zero-dimensional horn generator.

Couniversality handles the attachment over $Z$. To include the rest of $B$, use the cosieve cover by $Z$ and $C=B\setminus A$, with intersection $T=Z\setminus A$. This yields a canonical comparison

$$\begin{array}{c}{N}_{n}X{⨿}_{N_n{U}_A}{N}_n{U}_B\\ ⟶N_n(X{⨿}_{U_A}{U}_B)\end{array}$$

that is a weak equivalence for every attaching functor. In the final gluing, the specific monomorphic leg is $N_n{U}_T\hookrightarrow N_n{U}_C$. The map from $N_n{U}_A$ into $N_{n}X$ may identify simplices and is not assumed monic.

For horns this proves that every categorical horn attachment is weakly equivalent to its target. For boundaries it proves that an existing weak equivalence stays a weak equivalence after corresponding attachments. These are distinct inputs for factorization and left properness.

🏷️ Model axioms, properness, and the actual unit

Let $I$ be the simplicial boundary inclusions and $J$ the horn inclusions. Adjunction identifies maps lifting against $L_{n}I$ with trivial fibrations, and maps lifting against $L_{n}J$ with fibrations. Local presentability allows the small-object construction: attach all required lifting cells, iterate through a sufficiently long regular ordinal, and take colimits.

Filtered-colimit preservation handles limit stages. Relative horn-cell maps are weak equivalences, so retract and lifting arguments give both model factorizations for arbitrary source objects. In the $\omega$ case there are countably many cell sorts, but every operation, matching-boundary condition, and equation uses finite data. Finite orientals therefore still have the necessary smallness.

Right properness follows by applying the right adjoint to pullbacks and using simplicial right properness. Left properness follows first through boundary attachments and then through retracts with their source fixed, so that cobase change preserves the retract diagram. No cofibrancy restriction on the base object is inserted.

Finally, the poset unit is extended to every simplicial set by its simplex-attachment presentation. Only each generating simplex and boundary needs the poset description; a general twice-subdivided simplicial set is not assumed to be a poset nerve. Attaching maps can identify faces or send them to degenerate simplices. The comparison above and gluing with one specified monomorphic leg still prove the canonical map

$${\mathrm{Sd}}^{2}K⟶N_n{L}_{n}K$$

weakly equivalent for every $K$. Combining this with the subdivision–extension unit proves that the actual composite unit $K\to R_n{L}_{n}K$ is a weak equivalence. Naturality and two-out-of-three then establish the Quillen-equivalence criterion.

The scope page describes a Lean formalization of the main model-structure and nerve-detection statements in all these dimensions. This exposition audits selected manuscript constructions and their interfaces; it does not certify that formalization or independently rebuild the directed-chain and presentability foundations.

🏷️ Related posts

• The homotopy hypothesis via elementary expansions concerns weak groupoids and a semi-model structure with cofibrant-domain restrictions. Its joining-cell tests do not transfer directly to Street weak equivalences in directed strict categories; the present proof supplies stationary prisms and unrestricted attachments independently.

🏷️ Key steps and proof outlines

Labels remain valid after an attaching map identifies cells

The proof cannot compute an algebraic pushout by pretending that it is a union of its original pieces. An attaching functor may identify two old objects or turn an old arrow into an identity. The manuscript instead labels the entire pushout by the interval category $D_1$.

Suppose a poset map $\lambda :P\to [1]$ and a functor $\xi :X\to D_1$ agree on the attaching source $U_A$. They then induce a label on

$$Y=X{⨿}_{U_A}{U}_P.$$

The fiber lemma computes the actual full subcategory of label $ϵ$ as

$$Y_{ϵ}\cong X_{ϵ}{⨿}_{U_{A_{ϵ}}}{U}_{P_{ϵ}}.$$

The proof takes the pushout in the category of objects over $D_1$ and applies the fiber functor, whose colimit property is established earlier. This includes all composites and identifications generated by the attachment. On objects, the result is particularly transparent: objects of $A$ are replaced by their images in $X$, while objects of $P\setminus A$ remain distinct new objects.

Two labels also compute intersections. The zero-fiber of their maximum is the intersection of their zero-fibers; the one-fiber of their minimum is the intersection of their one-fibers. Thus sieve and cosieve covers, and their intersections, can be tracked through the pushout exactly. No injectivity of the attaching functor is required. (OpenAI, 2026)

Full sieve covers become genuine simplicial unions

Suppose full sieves $C_1,C_2$ cover the objects of $C$. Consider a Street-nerve simplex, a functor $z:{\mathcal{O}}_m\to C$. Choose a piece containing its final vertex $z(m)$. Every earlier vertex has an arrow to $z(m)$ in the oriental, so downward closure puts all the vertices in that same piece. Fullness then puts all higher cells of the simplex there too.

Consequently every simplex belongs to one piece, and

$$N_{n}C=N_n{C}_1{\cup }_{N_n(C_1\cap C_2)}{N}_n{C}_2.$$

The inclusions are monomorphisms of simplicial sets, so this ordinary union is also the required homotopy pushout. For cosieves, the same proof starts from the first vertex. The argument would fail for arbitrary full subcategories: a simplex could travel between the pieces.

Induction glues equivalences without gluing their chosen homotopies

For a finite poset $E$ with sieve $A$ and right-adjoint retraction, the explicit stationary prism handles the case where $E\setminus A$ has a greatest element. Otherwise choose two distinct maximal new elements $x_1,x_2$. The subposets obtained by deleting $x_1$, by deleting $x_2$, and by deleting both all retain the retraction and have fewer new elements.

Induction gives weak equivalences after attachment on those three pieces. The label calculation identifies their actual intersections, and the nerve-cover lemma expresses the full target as their simplicial union. The canonical maps from $X$ form a strictly commuting map of spans; homotopy-pushout invariance gives the desired equivalence on the union.

The local contraction homotopies need not agree on overlaps. Only the canonical maps in the spans must agree, which they do by construction. This distinction lets the proof use convenient local prisms without claiming a globally compatible family of such choices.

For an infinite poset, put $q=ir$, the idempotent endomorphism defined by the retraction. Every finite subset $T$ lies in the finite stable subset $T\cup q(T)$. These stable subsets form a filtered system. Apply the finite theorem to each while keeping the same attaching target $X$. Their pushouts have colimit $Y$ by the universal property. Preservation of filtered colimits by the nerve and closure of simplicial weak equivalences finish the passage to arbitrary $E$.

Why horn acyclicity yields a full model structure

The subdivision argument applies the attachment theorem to generating horns, with arbitrary targets. A transfinite succession of these attachments is still a weak equivalence: use composition at successor stages and filtered-colimit closure on the arrows from the fixed initial source at limit stages.

The small-object argument then factors every map using generating boundaries, and again using generating horns. Let $\mathcal{D}$ be the retract closure of relative horn-cell maps. Horn acyclicity gives $\mathcal{D}\subseteq C_n\cap W_n$.

For the reverse inclusion, factor a cofibration and weak equivalence $u$ as $u=pi$, with $i\in \mathcal{D}$ and $p$ a fibration. Since both $u$ and $i$ are weak equivalences, so is $p$. The lifting property of $u$ against this trivial fibration supplies a section exhibiting $u$ as a retract of $i$. Thus $\mathcal{D}=C_n\cap W_n$, giving the second weak factorization system. The arbitrary-target hypothesis is what allows these factorizations for every source, rather than only for sources already known to be cofibrant.

🏷️ Manuscripts and verification scope

• Thomason Model Structures in Every Strict Higher Dimension — pinned manuscript and companion source.

The family scope page describes selected formalization coverage. The page claims formal coverage of the proper combinatorial structures and Quillen equivalences in every positive finite dimension and omega. This is a statement of documented scope, not an independently checked Lean certification. No Lean build, axiom audit, or manuscript-to-formal-statement equivalence check was performed for these notes.

OpenAI collection provides prerequisites and the reading sequence; coverage register records completed and pending families.

🐻  OpenAI 2026. Thomason Model Structures in Every Strict Higher Dimension.