Framed combinatorial topology is a new research programme that unifies ideas from higher-dimensional algebra, stratified geometry, and combinatorial topology. Relevant ideas that appear as part of this unification include:
Higher-dimensional algebra and category theory: pasting diagrams, duality of cell and string diagrams, manifold diagrams, constructive approaches to the cobordism hypothesis, categorical coherences as manifold isotopies (e.g., naturality law = braid)
Stratified geometry: stratified bordisms, stratified Thom-Pontryagin constructions, a new approach differential singularities, higher-dimensional Morse theory, combinatorial classification of (stratified) smooth structures.
Combinatorial topology: recognition problem of combinatorial spheres and manifolds, taming the Hauptvermutung,
Diagrammatic mathematics deals with the applications of these ideas to related areas of mathematics. In particular, we obtain:
Diagrammatic higher categories. This uses manifold diagrams as a basis to define the compositional structure of higher-dimensional categories.
Diagrammatic (higher) observational type theory. This uses that framed cellular spaces are great model of “higher directed inductive types”.
Diagrammatic (geometric) topology. This studies higher knots, manifolds, and their singularities through the lens of tame tangles and manifold diagrams.
On this page we collect references on the subject. Please let me know if you think something is missing.
We define novel fully combinatorial models of higher categories. Our definitions are based on a connection of higher categories to “directed spaces”. Directed spaces will be locally modelled on manifold diagrams, which are stratifications of the $n$-cube such that strata are transversal to the flag foliation of the n-cube. The first part of this thesis develops a combinatorial language for manifold diagrams called singular n-cubes. In the second part we apply this language to build our notions of higher categories.
Singular n-cubes can be thought of as “flag-foliation-compatible” stratifications of the n-cube, such that strata are “stable” under projections from the $(k + 1)$- to the $k$-cube, together with a functorial assignment of data to strata. The definition of singular n-cubes is inductive, with $(n + 1)$-cubes being defined as combinatorial bundles of n-cubes over the (stratified) interval. The combinatorial structure of singular n-cubes can be naturally organised into two categories: $\mathbf{SI}//^n_C$, whose morphisms are bundles themselves, and $\mathbf{Cube}^n_C$, whose morphisms are inductively defined as base changes of bundles. The former category is used for the inductive construction of singular n-cubes. The latter category describes the following interactions of these cubes. There is a subcategory of “open” base changes, which topologically correspond to open maps of bundles. We show this subcategory admits an (epi,mono) factorisation system. Monomorphism will be called embeddings and describe how cubes can be embedded in one another such that strata are preserved. Epimorphisms will be called collapses and describe how strata can be can be refined. Two cubes are equivalent if there is a cube that they both refine. We prove that each “equivalence class” (that is, the connected component of the subcategory generated by epimorphisms) has a terminal object, called the collapse normal form. Geometrically speaking the existence of collapse normal forms translates into saying that any combinatorially represented manifold diagram has a unique coarsest stratification, making the equality relation between manifold diagrams decidable and computer implementable.
As the main application of the resulting combinatorial framework for manifold diagrams, we give algebraic definitions of various notions of higher categories. In particular, we define associative n-categories, presented associative n-categories and presented associative n-groupoids. The first depends on a theory of sets, while the latter two do not, making them a step towards a framework for working with general higher categories in a foundation- independent way. All three notions will have strict units and associators. The only “weak” coherences which are present will be called homotopies. We propose that this is the right conceptual categorisation of coherence data: homotopies are essential coherences, while all other coherences can be uniformly derived from them. As evidence to this claim we define presented weak n-categories, and develop a mechanism for recovering the usual coherence data of weak n-categories, such as associators and pentagonators and their higher analogues. This motivates the conjecture that the theory of associative higher categories is equivalent to its fully weak counterpart.
Executive summary
This thesis works towards a combinatorial notion of manifold diagrams by introducing the novel combinatorial structure of singular \(n\)-cubes labeled in \(\mathsf{C}\) (these are now, in more general form, called “\(n\)-trusses [labeled] in \(\mathsf{C}\)”). Based on a combinatorial definition of manifold diagrams (N.B: no real attempt is made at formalizing manifold diagrams in geometric terms), the thesis goes on to define combinatorial models of both free and non-free higher categories. It also sketches a path towards the categorical study of singularities and the Pontryagin-Thom construction. However, it certainly stops short of giving a full account of these ideas (in particular, it does not compare either notion to other models of higher categories).
[2] “High-level methods for homotopy construction in associative \(n\)-categories”, 2019, David Reutter & Jamie Vicary
A combinatorial theory of associative $n$-categories has recently been proposed, with strictly associative and unital composition in all dimensions, and the weak structure arising as a combinatorial notion of homotopy with a natural geometrical interpretation. Such a theory has the potential to serve as an attractive foundation for a computer proof assistant for higher category theory, since it allows composites to be uniquely described, and relieves proofs from the bureaucracy of associators, unitors and their coherence. However, this basic theory lacks a high-level way to construct homotopies, which would be intractable to build directly in complex situations; it is not therefore immediately amenable to implementation. We tackle this problem by describing a contraction operation, which algorithmically constructs complex homotopies that reduce the lengths of composite terms. This contraction procedure allows building of nontrivial proofs by repeatedly contracting subterms, and also allows the contraction of those proofs themselves, yielding in some cases single-step witnesses for complex homotopies. We prove correctness of this procedure by showing that it lifts connected colimits from a base category to a category of zigzags, a procedure which is then iterated to yield a contraction mechanism in any dimension. We also present homotopy.io, an online proof assistant that implements the theory of associative $n$-categories, and use it to construct a range of examples that illustrate this new contraction mechanism.
Summary and comments
This paper takes first steps towards a computer implementation of the idea of associative \(n\)-categories respectively combinatorial manifold diagrams as discussed in thesis, focusing in particular on the algorithmic construction of isotopies via a notion of “contractions”. Note this contraction underlie how the user interacts with the proof assistant homotopy.io.
Note that “singular \(n\)-cubes in \(\mathsf{C}\)” are called “\(n\)-iterated zigzags in \(\mathsf{C}\)” and the definition is slightly reworked from that in thesis (the resulting structures are the same).
fixed a few (of many) inaccuracies, added and improved material (most importantly, added “bundle” generalizations of some central results in Ch. 4 and 5)
Framed combinatorial topology is a novel theory describing combinatorial phenomena arising at the intersection of stratified topology, singularity theory, and higher algebra. The theory synthesizes elements of classical combinatorial topology with a new combinatorial approach to framings. The resulting notion of framed combinatorial spaces has unexpectedly good behavior when compared to classical, nonframed combinatorial notions of space. In discussing this behavior and its contrast with that of classical structures, we emphasize two broad themes, computability in combinatorial topology and combinatorializability of topological phenomena. The first theme of computability concerns whether certain combinatorial structures can be algorithmically recognized and classified. The second theme of combinatorializability concerns whether certain topological structures can be faithfully represented by a discrete structure. Combining these themes, we will find that in the context of framed combinatorial topology we can overcome a set of fundamental classical obstructions to the computable combinatorial representation of topological phenomena.
[4] “Zigzag normalisation for associative $n$-categories”, 2022, Lukas Heidemann, David Reutter & Jamie Vicary
The theory of associative n-categories has recently been proposed as a strictly associative and unital approach to higher category theory. As a foundation for a proof assistant, this is potentially attractive, since it has the potential to allow simple formal proofs of complex high-dimensional algebraic phenomena. However, the theory relies on an implicit term normalisation procedure to recognize correct composites, with no recursive method available for computing it. Here we describe a new approach to term normalisation in associative n-categories, based on the categorical zigzag construction. This radically simplifies the theory, and yields a recursive algorithm for normalisation, which we prove is correct. Our use of categorical lifting properties allows us to give efficient proofs of our results. This normalisation algorithm forms a core component of the proof assistant homotopy.io, and we illustrate our scheme with worked examples.
Diagrammatic notation has become a ubiquitous computational tool; early examples include Penrose’s graphical notation for tensor calculus, Feynman’s diagrams for perturbative quantum field theory, and Cvitanovic’s birdtracks for Lie algebras. Category theory provides a robust framework in which to understand the nature of such diagrams, and Joyal and Street formalized this framework by introducing string diagrams, governed by the syntax of monoidal 1-categories. The notion of “manifold diagrams” generalizes string diagrams to higher dimensions, and can be interpreted in higher-categorical terms by a process of geometric dualization. The closely related notion of “tame tangles” describes a well-behaved class of embedded manifolds that can likewise be interpreted categorically. In this paper we formally introduce the notions of manifold diagrams and of tame tangles, and show that they admit a combinatorial classification, by using results from the toolbox of framed combinatorial topology. We then study the stability of tame tangles under perturbation; the local forms of perturbation stable tame tangles provide combinatorial models of differential singularities. As an illustration we describe various such combinatorial singularities in low dimensions. We conclude by observing that all smooth 4-manifolds can be presented as tame tangles, and conjecture that the same is true for smooth manifolds of any dimension.
The goal of this article is to introduce basic concepts in the emerging area of diagrammatic higher category theory. The exposition aims to be brief and informative but mathematically as self-contained as possible (some familiarity with higher category theory is presumed). Several small exercises (with solutions) have been included, and plenty of open questions as well as future research directions in the area are discussed.
While this essentially summarizes many (but not all) ideas from the list of notes below, the notes are written at a more introductory level (without presuming much about your knowledge of higher categories). Note, the notes are written sequentially (with later notes often referring to earlier ones). The focus is mainly on intuition and brevity, and less on mathematical formality; however, some mathematical substance can nonetheless be found: to indicate this notes are rated with a “formality level” (FL) below.
A note on framed computadic and regular cells, explaining the classical problem of defining universal classes of shapes and how to resolve it. (FL 1/5)
A note on manifold diagrams, the dual notion of pasting diagrams of framed computadic cells, introduced via a geometric approach. (FL 2/5)
A note on the basic combinatorial theory of trusses, leading up to formal defintion of manifold-diagrammatic computads, as well as combinatorial defintions of (combinatorial) manifold and pasting diagrams. (FL 4/5)
A note on the the formalization of the categorical Pontryagin-Thom construction, relating functors of manifold-diagrammatic computads to stratifications on them, and discussing how this should lead to a “combinatorialization” of smooth manifolds and cobordisms. (FL 3/5)
See also
The following further material may be helpful to look at:
