nLab regular directed complex

Contents

Contents

Idea

The notion of regular directed complex, introduced by Hadzihasanovic, is a notion of pasting diagram shape. There, a pasting diagram is encoded as a kind of “directed cell complex”, that is, a cell complex together with an orientation on each cell, which divides its boundary into two halves: an input half and an output half.

Definition

In this framework, a pasting diagram will be encoded as an oriented graded poset (Def. ), which is a poset, whose covering diagram is graded, and each edge possess an orientation. To see this consider the following pasting diagram (referred in this page as the running pasting diagram) and the covering diagram associated to it

Basic order theory

Of course, not all oriented graded posets will lead to a well-formed pasting diagrams: before defining the one that will count, we introduce some terminology.

Definition

(oriented graded poset)
A graded poset is a poset together with a rank function dim:P\dim \colon P \to \mathbb{N} such that

  • if x<yx \lt y, then dimx<dimy\dim x \lt \dim y,
  • if xx covers yy, then dimx=dimy+1\dim x = \dim y + 1.
  • if xx covers no element, then dimx=0\dim x = 0.

An oriented graded poset is a graded poset together with a sign α{,+}\alpha \in \{ -, + \} for each edge in its covering diagram.

Remark

The grading function of an oriented graded poset defines a notion of dimension of an element. For instance, in the running pasting diagram, the dimensions of x,f,sx, f, s are repectively 0,1,20, 1, 2. If PP is an oriented graded poset, we write P nP_n for its elements of dimension nn. We speak also of the dimension of an oriented graded poset to mean the maximal of the dimension of its elements.

Definition

(faces and cofaces)
Let PP be an oriented graded poset. For all xx in PP, and α=\alpha = - (resp. α=+\alpha = +), we define the input (resp. output) faces

Δ αx{yPxcoversywith orientationα}. \Delta^\alpha x \coloneqq \{ y \in P \mid x \;\text{covers}\; y \;\text{with orientation}\; \alpha \}.

Dually, we define the input (reps. output) cofaces

αx{yPycoversxwith orientationα}. \nabla^\alpha x \coloneqq \{ y \in P \mid y \;\text{covers}\; x \;\text{with orientation}\; \alpha \}.

Definition

(ogPos)\mathbf{ogPos})
With that, we can define a morphism f:PQf \colon P \to Q of oriented graded posets to be a function of the underlying sets such that, for all xPx \in P and α{,+}\alpha \in \{ -, + \}, ff induces a bijection between Δ αx\Delta^\alpha x and Δ αf(x)\Delta^\alpha f(x).

Oriented graded posets and morphisms form the category ogPos\mathbf{ogPos}.

Proposition

Morphisms of oriented graded posets are order-preserving, closed and dimension-preserving.

Definition

(maximal element)
An element xx of an oriented graded poset is maximal if for α{,+}\alpha \in \{ -, + \}, αx=\nabla^\alpha x = \emptyset, that is, xx is maximal if it is covered by no element.

Definition

(boundaries)
Let UU be a closed subset of an oriented graded poset, let α=\alpha = - (resp. α=+\alpha = +), and let nn \in \mathbb{N}, let

Δ n αU{xU n αxU=}. \Delta^\alpha_n U \coloneqq \{ x \in U_n \mid \nabla^{- \alpha} x \cap U = \emptyset \}.

The input (reps. output) nn-boundary is the closed subset

n αUcl(Δ n αU) k<ncl(MaxU) k. \partial^\alpha_n U \coloneqq \mathrm{cl}(\Delta^\alpha_n U) \cup \bigcup_{k \lt n} \mathrm{cl}(\mathrm{Max} U)_k.

Example

In the running pasting diagram, calling it UU, we have

1 U={x,f,y,g,z}, \partial^-_1 U = \{ x, f, y, g, z \},

and

0 +U={z}. \partial^+_0 U = \{ z \}.

Notation

We write

nU n U n +U, \partial_n U \coloneqq \partial^-_n U \cup \partial^+_n U ,
ΔUΔ UΔ +U, \Delta U \coloneqq \Delta^- U \cup \Delta^+ U,

etc… The general convention is that if the superscript α\alpha is not provided to an operator, it is the union of the operator with α=\alpha = -, and with α=+\alpha = +.

Similarly, if the subscript nn is not provided, it means “the dimension of the oriented graded poset minus 1”, that is, we write:

U dimU1 U. \partial^- U \coloneqq \partial^-_{\dim U - 1} U.

We can also combine both notations, for instance

U= dimU1 U dimU1 +U. \partial U = \partial^-_{\dim U - 1} U \cup \partial^+_{\dim U - 1} U.

Last, if the index nn is negative, the result is the empty set, for instance,

1 U, \partial^-_{- 1} U \coloneqq \emptyset,

etc.

Remark

For any α,n\alpha, n, n αU\partial^\alpha_n U, nU\partial_n U, etc.. are subsets of UU, and the inclusion they defines

n αUU nUUetc, \partial^\alpha_n U \hookrightarrow U \quad\quad \partial_n U \hookrightarrow U \quad\quad \text{etc},

are all morphisms of oriented graded posets.

The last bit of terminology we introduce is roundness. Consider a topological nn-ball UU, and its boundary the nn-sphere U\partial U. The latter is made of the gluing of two (n1)(n - 1)-balls U\partial^- U and +U\partial^+ U along an (n1)(n - 1)-sphere n2U\partial_{n - 2} U, in particular:

U +U= n2U. \partial^- U \cap \partial^+ U = \partial_{n - 2} U.

Similarly, U\partial U is an (n1)(n - 1)-sphere, which is made of a copie of two (n2)(n - 2)-balls which intersect at an (n2)(n - 2)-sphere, etc.. We will say that an oriented graded poset is round if it satisfies similar intersection conditions.

Definition

(round)
Let PP be an oriented graded poset of dimension nn. We say that PP is round if for all 0k<n0 \le k \lt n, we have

k P k +P= k1P. \partial^-_k P \cap \partial^+_k P = \partial_{k - 1} P.

Inductive construction of molecules

We can now construct inductively a well-formed class of oriented graded posets, called the molecules, which model composable pasting diagrams. There are 3 constructors:

  • (Point) the oriented graded poset 1\mathbf{1} with a single point is a molecule.
  • (Paste) if U,VU, V are two molecules of dimensions >n\gt n such that n +U n V\partial^+_n U \cong \partial^-_n V, we construct the following pushout:

Then U# nVU \#_n V is a molecule.

  • (Atom) if two molecules are round, of the same dimension nn, such that there is an isomorphism UV\partial U \cong \partial V which restricts to isomorphisms αU αV\partial^\alpha U \cong \partial^\alpha V for α{,+}\alpha \in \{ -, + \}, we can glue the boundaries together to form an “nn-sphere”, i.e. we construct the pushout

Then, we add a top element \top to (UV)\partial(U \Rightarrow V) with orientation such that Δ MaxU\Delta^- \top \coloneqq \mathrm{Max} U and Δ +MaxV\Delta^+ \top \coloneqq \mathrm{Max} V. This defines UVU \Rightarrow V, which is a molecule.

Examples

If we take two copies of (Point) and apply (Atom) to them, we obtain the arrow I(11)\vec I \coloneqq (\mathbf{1} \Rightarrow \mathbf{1}): Then, we can use (Paste) with I\vec I and I\vec I on the 0-boundary to obtain I# 0I\vec I \#_0 \vec I:

Now we use (Atom) to construct (I# 0I)I(\vec I \#_0 \vec I) \Rightarrow \vec I: (which is also the second oriental).

Definition

(atom)
An atom is a molecule with a maximal element.

Lemma

If a molecule UU is an atom, then UU was produced by either (Point) or (Atom).

Definition

(regular directed complex)
A regular directed complex is an oriented graded poset PP such that for all xx in PP, cl(x)\mathrm{cl}(x) is an atom.

Of course, every molecule is a regular directed complex (see Lemma ), but for instance, is a regular directed complex but not a molecule.

Properties

It may seem that the above construction of molecules depends on the choice of an isomorphism during the construction. However we prove already:

Proposition

Isomorphisms of molecules are unique.

Proof

See (Corollary 3.4.12)

We will write U=VU = V to mean that there exists a unique isomorphism between UU and VV.

Proposition

The underlying poset of any regular directed complex PP is oriented thin. This means that any interval [x,y][x, y] in PP with dimx+2=dimy\dim x + 2 = \dim y contains exactly 4 elements x<t,t<yx \lt t, t' \lt y, with orientation satisfying

Remark

The above Proposition is still still true when considering the augmentation of PP (see Def. ). This additional result translates into the fact that any 1-dimensional element in PP has exactly one negative face and one positive face.

Common properties of molecules include:

Proposition

Let UU be a molecule. Then

  • for all α{,+}\alpha \in \{ -, + \} and ndimUn \geq \dim U, n aU=U\partial^\a_n U = U. In fact, dimU=min{n0 n aU=U}\dim U = \min \{ n \geq 0 \mid \partial^\a_n U = U \}.
  • for all α{,+}\alpha \in \{ -, + \} and n0n \geq 0, n aU\partial^\a_n U is a molecule, and if ndimUn \le \dim U, then dim n aU=n\dim \partial^\a_n U = n;
  • UU is connected, that is, UU is non-empty, and for all closed subsets V,WUV, W \subseteq U such that U=VWU = V \cup W and VW=V \cap W = \emptyset, then V=V = \emptyset or W=W = \emptyset;
  • if UU is round, then Max(U)=U dimU\mathrm{Max}(U) = U_{\dim U} (we say that UU is pure).
  • if UU is an atom, then UU is round.

Strict ω\omega-categorical structure

The category of molecule, with pastings # n\#_n and boundaries n α\partial^\alpha_n satisfies all the axioms of strict ω\omega-categories. More precisely, we have the following results.

Proposition

(globularity)
Any molecule UU is globular, that is, for all α,β{,+}\alpha, \beta \in \{ -, + \} and all k<nk \lt n, we have

k α( n βU)= k αU. \partial^\alpha_k(\partial^\beta_n U) = \partial^\alpha_k U.

Proposition

(boundaries)
Let U,VU, V be molecules such that U# kVU \#_k V is defined, let α{,+}\alpha \in \{ -, + \} and n0n \geq 0, then

n α(U# kV)={ n αU= n αV ifn<k, k U ifn=k,α=, k +V ifn=k,α=+, n αU# k n αV ifn>k. \partial^\alpha_n (U \#_k V) = \begin{cases} \partial^\alpha_n U = \partial^\alpha_n V & \text{if}\; n \lt k, \\ \partial^-_k U &\text{if}\; n = k, \alpha = -, \\ \partial^+_k V &\text{if}\; n = k, \alpha = +, \\ \partial^\alpha_n U \#_k \partial^\alpha_n V &\text{if}\; n \gt k. \end{cases}

Proposition

(unitality)
Let UU be a molecule of dimension nn, then for all k<nk \lt n, we have

k U# kU=U=U# k k +U. \partial^-_k U \#_k U = U = U \#_k \partial^+_k U.

Remark

Notice that in the constructor (Paste), we require that dimU,dimV>k\dim U, \dim V \gt k for U# kVU \#_k V to be defined. However, as long as k +U= k V\partial^+_k U = \partial^-_k V, the pushout in (Paste) makes sense, so we slightly overload the notation.

Proposition

(associativity)
Let U,V,WU, V, W be molecules such that (U# kV)# kW(U \#_k V) \#_k W or U# k(V# kW)U \#_k (V \#_k W) is defined, then

(U# kV)# kW=U# k(V# kW). (U \#_k V) \#_k W = U \#_k (V \#_k W).

Proposition

(exchange)
Let U,V,U,VU, V, U', V' be molecules, let k<nk \lt n such that (U# nU)# k(V# nV)(U \#_n U') \#_k (V \#_n V') is defined, then

(U# nU)# k(V# nV)=(U# kV)# n(U# kV). (U \#_n U') \#_k (V \#_n V') = (U \#_k V) \#_n (U' \#_k V').

Corollary

The set of all molecules is a strict ω\omega-category, with

  • source and target given by the boundaries;
  • composition given by the pasting operations # n\#_n;

In fact, we can do better, for PP an oriented graded poset, we let Mol/P\mathrm{Mol} / P to be the category whose objects are (the isomorphism classes of) morphisms f:UPf \colon U \to P, for UU a molecule. Precomposing ff by n αUU\partial^\alpha_n U \hookrightarrow U defines n αf\partial^\alpha_n f, while if g:VPg \colon V \to P is in Mol/P\mathrm{Mol} / P, such that n +f= n g\partial^+_n f = \partial^-_n g, then the universal property of the pushout defines a unique element f# kg:U# nVPf \#_k g \colon U \#_n V \to P in Mol/P\mathrm{Mol} / P. Hence:

Proposition

For all oriented graded poset PP, Mol/P\mathrm{Mol} / P is a strict ω\omega-category. Furthermore, any morphism f:PQf \colon P \to Q induces a strict ω\omega-functor

Mol/f:Mol/PMol/Q \mathrm{Mol} / f \colon \mathrm{Mol} / P \to \mathrm{Mol} / Q

sending UPU \to P to UPfQU \to P \stackrel{f}{\to} Q. This defines a functor Mol/:ogPosωCat\mathrm{Mol} / - \colon \mathbf{ogPos} \to \mathbf{\omega Cat}.

Submolecule and layering

Submolecule

Definition

(submolecule inclusion) The class of submolecule inclusions is the smallest subclass of inclusions of molecules containing all isomorphisms, closed under composition, and for all molecules U,VU, V such that U# nVU \#_n V is defined, both UU# nVU \hookrightarrow U \#_n V and VU# nVV \hookrightarrow U \#_n V are submolecule inclusions.

Not all inclusions of molecule are submolecule inclusion, but notably, we have the following:

Proposition

  • Any boundary inclusion n αUU\partial^\alpha_n U \hookrightarrow U is a submolecule inclusion;
  • If VV is an atom, then any inclusion VUV \hookrightarrow U is a submolecule inclusion.

Notation

Let U,VU, V be two molecules such that UVU \subseteq V. We write UVU \sqsubseteq V to signify that the canonical inclusion UVU \hookrightarrow V is a submolecule inclusion. For instance, by the above Proposition, for all xVx \in V, cl(x)V\mathrm{cl}(x) \sqsubseteq V.

Definition

(rewritable submolecule)
Let UU be a molecule. A submolecule VUV \sqsubseteq U is rewritable if VV is round (Def. ) and dimV=dimU\dim V = \dim U.

Rewritable submolecule can be substituted: if VUV \sqsubseteq U is rewritable and if WW is another molecule such that VWV \Rightarrow W is defined, then we can “replace” VV by WW inside UU, whose result we write U[W/V]U[W / V]. We can construct this formally in two steps: first we take the following pushout where ι\iota is the submolecule inclusion VUV \sqsubseteq U. Second, U(VW)U \cup (V \Rightarrow W) can be interpreted as a higher-dimensional rewrite rule that matches VV in UU and transforms it into WW, so we define the substition to be the “result” of this rewrite rule, i.e.:

U[W/V] n +U(VW). U[W / V] \coloneqq \partial^+_n U \cup (V \Rightarrow W).

The choice of terminology “substitution” and “rewriting”, is more than a mere analogy: rewritable submolecules and their interpretations for rewriting system are discussed in there.

Layering

Definition

(layering)
Let UU be a molecule, let 1k<dimU-1 \leq k \lt \dim U, and

mcard( i>k(MaxU) i). m \coloneqq \card(\bigcup_{i \gt k} (\mathrm{Max} U)_i).

A kk-layering of UU is a sequence (U (i)) 1im(U^{(i)})_{1 \le i \le m} such that

U=U (1)# k# kU (m) U = U^{(1)} \#_k \ldots \#_k U^{(m)}

and dimU (i)>k\dim U^{(i)} \gt k.

Example

For instance let O 1O^1 be 11\mathbf{1} \Rightarrow \mathbf{1} (i.e. O 1=IO^1 = \vec I) and O 2O^2 be O 1O 1O^1 \Rightarrow O^1, then the molecule has no -1-layering, one 0-layering

O 2# 0O 1# 0O 2, O^2 \#_0 O^1 \#_0 O^2,

and two 1-layerings: calling U(O 2# 0O 1# 0O 1)U \coloneqq (O^2 \#_0 O^1 \#_0 O^1) and U(O 1# 0O 1# 0O 2)U' \coloneqq (O^1 \#_0 O^1 \#_0 O^2), then the molecule is both equal to U# 1UU \#_1 U' and U# 1UU' \#_1 U.

The running pasting diagram has only on 0-layering.

Definition

(layering dimension)
Let UU be a molecule, the layering dimension of UU is the integer

lydimUmin{k1card( i>k+1(MaxU) i)1} \mathrm{lydim} U \coloneqq \min \{ k \geq -1 \mid \card(\bigcup_{i \gt k + 1} (\mathrm{Max} U)_i) \le 1 \}

The main theorem about layerings is as follows:

Theorem

Let UU be a molecule, lydimk<dimU\mathrm{lydim} \le k \lt \dim U. Then UU admits a kk-layering.

Other results include:

Proposition

Let UU be a molecule, and let (U (i)) 1im(U^{(i)})_{1 \le i \le m} be a kk-layering of UU. Then

  • k=1k = -1 if an only if UU is an atom;
  • if k0k \geq 0, then m>1m \gt 1 and lydimU (i)<k\mathrm{lydim} U^{(i)} \lt k;
  • UU admits an ll layering for kl<dimUk \le l \lt \dim U.

Furthermore, if VV is another molecule such that U# nVU \#_n V is defined, then

lydim(U# nV)max{lydimU,lydimV,n}. \mathrm{lydim} (U \#_n V) \geq \max \{ \mathrm{lydim} U, \mathrm{lydim} V, n \}.

Operations

Regular directed complexes are closed under many relevant operations used for higher category theory.

Gray product

Definition

(Gray product)
Let P,QP, Q be oriented graded posets. The Gray product of PP and QQ is the oriented graded poset PQP \otimes Q whose

  • underlying graded poset is the cartesian product P×QP \times Q,
  • orientation is defined, for all (x,y)P×Q(x, y) \in P \times Q and α{,+}\alpha \in \{ -, + \}, by the equation Δ α(x,y)=Δ αx×{y}+{x}×Δ () dimxαy\Delta^\alpha(x, y) = \Delta^\alpha x \times \{ y \} + \{ x \} \times \Delta^{(-)^{\dim x} \alpha} y.

Example

The Gray product II\vec{I} \otimes \vec{I} is

Theorem

Let P,QP, Q be regular directed complexes. Then PQP \otimes Q is a regular directed complex.

Proof

The proof is extremely combinatorial, and can be found in Section 7.2.

The Gray product is associtive and has unit the point 1\mathbf{1}. It is not symmetrical.

Join

Similarly, we can take the join of regular directed complexes. If the underlying poset of a join is easy to describe, describing the precise orientation can be quite cumbersome; since we have the Gray product, we can take the following shortcut.

Definition

(augmentation and diminution)
Let PP be an oriented graded poset.

  • The augmentation of and PP is the oriented graded poset P P{}P_\bot \coloneqq P \cup \{ \bot \} such that +=P 0\nabla^+ \bot = P_0 and =\nabla^- \bot = \emptyset.
  • Suppose PP has a minimal element \bot, then the diminution of PP is the oriented graded poset P ¬P\{}P_{\not{\bot}} \coloneqq P \backslash \{ \bot \}.

Definition

(join)
Let P,QP, Q be an oriented graded poset. The join of PP and QQ is the oriented graded poset

PQ(P Q ) ¬. P \star Q \coloneqq (P_{\bot} \otimes Q_{\bot})_{\not\bot}.

Proposition

The underlying poset of PQP \star Q has elements

{xxP}{xyxP,yQ}{yyQ}. \{ x\star \mid x \in P \} \cup \{ x \star y \mid x \in P, y \in Q \} \cup \{ \star y \mid y \in Q \}.

As in topology, it really consist of a copy of PP (whose elements are of the form xx\star), a copy of QQ (whose elements are of the form y\star y), and every element of xx of PP is linked to every element yy of QQ with xyx \star y.

Theorem

Let P,QP, Q be regular directed complexes. Then PQP \star Q is a regular directed complex.

The join is associtive and has unit \emptyset, the empty regular directed complex. It is not symmetrical.

Example

The nn-th iterated join 11\mathbf{1} \star \ldots \star \mathbf{1} of the point is the (n1)(n - 1)-th oriental.

Suspension

Definition

(suspension)
Let PP be an oriented graded poset. The suspension of PP is the oriented graded poset SP\mathsf{S}P whose

  • underlying set is
    {SxxP}{ , +}, \{ \mathsf{S}x \mid x \in P \} \cup \{ \bot^-, \bot^+ \},
  • partial order and orientation are defined by
    αx{{Syy αx} ifx=Sx,xP, {SyyP 0} ifx= α, ifx= α. \nabla^\alpha x \coloneqq \begin{cases} \{ \mathsf{S}y \mid y \in \nabla^\alpha x' \} & \text{if}\; x = \mathsf{S}x', x' \in P, \\ \{ \mathsf{S}y \mid y \in P_0 \} & \text{if}\; x = \bot^\alpha, \\ \emptyset & \text{if}\; x = \bot^{-\alpha}. \end{cases}

    for all xSPx \in \mathsf{S}P and α{,+}\alpha \in \{ -, + \}.

Theorem

Let PP be a regular directed complex. Then SP\mathsf{S}P is a regular directed complex.

Proposition

Let U,VU, V be molecules.

  • suppose U# kVU \#_k V is defined, then S(U# kV)=SU# k+1SV\mathsf{S}(U \#_k V) = \mathsf{S}U \#_{k + 1} \mathsf{S}V.
  • suppose UVU \Rightarrow V is defined, then S(UV)=(SUSV)\mathsf{S}(U \Rightarrow V) = (\mathsf{S}U \Rightarrow \mathsf{S}V).

Example

The nn-th iterated suspension SS1\mathsf{S}\ldots\mathsf{S}\mathbf{1} is the nn-th globe.

Geometric realization

Since every regular directed complex is in particular a poset, we can take its nerve, which is a simplicial set P ΔP^\Delta, whose nn-simplices are chains x 0x nx_0 \le \ldots \le x_n in PP. Via the classical geometric realization of simplicial sets, we define a functor |||-| from regular directed complexes to (a convenient category of) topological spaces.

As expected, round molecules are round:

Proposition

Let UU be a round molecule of dimension nn, then

  • |U||U| is an nn-ball,
  • |U||\partial U| is an nn-sphere.

Furthermore, Gray products, joins, and suspensions are sent to their topological counterpart:

Proposition

Let P,QP, Q be regular directed complexes, then

Proof techniques

Structural induction

Since molecules are defined inductively, we can use structural induction to prove statement about them. To prove that a statement 𝒫\mathcal{P} is true for all molecules, we can do as follows:

  • We prove that 𝒫\mathcal{P} is true for the (Point) 1\mathbf{1}.
  • We let U,VU, V be molecules such that U# nVU \#_n V is defined, and we suppose that 𝒫\mathcal{P} holds for both UU and VV. Then we prove that 𝒫\mathcal{P} holds for U# nVU \#_n V.
  • We let U,VU, V be molecules such that UVU \Rightarrow V is defined, and we suppose that 𝒫\mathcal{P} holds for both UU and VV. Then we prove that 𝒫\mathcal{P} holds for UVU \Rightarrow V.

For instance:

Lemma

Any molecule is a regular directed complex.

Proof

Let UU be a molecule, we need to prove that for all xUx \in U, cl(x)\mathrm{cl}(x) is an atom. We proceed by induction on the construction of UU. If UU was produced by (Point), then xx must be the unique element of UU whose closure is UU itself. If UU was produced by (Paste), then U=V# kWU = V \#_k W , and xVx \in V or xWx \in W ; the inductive hypothesis applies. If UU was produced by (Atom), it is equal to (VW)+{}(V \cup W ) + \{ \top \}, and either xVx \in V or xWx \in W, in which case the inductive hypothesis applies, or x=x = \top, and cl(x)=U\mathrm{cl}(x) = U is an atom by definition.

Other methods

The proof by induction on submolecules allows us to prove a statement 𝒫𝒬\mathcal{P} \implies \mathcal{Q} for all molecules as follows: assume that a molecule UU satisfies 𝒫\mathcal{P}, then

  • we prove that {x}\{ x \} satisfies 𝒬\mathcal{Q} for all xU 0x \in U_0 (the base cases);
  • we prove that UU satisfies 𝒬\mathcal{Q} under the assumption that every proper submolecule VUV \sqsubseteq U satisfies 𝒬\mathcal{Q}

This induction principle is justified since every proper submolecule of UU has stricly fewer elements than UU, and the set of minimal elements for \sqsubseteq is presicely U 0U_0.

Example

The proof that molecules are stable under Gray product uses induction on submolecules.

Another proof technique is the induction on the layering dimension: to prove that a property holds for all molecules U, it suffices to

  • prove that it holds when lydimU=1\mathrm{lydim} U = -1, i.e. when UU is an atom (base case);
  • prove that it holds when klydimU0k \coloneqq \mathrm{lydim} U \geq 0, assuming that it holds of all the (U (i)) 1im(U^{(i)})_{1 \le i \le m} in any kk-layering of UU.

Indeed, by Theorem , any molecule has a layering, and Proposition gives the well-foundedness.

For instance, let us prove the following:

Proposition

Every molecule is made of pasting of atoms.

Proof

Let UU be a molecule, we proceed by induction on klydimUk \coloneqq \mathrm{lydim} U. If k=1k = -1, then this follows by definition since UU is an atom. Let k>0k \gt 0, and take a kk-layering of UU

U=U (1)# k# kU (m), U = U^{(1)} \#_k \ldots \#_k U^{(m)},

with lydimU (i)<k\mathrm{lydim} U^{(i)} \lt k. Then by induction, each U (i)U^{(i)} is a composition of atoms, thus so is UU.

Remark

The proof works equally well by structural induction.

References

The main reference on regular directed complexes:

For a computational perspective on regular directed complexes:

  • Diana Kessler, Amar Hadzihasanovic, Higher-dimensional subdiagram matching, LICS 2023 (link)

Last revised on August 8, 2024 at 11:09:35. See the history of this page for a list of all contributions to it.