Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
(13th February 2015)
I would like, in a series of comments in this thread, to outline a proof of the homotopy hypothesis, in a very strong sense, for a certain algebraic, cubical notion of $\infty$-groupoid. I have been working on this kind of question for around four and a half years, and the rough outline of the approach that I will take dates from the beginning of this time. In the years since, when time has permitted, I have been working on placing the approach in a conceptual framework, reworking aspects of it accordingly, and on certain details. Recently, I have felt that I now understand the story deeply enough to wish to make the details public, and have clarified the conceptual points that I wished to address.
It is likely, however, that writing this up in a conventional way will take me a very long time. This is principally because I wish to write it up in a way which follows my own ’philosophy’ as to how best to approach it. This has a considerable foundational aspect: it is important to me to work constructively, in a strong sense, and I actually wish to work in a formal ’synthetic category theory’, which I am implementing as a Martin-Löf type theory in Coq. This ’synthetic category theory’ differs quite considerably from ’standard’ approaches to categorical foundations, even in the treatment of basic aspects. Thus it will take a considerable time before it is developed even to the point of being able to carry out the work on the homotopy hypothesis that I will describe.
In this series of posts, at least for a considerable time, I do not plan to emphasise these foundational aspects. I instead plan to focus on the principal ideas which relate directly to the homotopy hypothesis.
This ’philosophy’ also has a ’stylistic’ aspect. I like to argue very diagramatically, and I like to give full details. Sometimes I also like to write up material in the literature, if it fixes notation, or if I feel that my presentation differs in ways that I prefer. All of these points differ from the sylistic conventions of ’standard’ write ups, and tend to mean that my write ups are quite long.
Secondly, the work on the homotopy hypothesis has evolved into a broader programme investigating the foundations of abstract homotopy theory: ways to construct derivators; ways to construct model categories, and a reworking of this notion; a cubical Milnor theorem; etc. All these aspects also need to be written up to present fully the work on the homotopy hypothesis as I see it. This is a considerable task, and is not linear: the projects are inter-related. Thus I feel somewhat constrained and daunted by the task of writing it up in a conventional way. In addition, I am interested in other things, which also need writing up, some of which I have mentioned on the nForum before.
Thirdly, I do not have so much time to work on the writing up. I put a great deal of energy into teaching, and enjoy and am very motivated by it. I feel an ethical responsibility (my apologies if this sound pretentious, I do not intend it to be perceived this way!) to prioritise it over research when the two must be balanced, and do so. Whilst I happen to have a little more time than usual for a few months just now, it is quite possible that I will not have much time, possibly very little time at all, for intensively writing up work in the foreseeable future afterwards. Thus I would prefer to just write up things here and there where I can.
The reason that I propose to post my work here in the nForum is that I see it as a place in which a community can discuss mathematics related to category theory and higher category theory. I appreciate that the nForum was originally intended as a support for the nLab, but I hope that it now can be considered in a broader light. Indeed, I should say from the beginning that I do not have any particular intention myself to incorporate anything that I write into the nLab (this is of course not to preclude others from doing so, if they so wish and feel that it fits), and that nothing to do with the nLab is, directly at least, part of my motivation for posting here. If the kind of contribution that I have in mind is not welcomed, because a stricter interpretation of the purpose of the nForum is upheld, or for any other reason, just let me know.
My principal hope is that people will ask questions, and engage in discussion with me, about the ideas that I will post (just post comments in between mine). This would help me enormously with regard to spurring me on to write up more.
As a final, quick caution, I should say that I do not intend my posts to be viewed as presenting the mathematics ’from on high’. I hope we can agree that arriving at a ’bug free’ presentation of mathematical ideas is a more organic process, and that details are likely to be tweaked in the light of discussion.
(13th February 2015)
I’ll begin by working towards a definition of a cubical analogue of the $\mathsf{Ex}^{\infty}$ functor for simplicial sets. This cubical $\mathsf{Ex}^{\infty}$ functor will play a crucial role in the approach to the homotopy hypothesis that I will discuss.
I’ll first define the category of cubical sets. Let $\square_{\leq 1}$ be the unique category with the following properties.
1) There are two objects, which I’ll denote by $I^{0}$ and $I^{1}$.
2) There is a pair of arrows as follows.
3) There is an arrow as follows.
4) The following diagrams in $\square_{\leq 1}$ commute.
I often refer to this category $\square_{\leq 1}$ as the free-standing interval equipped with a contraction structure. This terminology comes from my thesis.
We now denote by $\square$ the free strict monoidal category on $\square_{\leq 1}$ in which $I^{0}$ is a unit object. A subtle but crucial point here: $\square$ is not the free strict monoidal category on $\square_{\leq 1}$. In the latter category, $I^{0}$ is not a unit object. One way to define $\square$ is to take the free strict monoidal category on $\square_{\leq 1}$, and then to identify the unit object with $I^{0}$. I will make a lot of use, although not for a while, of the fact that being a ’free strict monoidal category with a designated unit’ is a 2-universal property, not only a 1-universal property.
I’ll denote the object $I^{1} \otimes \cdots \otimes I^{1}$ of $\square$, where the tensor product is taken $n$ times, by $I^{n}$.
The category of cubical sets is the free co-completion of $\square$. I’ll denote it by $\mathsf{Set}^{\square^{op}}$, even though one of the foundational aspects of the work is that I will construct the free co-completion of a category in a purely categorical way, without relying upon a prior notion of set, and thus this notation will not really be appropriate. Another foundational aspect of the work is that I will work throughout with ’unbiased monoidal categories’, but I’ll ignore this aspect too for a good while.
PS: Apologies for the missing commutative diagrams. I will edit once I have found a satisfactory way to include them. At the moment I am thinking of creating the diagrams in TikZ, and then including them somehow. Does anyone know if it is possible to include SVG code in a forum post? Or if there is some other good way to include images (if there is nothing better, I could host them on my own webpage).
Edit: Commutative diagrams now added. They are png images, hosted at this bitbucket repository, together with the source code. I have used a little html to centre them.
You are very welcome to share material here on the forum. (The urge to put stuff on the $n$Lab is meant constructively: experience shows that material scattered through discussion forum threads is much harder to absorb later, than if the stabled bits of it have been compiled on a dedicated page. )
Regarging diagrams: the $n$Lab at least supports SVG graphics, see at How to… include SVG figures. Other ways to include diagrams are discussed at How to… draw commutative diagrams (though the instructions there may need updating, not sure).
Richard: have you a personal n-Lab page (like my homepage). If you have why not develop a series of entries on this stuff using the richer environment there, and making it available when you want to for all to see. You can (I seem to remember) password protect some of the pages so need not fear spam. WHen it has satbilised then you can put it on the regular nLab pages.
Following on from the two comments above, you could always then advertise any additions as you make them in this discussion thread, while keeping the whole on an nLab page with its better graphics.
… that is what I was going to say next, so thanks David.
Richard comments boxes on n-Lab pages are also a source of useful feedback, but then people have to tell others here where the comments boxes are.
A few versions of “cubical sets” can be found in the literature. Could you say which version your universal property describes? Are these plain cubical sets with standard face and degeneracy operators? Or do they include connections or perhaps something else?
Urs, Tim, and David, thank you for your suggestions. I do not have a personal web page on the nLab, but for now I am quite keen to experiment with just posting in the nForum. As mentioned, my hope is to discuss the material with others, and a forum seems like the best place for that. The plan would be to collate the material after a while into something more stable: I certainly agree that leaving the material just in a forum discussion would not be best in the long term. If all goes to plan, I, every now and then, could make a ’summary post’, acting as a signpost through the discussion.
I have settled on a way to include the diagrams that is sufficiently robust for me. In case anybody is interested: I write them in TikZ (I have some macros which mean that I can usually do this very quickly), and then export them to pdf files; convert them to png files (they could be converted to svg instead, but svg files tend not to display well on my browser); and then host them in a git repository, which I link to from the post. If anybody is interested, the source files can be found on the repository too.
Karol, thank you for the question, it is exactly the kind of thing that I am looking for. Yes, the cubical sets that I have defined are the plain cubical sets that you refer to.
However, connections will play a role later on, and indeed other structures as well.
Connections (and other structures) could be included already at this stage, and taken into account in what I am about to do next. However, since we have less things to check when constructing functors canonically out of $\square$ than out of the version with connections, various things can be presented a little more simply when working with plain cubical sets, and thus I will do so.
It is slightly surprising, but I have found that typically connections are not so important to build into cubical sets themselves: it is usuallly enough that they are present in the structures we build upon cubical sets (appropriate flavours of $n$-groupoid, for example), or in the categories which we construct functors from cubical sets into ($\mathsf{Top}$, for example).
Something that I have thought a few times about, though, is that it could be very nice to axiomatise the notion of a ’decorated category of cubes’ (i.e. a category of cubes with some extra structure: connections, etc), and to work in this generality. I certainly think that this should be possible, and that everything that I will do could be carried out in this generality.
I do not have a personal web page on the nLab, but for now I am quite keen to experiment with just posting in the nForum.
If you have lots of stuff you want to create in nLab like format you can always create a a bunch of pages in Doriath. To link from there to the actual nLab you have to give your links
nLab:
prefixes - e.g. [[nLab:modular lattice]]
. If you use this prefix in the nLab or nForum it works fine but does show the namespace - modular lattice (nlab) which should be no big deal if you are copying and pasting to the nForum.
(14th February 2015)
Carrying on from #2, I’ll now define a functor as follows.
The next step will be to use this functor to define the functor $\mathsf{Ex}^{\infty}$ that we are aiming for.
We’ll need a little notation when working with cubical sets.
1) Given an integer $n \geq 0$, I’ll denote by $\square^{n}$ the cubical set represented by $I^{n}$. I often refer to $\square^{n}$ as the free-standing $n$-cube.
2) I’ll use the same notation for an arrow
as for the corresponding arrow in $\square$. Thus, for instance, there is a pair of arrows
and an arrow as follows.
3) Given a cubical set $X$, we’ll refer to a morphism of cubical sets
as an n-cube of $X$.
With this notation to hand, we will, to construct our functor $\mathsf{Ex}$, fix a co-cartesian square as follows.
In other words, we fix a pushout of the following diagram.
The cubical set $\mathsf{Sd}_{\leq 1}(\square^{1})$ can be pictured as follows.
Indeed, we take two copies of $\square^{1}$
and glue together the two 0-cubes depicted in blue. The arrow head points to the 0-cube corresponding to $i_{1}$.
We now define a functor
as follows.
1) To $I^{0}$, we associate the cubical set $\square^{0}$.
2) To $I^{1}$, we associate the cubical set $\mathsf{Sd}_{\leq 1}(\square^{1})$.
3) To $i_{0}$, we associate the following morphism of cubical sets.
4) To $i_{1}$, we associate the following morphism of cubical sets.
5) To $p$, we associate the canonical morphism
of cubical sets such that the following diagram in $\mathsf{Set}^{\square^{op}}$ commutes.
In fact, $\square^{0}$ is a final object of $\mathsf{Set}^{\square^{op}}$, so we could instead have made use of this universal property to define $\mathsf{Sd}_{\leq 1}(p)$. I find the above definition to get more to the heart of the matter, though.
Now, the monoidal structure on $\square$ gives rise to a (closed) monoidal structure on $\mathsf{Set}^{\square^{op}}$: on representable presheaves, we specify that it agrees with the monoidal structure on $\square$, and then we extend by colimits.
By the universal property of $\square$, the functor $\mathsf{Sd}_{\leq 1}$ gives rise to a functor as follows.
In other words, we ’extend $\mathsf{Sd}_{\leq 1}$ monoidally’. For instance, $\mathsf{Sd}(\square^{2})$ looks as follows.
The squares here are not ’hollow’, they are 2-cubes. A pair of dots $\bullet \bullet$ should be read as $\bullet \otimes \bullet$. I have omitted the labels of the 1-cubes and 2-cubes.
By the universal property of free co-completion, the functor
extends to a functor
which I’ll also denote by $\mathsf{Sd}$ (it agrees with our original $\mathsf{Sd}$ on representables).
As is the case for any functor constructed in this way, $\mathsf{Sd}$ admits a right adjoint
which is the functor $\mathsf{Ex}$ that we were aiming to construct in this post.
The adjunction tells us that, given a cubical set $X$, an $n$-cube of $\mathsf{Ex}(X)$ is a morphism as follows.
For instance, a $1$-cube of $\mathsf{Ex}(X)$ consists of a pair of $1$-cubes $f$ and $g$ of $X$ whose faces match up as follows.
Thank you for your suggestion, Rod. Regarding the personal page in the nLab: this was in reply to Tim, I am not actually looking to create nLab-like pages. The ’experiment’ that I mentioned is with regard to posting mathematics in this way, with the hope of receiving questions and engaging in discussion, not really with regard to the presentation of the mathematics.
As an aside to all, when I first made the last two posts, some of the figures did not display for a while. This was probably a temporary difficulty with connecting to bitbucket, or something like that, because they display fine now. Thus, if you do not see some of the figures, hold on for a little while, and they will hopefully appear eventually!
(15th February 2015)
Continuing from #12, I’ll now define a natural transformation as follows.
This natural transformation will be used to define the $\mathsf{Ex}^{\infty}$ functor that we are aiming to construct. To construct $\iota$, we will make use of the 2-universal property of $\square$, and the 2-universal property of free co-completion. This technique is one of the innovations of our work on cubical homotopy theory, and we will see it again.
Let
be the canonical functor.
Let
denote the Yoneda embedding functor.
Let
be the restriction of the Yoneda embedding functor to $\square_{\leq 1}$, namely the composite functor $y \circ \mathsf{can}$.
We begin by defining a natural transformation
in the following way.
1) To $I^{0}$, we associate the following identity morphism.
2) To $I^{1}$, we associate the canonical morphism
of cubical sets such that the following diagram in $\mathsf{Set}^{op}$ commutes.
It is straightforward to check that the three diagrams which must commute do indeed commute.
Recall that we can picture $\mathsf{Sd}_{\leq 1}(\square^{1})$ as follows
and that we can picture $\square^{1}$ as follows.
The morphism
can then be pictured as sending the left 1-cube of $\mathsf{Sd}(\square^{1})$ to the unique non-degenerate 1-cube of $\square^{1}$, whose faces are $0$ and $1$; and sending the right 1-cube of $\mathsf{Sd}(\square^{1})$ to the degenerate 1-cube of $\square^{1}$ whose faces are both $1$.
By the 2-universal property of $\square$, the natural transformation
gives rise to a natural transformation as follows.
We now observe that it is the identity functor
to which the Yoneda embedding functor
gives rise by means of the universal property of $\mathsf{Set}^{\square^{op}}$ as a free co-completion.
By means of the 2-universal property of $\mathsf{Set}^{\square^{op}}$ as a free co-completion, the natural transformation
thus gives rise to a natural transformation as follows.
I’ll again denote this natural transformation by $\phi$ (it agrees with our earlier $\phi$ on representables).
Let
be the unit natural transformation of the adjunction between $\mathsf{Sd}$ and $\mathsf{Ex}$.
Let $\mathsf{Ex} \cdot \phi$ denote the natural transformation
obtained by whiskering the following diagram.
Let
be the composition of natural transformations $(\mathsf{Ex} \cdot \phi) \circ \eta$. In other words, the following triangle commutes.
This natural transformation $\iota$ is the one which we were aiming to define. Given a cubical set $X$, it for instance sends a 1-cube
of $X$ to the 1-cube of $\mathsf{Ex}(X)$ pictured below, in which the right 1-cube is degenerate.
(16th February 2015)
Continuing from #15, I’ll in this post define the functor $\mathsf{Ex}^{\infty}$ that we have been working towards.
Actually, there is more than one possible definition. One possibility is to take the colimit of the following diagram in the category of functors from $\mathsf{Set}^{\square^{op}}$ to itself.
Here $\iota \cdot \mathsf{Ex}^{n}$ for $n \geq 1$ is the whiskering of the following diagram.
This is analogous to the definition of the well known $\mathsf{Ex}^{\infty}$ functor in the simplicial case.
However, one of the main points of departure of our work on the homotopy hypothesis will be to observe that, after 1-truncation, $\mathsf{Ex}^{\infty}(X)$, where $X$ is a cubical set, is very close to the underlying cubical set of the free groupoid on the 1-truncation of $X$.
There is a difference, however: the arrows of the free groupoid on the 1-truncation of $X$ can be viewed as zig-zags of $n$ arrows, where $n \geq 0$ is any even integer. Depicted below, for example, is a zig-zag consisting of six arrows.
On the other hand, the 1-cubes of $\mathsf{Ex}^{\infty} (X)$ as defined at the beginning of this post can be viewed as zig-zags of $2^{n}$ 1-cubes of $X$, where $n \geq 0$ is an even integer. There is, for instance, no zig-zag of six 1-cubes of the same shape as in the previous picture.
This difference is probably not essential for what I will do: I think it likely that one could adapt everything to go through for the $\mathsf{Ex}^{\infty}$ functor defined above. However, it will be convenient for us to give a different definition, which makes the analogy between the 1-truncation of $\mathsf{Ex}^{\infty}(X)$ and the free groupoid on the 1-truncation of $X$ closer.
The idea to use this alternative definition is due to Erik Rybakken. The key result that I will prove in future posts about this $\mathsf{Ex}^{\infty}$ functor is joint work with Espen Auseth Nielsen and Erik Rybakken.
Actually, whilst the analogy between $\mathsf{Ex}^{\infty}(X)$ and the free groupoid functor is something that has been an important part of my thinking about the homotopy hypothesis for quite a long time, it was not this which led Erik to his definition. It was rather to simplfy the construction of certain morphisms of cubical sets needed to carry out the proof of the ’key result’ mentioned in the previous paragraph.
I’ll now work towards the definition of $\mathsf{Ex}^{\infty}$ that we’ll adopt.
Let us denote the functor
by $\mathsf{Sd}_{\leq 1}^{1}$, the morphism of cubical sets
by $r_{0}^{1}$, and the morphism of cubical sets
by $r_{1}^{1}$.
We will now define inductively, for every integer $n \geq 1$, a functor as follows.
Suppose that we have defined $\mathsf{Sd}_{\leq 1}^{n}$, where $n \geq 1$ is an integer. We fix a co-cartesian square in $\mathsf{Set}^{\square^{op}}$ as follows.
The functor $\mathsf{Sd}_{\leq 1}^{n+1}$ is then defined as follows.
1) To $I^{0}$, we associate the cubical set $\square^{0}$.
2) To $I^{1}$, we associate the cubical set $\mathsf{Sd}_{\leq 1}^{n+1}(\square^{1})$.
3) To $i_{0}$, we associate the following morphism of cubical sets.
4) To $i_{1}$, we associate the following morphism of cubical sets.
5) To $p$, we associate the canonical morphism
of cubical sets such that the following diagram in $\mathsf{Set}^{\square^{op}}$ commutes.
In other words, to obtain $\mathsf{Sd}_{\leq 1}^{n+1}(\square^{1})$, we glue a copy of $\mathsf{Sd}_{\leq 1}^{1}(\square^{1})$ to the end of $\mathsf{Sd}_{\leq 1}^{n}(\square^{1})$. For instance, $\mathsf{Sd}_{\leq 1}^{3}(\square^{1})$ is obtained by glueing a copy of $\mathsf{Sd}_{\leq 1}^{1}(\square^{1})$
to the end of a copy of $\mathsf{Sd}_{\leq 1}^{2}(\square^{1})$.
This gives the following.
By the universal property of $\square$, the functor $\mathsf{Sd}_{\leq 1}^{n}$ gives rise to a functor as follows.
By the universal property of free co-completion, this functor $\mathsf{Sd}^{n}$ extends to a functor
which I’ll also denote by $\mathsf{Sd}_{n}$ (it agrees with $\mathsf{Sd}^{n}$ on representables).
As is the case for any functor constructed in this way, $\mathsf{Sd}_{n}$ admits a right adjoint as follows.
Let us denote the natural transformation
by $\phi_{\leq 1}^{1}$, and denote the morphism of cubical sets
by $q^{1}$.
Inductively, I’ll now define, for every integer $n \geq 1$, a natural transformation as follows.
Suppose that we have defined $\phi_{\leq 1}^{n}$. We then define $\phi_{\leq 1}^{n+1}$ in the following way.
1) To $I^{0}$, we associate the following identity morphism.
2) To $I^{1}$, we associate the canonical morphism
of cubical sets such that the following diagram in $\mathsf{Set}^{op}$ commutes.
It is straightforward to check that the three diagrams which must commute do indeed commute.
Recall that we can picture $\mathsf{Sd}_{\leq 1}^{3}(\square^{1})$ as follows
and that we can picture $\mathsf{Sd}_{\leq 1}^{2}(\square^{1})$ as follows.
The morphism
can be pictured as ’chopping off the last zig-zag’ of $\mathsf{Sd}_{\leq 1}^{3}(\square^{1})$. Namely the first four 1-cubes, from the left, of $\mathsf{Sd}_{\leq 1}^{3}(\square^{1})$ are sent to the corresponding four non-degenerate 1-cubes of $\mathsf{Sd}_{\leq 1}^{2}(\square^{1})$; and the last two 1-cubes of $\mathsf{Sd}_{\leq 1}^{3}(\square^{1})$ are both sent to the degenerate 1-cube whose faces are the rightmost 0-cube of $\mathsf{Sd}_{\leq 1}^{2}(\square^{1})$.
By the 2-universal property of $\square$, the natural transformation
gives rise to a natural transformation as follows.
By means of the 2-universal property of $\mathsf{Set}^{\square^{op}}$ as a free co-completion, this natural transformation $\phi^{n+1}$ gives rise to a natural transformation as follows.
Let us denote the natural transformation
by $\iota_{1}$.
For any integer $n \geq 1$, let
be the unit natural transformation of the adjunction between $\mathsf{Sd}_{n+1}$ and $\mathsf{Ex}_{n+1}$, and let
be the co-unit natural transformation of the adjunction between $\mathsf{Sd}_{n}$ and $\mathsf{Ex}_{n}$.
Let $\eta_{n+1} \cdot \mathsf{Ex}_{n}$ denote the natural transformation
obtained by whiskering the following diagram.
Let $\mathsf{Ex}_{n+1} \cdot \phi_{n+1} \cdot \mathsf{Ex}_{n}$ denote the natural transformation
obtained by whiskering the following diagram.
Let $\mathsf{Ex}_{n+1} \cdot \epsilon_{n}$ denote the natural transformation
obtained by whiskering the following diagram.
Let
be the composition of these natural transformations. In other words, the following diagram commutes.
Given a cubical set $X$, the natural transformation $\iota_{3}$ for instance sends a 1-cube
of $\mathsf{Ex}_{2}(X)$ to the 1-cube of $\mathsf{Ex}_{3}(X)$ pictured below, in which the two 1-cubes in the rightmost zig-zag are degenerate.
We define
to be the colimit in the category of functors from $\mathsf{Set}^{\square^{op}}$ to $\mathsf{Set}^{\square^{op}}$ of the following diagram.
Unwrapping this definition, a $1$-cube, for instance, of $\mathsf{Ex}^{\infty}(X)$ can, as discussed earlier, be viewed as a zig-zag of $2n$ 1-cubes of $X$, for some integer $n \geq 0$.
My apologies to anyone who has already tried to read today’s post (split into four). I temporarily couldn’t see the pictures when previewing: some of the diagrams were out of order, and I had copied and pasted the wrong text towards the end. Everything has hopefully been tidied up now!
(17th February 2015)
Continuing from #19, we now have to hand a functor as follows.
Two important points to keep in mind from the discussion so far are the following.
1) This functor is not directly analogous to the simplicial $\mathsf{Ex}^{\infty}$ functor, as discussed at the beginning of #16.
2) We have not relied at any point on a presentation of $\square$ by generators and relations. Our functors and natural transformations have been constructed canonically.
One of the properties of the simplicial $\mathsf{Ex}^{\infty}$ functor is that the canonical morphism
of simplicial sets is a weak equivalence. However, the only proof that I am aware of is very indirect, and relies upon the Milnor theorem that the adjunction morphism
is a weak equivalence.
The key property of the cubical $\mathsf{Ex}^{\infty}$ functor that we have defined is analogous. To describe it, we need to prepare a little.
Let $\mathcal{A}$ be a co-complete monoidal category, and let $\mathsf{I} = (I,i_{0},i_{1},p)$ be an interval in $\mathcal{A}$ equipped with a contraction structure, in the sense of my thesis. This structured interval determines (more precise details for everything in this introduction will be given later) a functor
and thus a functor as follows.
I will prove that, if the interval $\mathsf{I}$ admits certain further structures, then the arrow
of $\mathcal{A}$ is a homotopy equivalence with respect to $\mathsf{I}$, where
the canonical natural transformation.
The principal points that I wish to draw attention to are the following.
1) Taking $\mathcal{A}$ to be $\mathsf{Top}$, and taking $\mathsf{I}$ to be the usual topological interval, our result gives that
is a weak equivalence of cubical sets. The extra generality of our result places our proof in a conceptual framework, but is important not only for this aesthetic reason. We will actually make use of a different choice of $\mathcal{A}$ when working on the homotopy hypothesis.
2) Our proof is completely different from the proof in the simplicial setting referred to earlier. In particular, it is constructive. We will construct by hand a homotopy inverse to
and by hand the homotopy that we need to show that we have a homotopy equivalence.
At this point, having completed the construction of the cubical $\mathsf{Ex}^{\infty}$ functor, I was originally planning to assume a few properties of our functor $\mathsf{Ex}^{\infty}$, and a few other things, and begin discussing the homotopy hypothesis directly. However, I am fond of our approach to the result described above, and have decided to give the details now, before moving onto the homotopy hypothesis. As mentioned in a previous post, all work on this result is joint with Espen Auseth Nielsen and Erik Rybakken.
I have intended since our work on this result began to take shape to dedicate it to the memory of Daniel Kan. I never met or corresponded with him, but the tools and ideas that he introduced in his work are used in almost every line that I write, and have had a great influence on my mathematical thought. Category theory was very young when he wrote his first papers, and it is remarkable to me that he was already able to make use of the language, and to make crucial developments in it, to lay the foundations for abstract homotopy theory. His influence is of course widely acknowledged, but my impression nevertheless is that its extent is still to be fully appreciated: I think that future historians of mathematics will come to see his early work as highly significant, the sapling from which the vast tree of abstract homotopy theory grew.
Richard, thank you for a very thorough presentation of your results. I wish more people did this.
Are you aware of the paper Simplicial Sets from Categories by Latch, Thomason and Wilson? The proof of their Theorem 4.1 can be easily adapted to a neat proof that $X \to \Ex X$ is a weak equivalence for every simplicial set $X$. The argument can be presented in a completely combinatorial way without any reference to topological spaces whatsoever. I think that this approach should work over an elegant Reedy category (is $\square$ such?) provided that a reasonable $\Ex$ functor can be constructed (I haven’t digested your definition yet so I don’t know whether it is in line with that argument).
I know of two other “purely combinatorial” proofs that $X \to Ex^\infty (X)$ is a weak homotopy homotopy equivalence of simplicial sets:
Proposition 2.3.19 in [Cisinski, Les préfaisceaux comme modèles des types d’homotopie], which mainly relies on the fact that $diag : \mathbf{ssSet} \to \mathbf{sSet}$ takes degreewise weak homotopy equivalences to weak homotopy equivalences. It seems to be closely related to the theorem of Latch, Thomason, and Wilson that Karol mentioned.
A colleague of mine has recently given an explicit presentation of $X \to Ex^\infty (X)$ as an anodyne extension (indeed, as a relative cell complex built from horn inclusions). Of course, this depends very much on the combinatorics of simplices, but it does eventually give an independent construction of the model structure on simplicial sets.
As far as I can tell Cisinski’s proof is basically the same as that of LTW. The thing is that all the prerequisites for that argument (preservation of weak equivalences by the diagonal functor being the crucial one) can be established in an elementary way without going through the abstract theory of model structures on categories of presheaves.
When it comes to the second approach, of course it follows a posteriori that the map $X \to \Ex^\infty X$ is an anodyne extension, but I always assumed that writing that down explicitly would be a hopelessly tedious task. Can you say anything about that? In particular does it work for $\Ex$ or only $\Ex^\infty$?
Thank you for the encouragement, Karol!
Thank you very much to you both for the interesting comments. Please jump in with references as you have done here whenever you wish!
I was aware of both the paper of Latch, Thomason and Wilson and the work of Cisinski, but had forgotten about these proofs! It is great that you have reminded me.
I think that this approach should work over an elegant Reedy category (is $\square$ such?)
I had not thought much about this before, but, yes, it seems to me that $\square$ is an elegant Reedy category. That it is a Reedy category is well known: a reference for the third property in the definition of a Reedy category given in the nLab is Lemma 4.1 in the paper Cubical sets and their site of Grandis and Mauri, but the result for example also appears as Lemme 8.4.4 in the work Les préfaisceaux comme modèles des types d’homotopie of Cisinski, and probably has been known for much longer. Given the usual presentation of $\square$ by generators and relations, it is straightforward to see how a proof should go, appealing to the functoriality of $- \otimes -$, although writing down a truly rigorous proof might take some care.
I have not found a reference which observes that $\square$ is an elegant Reedy category, but I think this should follow from Proposition 1.2.1 in Notes on simplicial homotopy theory by Joyal and Tierney, which is one way to prove it for $\Delta$. I haven’t checked all the details carefully, though.
If I read Theorem 5.1 in the paper of Grandis and Mauri correctly, it would seem to me that the category of cubes with connections can also be viewed as a Reedy category, if we regard both co-degeneracies and co-connections as belonging to $R_{-}$. However, this doesn’t seem particularly natural to me. The result of Grandis and Mauri would rather suggest considering factorisations into three kinds of maps, not only two. I’ve not thought about whether the category of cubes with connections, if able to be viewed as a Reedy category in this way, is elegant, but it seems possible.
I think that this approach should work over an elegant Reedy category provided that a reasonable Ex functor can be constructed
That would be interesting! More generally, it would be very interesting to see any kind of serious work along these lines in abstract homotopy theory, namely working in an axiomatic framework that captures both simplicial and cubical sets. Of course there is the notion of a test category, but this seems to me to be too general. The notion of a Reedy category is closer, but still does not feel right to me. One reason is given above, but, more conceptually, it doesn’t seem to me the existence/uniqueness of the factorisations required in the definition of a Reedy category is at the heart of why $\Delta$ and $\square$ are good categories of shapes for abstract homotopy theory. I have never used this when working with cubical sets, for instance.
My feeling is that the category of cubes is somehow ’universal’ amongst categories of shapes for abstract homotopy theory. It would be interesting, taking this idea seriously, to try to formally develop the homotopy theory of simplicial sets ’from a cubical point of view’. A point of view that is a little similar to this can be found in Jardine’s two papers on cubical homotopy theory: Cubical homotopy theory - a beginning and Categorical homotopy theory. The question of formalising the notion of a ’decorated category of cubes’ that I mentioned in #9 is closely related.
The proof that I will give is of a very different flavour from that of Latch, Thomason, and Wilson, and that of Cisinski. Perhaps one could summarise the difference by saying that the proof I will give is ’structural’ rather than ’combinatorial’. But this will become clearer when I’ve given further details.
My feeling is that the category of cubes is somehow ’universal’ amongst categories of shapes for abstract homotopy theory.
Personally, I feel that this distinction should go to $\Delta$ but that’s just based on my own astonishment at how neat and elegant simplicial homotopy theory is. If I try to think about it in an unbiased way I don’t see any clear advantages of either approach. In both cases we start with some basic notion of a $1$-dimensional homotopy and we follow some pattern of generating notions of homotopies of higher dimensions, both look equally ad hoc to me. I see where you are coming from with the universal property of $\square$ but the choice of a monoidal category as the basic structure seems just as arbitrary as the choice of a Reedy category.
That would be interesting! More generally, it would be very interesting to see any kind of serious work along these lines in abstract homotopy theory, namely working in an axiomatic framework that captures both simplicial and cubical sets.
In one of his papers Clemens Berger mentions a notion of a “geometric Reedy category” that he tried to develop together with Cisinski that was supposed to do something like that. I asked him about it and from what he told me it seemed that the project didn’t get too far and that their ideas weren’t particularly compatible with the subdivision/$\Ex$ approach. This is a problem that I occasionally ponder idly but somehow it never takes off…
Personally, I feel that this distinction should go to $\Delta$ but that’s just based on my own astonishment at how neat and elegant simplicial homotopy theory is.
I hope to eventually convince people reading that cubical homotopy theory is just as neat and elegant! Indeed, I would even argue that cubical homotopy is still more elegant, because there is an extra level of structure which one can make use of to construct cubical sets and morphisms between them canonically, rather than writing out explicit formulae and checking that relations hold. I should say, though, that one can certainly work in this way with cubical sets too.
In particular, I find that working cubically allows one to formally ’figure things out in low dimensions (where one can draw pictures), and then abstract from this to all dimensions’, which of course is how one works in practise in simplicial homotopy theory (or, perhaps, I should say, ’foundational simplicial homotopy theory’, namely before one has developed enough tools to be able to work with a ’higher level language’).
If I try to think about it in an unbiased way I don’t see any clear advantages of either approach. In both cases we start with some basic notion of a 1-dimensional homotopy and we follow some pattern of generating notions of homotopies of higher dimensions, both look equally ad hoc to me. I see where you are coming from with the universal property of $\square$ but the choice of a monoidal category as the basic structure seems just as arbitrary as the choice of a Reedy category.
I agree that what you write in the second sentence is the heart of the matter. I personally do find the data of an interval and a monoidal structure to be more natural than the notion of a Reedy category for capturing this idea, though. Having an interval and a monoidal structure is a direct abstraction from $\mathsf{Top}$, once one notices that the fact that the monoidal structure in $\mathsf{Top}$ is cartesian is not necessary for the development of homotopy theory: we just need certain structures to exist and to interact well with the monoidal structure. In particular, we will have a functor out of our category of shapes whenever we have an appropriate interval in some other monoidal category, which I feel to be very significant: I don’t see the structure of a Reedy category as giving us the possibility to construct functors out of it.
But I do not have any precise way to formulate the sense in which I feel that the category of cubes should be considered ’universal’ amongst categories of shapes, so can only give ’philosophical’ arguments such as these!
This is a problem that I occasionally ponder idly but somehow it never takes off…
Thanks for mentioning this! I would certainly be very interested in developing an abstract notion of ’category of shape’, and it is definitely something that I would like to think about in the future. If I do so, I’ll let you know!
Having an interval and a monoidal structure is a direct abstraction from $\mathsf{Top}$, once one notices that the fact that the monoidal structure in $\mathsf{Top}$ is cartesian is not necessary for the development of homotopy theory: we just need certain structures to exist and to interact well with the monoidal structure.
Again, the choice of the monoidal structure of $\mathsf{Top}$ as the starting point is arbitrary. I could equally well generate higher homotopies by using factorizations in $\mathsf{Top}$ which would lead to me to a Reedy type structure. However, I think that it will be more productive to let you go on with your story rather than do a full on rebuttal. I’m looking forward to the continuation of your write up.
Again, the choice of the monoidal structure of Top as the starting point is arbitrary.
Yes, I would agree with that. When looking for an axiomatic framework, one of course has to start somewhere, in a way which is going to be a matter of taste and efficacy (whether it will lead to a good theory). I personally find developing homotopy theory in the setting of structured intervals/cylinders/co-cylinders together with a monoidal structure very satisfactory, but certainly what I wrote about finding the monoidal structure of the category of cubes more natural than its Reedy structure is a consequence of, or at least very closely tied to, this point of view. I agree entirely that one may well be able to make a convincing argument for a different point of view.
Maybe a better illustration of the difference I see between the monoidal and Reedy settings is that everything in the monoidal setting is built up from a handful of objects and arrows that are part of the structure, whereas in the Reedy setting one needs to know something about all arrows as part of the structure (this is also the case with the cylindrical approach to abstract homotopy theory of Kamps, which relies upon ’Kan-like conditions’). But I completely agree that there will not be an absolute reason why the one should be considered preferable over the other: one will only be able to give justifications that take certain things as common ground.
I’m looking forward to the continuation of your write up.
Thank you! My apologies for the delay, a few things cropped up, but I have nearly finished preparing the next posts now. I’m not quite sure when I’ll get the chance to put the finishing touches, but at the latest it should be early next week.
I would just like to add that I’m enjoying reading the installments of this mathematical serial. I’m also particularly interested to hear your thoughts, Richard, on the choice of the monoidal rather than the cartesian cube category on an interval. It seems to me that the latter has many advantages as well.
Thank you for the encouragement, Ulrik!
It is taking a bit longer than expected to finish off the next post, because I will go a little further in that post than originally planned, but it’ll be ready soon.
I’m also particularly interested to hear your thoughts, Richard, on the choice of the monoidal rather than the cartesian cube category on an interval. It seems to me that the latter has many advantages as well.
Thank you for the interesting question! In short, I agree with you!
On the one hand, the free cartesian category on $\square_{\leq 1}$ with unit $I^{0}$, let us denote it by $\square^{\mathsf{cart}}$ is a ’decorated category of cubes’ (i.e. similar to $\square$ but with extra structure). From this point of view, the same remarks apply as in #9: it is harder to construct functors out of it than out of $\square$. However, this does not matter, because $\square^{\mathsf{cart}}$ has its own universal property, which makes it just as easy to construct functors out of it.
Moreover, cubical homotopy theory with respect to this category would seem to me to be very well suited to constructing models of type theories. The cartesian monoidal structure on $\mathsf{Set}^{(\square^{\mathsf{cart}})^{op}}$ would have the same nice conceptual properties as the non-cartesian monoidal structure on cubical sets, that I was advocating the use of for constructing models of type theory in this discussion, but would also allow one to model type theory in the usual way which one can with a cartesian monoidal structure.
At the moment, I also see no reason why the work I am outlining on the homotopy hypothesis would not go through for this category. It is crucial that the monoidal structure we work with is ’topological’, namely the tensor product of an $m$-cube and an $n$-cube is an $(m+n)$-cube, but this would be the case for presheaves on $\square^{\mathsf{cart}}$.
Indeed the only advantage that I can see of $\square$ over $\square^{\mathsf{cart}}$ is the obvious one that it interacts well with more general categories (this is just the difference in generality between an arbitrary monoidal structure and a cartesian one).
It is interesting to ponder how $\square^{\mathsf{cart}}$ would fit into a formalism for describing ’shape categories’ appropriate for homotopy theory, that Karol and I have been discussing. It may for instance be that, rather than consider just ’decorated categories of cubes’, one should consider more general ’decorated free structures’ on $\square_{\leq 1}$. Maybe one can even work with quite general 2-monads on $\mathsf{Cat}$, rather than just those describing monoidal-ness or cartesian-ness. I have not thought about this at all, but it is something to keep in mind!
(Completed on the 2nd of March, but posted on the 9th of March, as the nForum was down from earlier on the 2nd until some time on the 8th. This post will be spread over a large number of entries).
Continuing from #21, I’ll now begin working towards the proof of the result mentioned in that post.
Let us denote by $\alpha$ the natural transformation
which is part of the data of the colimit defining $\mathsf{Ex}^{\infty}$.
Let $\mathcal{A}$ be a co-complete monoidal category, and let $\underline{\mathsf{I}} = (\mathsf{I},i^{\mathcal{A}}_{0},i^{\mathcal{A}}_{1},p^{\mathcal{A}})$ be an interval in $\mathcal{A}$ equipped with a contraction structure, in the sense of VI of my thesis. The following defines a functor
which I’ll denote by $\left| - \right|_{\leq 1}$.
1) To $I^{0}$, we associate the unit object $1$ of the monoidal structure of $\mathcal{A}$.
2) To $I^{1}$, we associate the object $\mathsf{I}$ of $\mathcal{A}$.
3) To the arrows $i_{0}$, $i_{1}$, and $p$ of $\square_{\leq 1}$, we associate the arrows $i_{0}^{\mathcal{A}}$, $i_{1}^{\mathcal{A}}$, and $p^{\mathcal{A}}$ of $\mathcal{A}$ respectively.
By means of the universal property of $\square$, the functor
gives rise to a functor as follows.
By means of the universal property of $\mathsf{Set}^{\square^{op}}$ as a free co-completion, the functor $\left| - \right|_{\square}$ gives rise to a functor as follows.
Before constructing the natural transformations $\rho_{n}$, let us first explore the idea. Of greatest significance is the idea behind the definition of the natural transformation
at the level of 1-cubes, which is as follows. Given a cubical set $X$, recall that a 1-cube $z$ of $\mathsf{Ex}_{1}(X)$ is a zig-zag of 1-cubes of $X$ as shown below.
We wish to send $z$ to the 1-cube of $S\big( \left| X \right| \big)$ corresponding to the path in $\left| X \right|$ given by $g^{-1} \cdot f$. In other words, we reverse the path in $\left| X \right|$ corresponding to $g$, and then glue it to the end of the path in $\left| X \right|$ corresponding to $f$. The involution structure precisely allows us to ’reverse’ paths, and the subdivision structure precisely allows us to ’glue’ them.
It is not clear to me whether it is possible to modify $\square$ in order to be able to work with $X$ instead of $S\big( \left| X \right| \big)$. We could require that cubical sets have involutions, which would allow to reverse 1-cubes in $X$, but to build a subdivision structure into an interval, one would have to do so as an absolute pushout, which seems tricky. In any case, it would take quite a lot of work to construct functors out of such a modified $\square$.
One of the main technical ideas in the proof I will give is that there is no need for such a modification of $\square$: to ’replace $X$ by $S\big( \left| X \right| \big)$’ allows us to make sense of ’reversing and glueing’ 1-cubes (and indeed $n$-cubes for any $n$). More generally, this replacement ’makes any structures in $\mathcal{A}$ available inside $\mathsf{Set}^{\square^{op}}$’. This is one aspect of what I was getting at in the fourth paragraph of my reply to Karol in #9.
The simple idea for the definition of $\rho_{1}$ at the level of 1-cubes described above does not quite work when we do not have strictness of right identities. Indeed, the obvious natural transformation
to choose for $\rho_{0}$ is the unit natural transformation coming from the adjunction between $S$ and $\left| - \right|$. However, the diagram
does not then necessarily commute. To see this, let
be a 1-cube of $X$. Taking the longer route through the triangle
gives, noting that the reverse of a constant path is constant since the involution structure $v^{\mathcal{A}}$ is compatible with $p^{\mathcal{A}}$, the path $c_{x_{1}} \cdot f$, namely the constant path at $x_{1}$ glued to the end of $f$. Since we do not necessarily have strictness of right identities, this path is not necessarily $f$ on the nose, whilst $f$ is the path that we obtain by taking the shorter route through the triangle.
Let us now discuss how we can get around this difficulty. We will now assume that our subdivision structure is compatible with $p^{\mathcal{A}}$, in the sense of VI of my thesis. This condition is much weaker than strictness of right identities: it says that the glueing together two constant paths gives a constant path. This of course holds for the interval in $\mathsf{Top}$.
We tweak $\rho_{0}$ as follows: we send a 1-cube
of $X$ to the 1-cube of $S\big( \left| X \right| \big)$ corresponding to the path $c_{x_{1}} \cdot f$ in $\left| X \right|$.
We then tweak $\rho_{1}$ as follows: we send a 1-cube of $\mathsf{Ex}_{1}(X)$, namely a zig-zag
of 1-cubes of $X$, to the 1-cube of $S\big( \left| X \right| \big)$ corresponding to the path $(c_{x_{2}} \cdot g^{ -1}) \cdot f$ in $\left| X \right|$.
We then tweak $\rho_{2}$ as follows: we send a 1-cube of $\mathsf{Ex}_{2}(X)$, namely a zig-zag
of 1-cubes of $X$, to the 1-cube of $S\big( \left| X \right| \big)$ corresponding to the path $\Big( \big( c_{x_{4}} \cdot (g_{2}^{-1} \cdot f_{2} ) \big) \cdot g_{1}^{-1} \Big) \cdot f_{1}$ in $\left| X \right|$.
We then tweak $\rho_{3}$ as follows: we send a 1-cube of $\mathsf{Ex}_{3}(X)$, namely a zig-zag
of 1-cubes of $X$, to the 1-cube of $S\big( \left| X \right| \big)$ corresponding to the path $\bigg( \Big( \big( c_{x_{6}} \cdot (g_{3}^{-1} \cdot f_{3}) \big) \cdot \big( g_{2}^{-1} \cdot f_{2} \big) \Big) \cdot g_{1}^{-1} \bigg) \cdot f_{1}$ in $\left| X \right|$.
We then tweak $\rho_{n}$ for every $n \geq 4$ in a similar way: we send a 1-cube of $\mathsf{Ex}_{n}(X)$, namely a zig-zag
of $2n$ 1-cubes of $X$, to the path constructed in the same way as the path to which the zig-zag obtained by ’chopping off’ $f_{n}$ and $g_{n}$ is sent under $\rho_{n-1}(X)$, except that the constant path $c_{x_{2(n-1)}}$ is replaced by a bracket with $c_{x_{2n}} \cdot (g_{n}^{-1} \cdot f_{n})$ inside.
It is crucial to get the bracketing in the paths we have just described right, since (think again of $\mathsf{Top}$) glueing of paths is not in general associative on the nose.
There is a different possibility for getting around the lack of strictness of identities. Instead of working with $\mathsf{Ex}^{\infty}$, we could work with the homotopy colimit of the diagram used to define $\mathsf{Ex}^{\infty}$, namely the homotopy colimit of the following diagram.
By ’homotopy colimit’ here, I mean that we take the (ordinary!) colimit of the modification of the diagram above in which we ’insert a cylinder’ at every step: we replace the natural transformation
by the following diagram of natural transformations
and replace the natural transformation
for every $n \geq 1$ by the following diagram of natural transformations.
Let us denote the homotopy colimit, in this sense, of the diagram
by $\mathsf{Ex}^{\infty}_{h}$.
Assuming that $\underline{\mathsf{I}}$ is equipped with what Grandis terms a ’zero collapse structure’ in the paper Categorically algebraic foundations for homotopical algebra, which gives a means to construct a homotopy between $c_{x_{1}} \cdot f$ and $f$ for a 1-cube
of $X$, we will be able to construct a map from $\mathsf{Ex}_{h}^{\infty}(X)$ to $S\big( \left| X \right| \big)$.
For every cubical set $X$, I believe it possible to demonstrate that
is a cofibration, in the sense of VIII of my thesis, if $\underline{\mathsf{I}}$ is equipped with a certain structure, and, given this same structure, that
is a cofibration.
It should then follow that
is a homotopy equivalence for any cubical set $X$, where
is the canonical morphism of cubical sets.
However, I will not follow this approach. Instead, I follow the simpler ’tweaking’ method that I described first: I wish to give as ’down to earth’ a proof as possible, which can hopefully give people a clear understanding of why we should expect
to be a homotopy equivalence for any cubical set $X$.
Let us now embark upon the formal construction of the natural transformations $\rho_{n}$. As mentioned, we now assume that $\underline{\mathsf{I}}$ is equipped with an involution structure $v^{\mathcal{A}}$ compatible with $p^{\mathcal{A}}$, and a subdivision structure $(\mathsf{S},r^{\mathcal{A}}_{0},r^{\mathcal{A}}_{1},s^{\mathcal{A}})$ compatible with $p^{\mathcal{A}}$, in the sense of VI of my thesis.
Let us first work towards defining $\rho_{0}$.
Let us denote by
the canonical arrow of $\mathcal{A}$ such that the following diagram in $\mathcal{A}$ commutes.
We define a natural transformation
in the following way.
1) To the object $I^{0}$, we associate the following identity arrow.
2) To the object $I^{1}$, we associate the arrow
of $\mathcal{A}$.
It is straightforward to check that the three diagrams that must commute do indeed commute (for the diagram involving $p^{\mathcal{A}}$, we appeal to our assumption that the subdivision structure $(\mathsf{S},r_{0}^{\mathcal{A}},r_{1}^{\mathcal{A}},s^{\mathcal{A}})$ is compatible with $p^{\mathcal{A}}$).
By means of the 2-universal property of $\square$, the natural transformation $\tau_{0}^{\leq 1}$ gives rise to a natural transformation as follows.
By means of the 2-universal property of free co-completion, the natural transformation $\tau_{0}^{\square}$ gives rise to a natural transformation as follows.
Let us denote by $\eta_{\mathcal{A}}$ the unit natural transformation
of the adjunction between $S$ and $\left| - \right|$.
We define $\rho_{0}$ to be the natural transformation $(S \cdot \tau_{0}) \circ \eta_{\mathcal{A}}$. In other words, the following diagram commutes.
Here $S \cdot \tau_{0}$ is the natural transformation obtained by whiskering the following diagram.
Let us now work towards defining $\rho_{1}$. I will for the time being use the original notation $\mathsf{Ex}$ and $\mathsf{Sd}$ instead of $\mathsf{Ex}_{1}$ and $\mathsf{Sd}_{1}$, and the same in similar cases. When we come to work towards defining $\rho_{n}$ for $n \geq 2$, we’ll return to the notation $\mathsf{Ex}_{n}$ and $\mathsf{Sd}_{n}$.
Let us denote by
the canonical arrow of $\mathcal{A}$ such that the following diagram in $\mathcal{A}$ commutes.
Let us denote by
the canonical arrow of $\mathcal{A}$ such that the following diagram in $\mathcal{A}$ commutes.
We define a natural transformation
in the following way.
1) To the object $I^{0}$, we associate the following identity arrow.
2) To the object $I^{1}$, we associate the arrow
of $\mathcal{A}$.
It is straightforward to check that the three diagrams that must commute do indeed commute (for the diagram involving $p$, we appeal to both our assumption that the subdivision structure $(\mathsf{S},r_{0}^{\mathcal{A}},r_{1}^{\mathcal{A}},s^{\mathcal{A}})$ is compatible with $p^{\mathcal{A}}$ and that the involution structure $v^{\mathcal{A}}$ is compatible with $p^{\mathcal{A}}$).
Noting that it is the functor
to which the functor $\left| \mathsf{Sd}_{\leq 1}(-) \right|$ gives rise by means of the universal property of $\square$, the natural transformation $\tau_{1}^{\leq 1}$ gives rise, by means of the 2-universal property of $\square$, to a natural transformation as follows.
Noting that it is the functor
to which the functor
gives rise by means of the universal property of free co-completion, the natural transformation $\tau_{1}^{\square}$ gives rise, by means of the 2-universal property of free co-completion, to a natural transformation as follows.
Let us denote by $\epsilon_{\mathcal{A}}$ the co-unit natural transformation
of the adjunction between $S$ and $\left| - \right|$.
Let us denote by $\epsilon$ the co-unit natural transformation
of the adjunction between $\mathsf{Sd}$ and $\mathsf{Ex}$.
Let us denote by $\tau_{1}^{\mathsf{adj}}$ the natural transformation
given by the composition of four natural transformations on the longer route around the following triangle.
In other words, this triangle commutes.
Here $\eta_{\mathcal{A}} \cdot (\mathsf{Ex} \circ S)$ is the natural transformation obtained by whiskering the following diagram.
The natural transformation $S \cdot \tau_{1} \cdot (\mathsf{Ex} \circ S)$ is that obtained by whiskering the following diagram.
The natural transformation $(S \circ \left| - \right|) \cdot \epsilon \cdot S$ is that obtained by whiskering the following diagram.
The natural transformation $S \cdot \epsilon_{\mathcal{A}}$ is that obtained by whiskering the following diagram.
This construction of $\tau_{1}^{\mathsf{adj}}$ given $\tau_{1}$ is the canonical procedure for obtaining a natural transformation between right adjoints given a natural transformation between left adjoints, noting that $\epsilon_{\mathcal{A}}) \circ \big( \left| - \right|) \cdot \epsilon \cdot S \big)$ is the co-unit for the adjunction between $\left| \mathsf{Sd} \right|$ and $\mathsf{Ex} \circ S$.
We define
to be the natural transformation given by $(\tau_{1}^{\mathsf{adj}} \cdot \left| - \right|) \circ (\mathsf{Ex} \cdot \eta_{\mathcal{A}})$. In other words, the following diagram commutes.
Here $\eta_{\mathcal{A}} \cdot \mathsf{Ex}$ is the natural transformation obtained by whiskering the following diagram.
The natural transformation $\tau_{1}^{\mathsf{adj}} \cdot \left| - \right|$ is obtained by whiskering the following diagram.
Having now defined $\rho_{0}$ and $\rho_{1}$, let us prove that the diagram
commutes.
The heart of the matter is to demonstrate that the following diagram commutes.
We proceed as follows.
1) The following diagram commutes.
2) The following diagram commutes.
That the triangle
commutes holds by our assumption that $v^{\mathcal{A}}$ is compatible with $p^{\mathcal{A}}$.
3) By 1) and 2), the following diagram commutes.
4) Let
be the natural transformation of VI.18 in my thesis, with respect to $(\mathsf{S}, r_{0}^{\mathcal{A}}, r_{1}^{\mathcal{A}}, s^{\mathcal{A}})$ and $p^{\mathcal{A}}$. By definition, the following diagram commutes.
Hence the following diagram commutes.
5) By the universal property of a co-cartesian square, we deduce from 3) and 4) that the following diagram commutes.
6) By our assumption that $(\mathsf{S}, r_{0}^{\mathcal{A}}, r_{1}^{\mathcal{A}}, s^{\mathcal{A}})$ is compatible with $p^{\mathcal{A}}$, the following diagram commutes.
7) We deduce from 5) and 6) that the following diagram commutes.
8) We deduce from 7) and the definition of the arrow $o$ that the following diagram commutes.
9) By definition of $o$ and $q$, the following diagram commutes.
10) By 8) and 9), the following diagram commutes.
11) By definition of $q_{r}$, the following diagram commutes.
12) By the universal property of a co-cartesian square, we deduce from 10) and 11) that the following diagram commutes.
13) We deduce from 12) that the following diagram commutes.
In other words, the following diagram commutes.
14) In addition, the following diagram commutes.
15) We conclude from 13) and 14) that the following diagram commutes.
16) Noting that it is the natural transformation
to which the natural transformation
gives rise by means of the 2-universal property of $\square$ and the 2-universal property of free co-completion, we conclude from 15) that the following diagram commutes, as we wished to show.
The remainder of our proof that the diagram
commutes will be a reduction to the diagram
whose commutativity we have just established.
To carry out this reduction, we will need a few observations which hold in an arbitrary strict 2-category $\mathcal{C}$.
1) Let
be a 2-arrow of $\mathcal{C}$, and let
be a 2-arrow of $\mathcal{C}$. Then the following diagram commutes.
Let us demonstrate this. By definition, $\zeta_{1} \circ \zeta_{0}$ is obtained by pasting the 2-arrows in the following diagram. I have omitted the label of the 1-arrow in the middle, which is the identity.
Since
is an identity for horizontal composition of 2-arrows, we deduce that $\zeta_{1} \circ \zeta_{0}$ is obtained by pasting the 2-arrows in the following diagram. Both of the 1-arrows in the middle are the identity.
Since
is by definition an identity for vertical composition of 2-arrows, we deduce that $\zeta_{1} \circ \zeta_{0}$ is obtained by pasting the 2-arrows in the following diagram.
Appealing to the fact that
is by definition an identity for vertical composition, and similarly that
is by definition an identity for vertical composition, we deduce that $\zeta_{1} \circ \zeta_{0}$ is obtained by pasting the 2-arrows in the following diagram. The leftmost of the two 1-arrows in the middle is $f_{1}$, and the rightmost is $f_{0}$.
Carrying out the pasting of these 2-arrows first horizontally and then vertically, we deduce that $\zeta_{1} \circ \zeta_{0}$ is obtained by pasting the 2-arrows in the following diagram, as we wished to show.
2) Let
be a 2-arrow of $\mathcal{C}$, let
be a 2-arrow of $\mathcal{C}$, and let
be a 1-arrow of $\mathcal{C}$. Then the following diagram commutes.
Let us demonstrate this. We make the following observations.
I) We have that $(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0})$ is obtained by pasting the following 2-arrows. The 1-arrow in the middle is $g$.
By definition of $g \cdot \zeta_{1}$ and $g \cdot \zeta_{0}$, we deduce that $(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0})$ is obtained by pasting the 2-arrows in the following diagram. The leftmost of the 1-arrows in the middle is the identity, and the rightmost is $g$.
By 1), we deduce that $(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0})$ is obtained by pasting the 2-arrows in the following diagram. The first from the left of the 1-arrows in the middle is $f_{1}$, the second is $f_{0}$, and the third is $g$.
II) Pasting together the 2-arrows
we obtain $g \cdot \zeta_{0} \cdot f_{1}$.
III) Pasting together the 2-arrows
gives the following 2-arrow.
Pasting together the 2-arrows
thus gives the 2-arrow obtained by pasting together the following 2-arrows, which is $(g \circ f_{0}) \cdot f_{1}$.
It follows from I) - III) that $(g \cdot \zeta_{1}) \circ (g \cdot \zeta_{0})$ is obtained by pasting the following 2-arrows, as we wished to show. The 1-arrow in the middle is $g \circ f_{0} \circ f_{1}$.
3) Let
be a 2-arrow of $\mathcal{C}$, and let
be a 2-arrow of $\mathcal{C}$. Then the following diagram commutes.
Let us demonstrate this. We make the following observations.
I) We have that $(\zeta_{1} \cdot f_{1}) \circ \zeta_{0}$ is obtained by pasting the following 2-arrows. The middle 1-arrow is $f_{1}$.
Since
is an identity for horizontal composition, we deduce, appealing to the definition of $\zeta_{1} \cdot f_{1}$, that $(\zeta_{1} \cdot f_{1}) \circ \zeta_{0}$ is obtained by pasting the following 2-arrows. The leftmost 1-arrow in the middle is $f_{1}$, and the rightmost is the identity.
II) We obtain the same 2-arrow, namely $\zeta_{0}$, by pasting of the 2-arrows
as by pasting the following 2-arrows.
III) We obtain the same 2-arrow, namely $\zeta_{1}$, by pasting of the 2-arrows
as by pasting the following 2-arrows.
Carrying out the pasting of the 2-arrows
by composing first vertically and then horizontally, we deduce that $(\zeta_{1} \cdot f_{1}) \circ \zeta_{0}$ is obtained by pasting the following 2-arrows.
Carrying out this pasting by composing first horizontally and then vertically, we conclude that $(\zeta_{1} \cdot f_{1}) \circ \zeta_{0}$ is obtained by pasting the following 2-arrows, as we wished to show. The 1-arrow in the middle is $f_{2} \circ f_{0}$.
4) Let
be a 2-arrow of $\mathcal{C}$, let
be a 2-arrow of $\mathcal{C}$, and let
be a 1-arrow of $\mathcal{C}$. Then the following diagram commutes.
Let us demonstrate this. We make the following observations.
I) We have that $(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big)$ is obtained by pasting the following 2-arrows. The middle 1-arrow is $f \circ f_{1} \circ g_{0}$.
II) The 2-arrow
can be obtained by pasting together the following 2-arrows.
III) We deduce from I) and II), by the definition of the 2-arrows which make up the pasting diagram in I), that $(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big)$ is obtained by pasting the following 2-arrows.
IV) We obtain the same 2-arrow, namely $\zeta_{0}$, by pasting of the 2-arrows
as by pasting the following 2-arrows.
V) We obtain the same 2-arrow, namely $\zeta_{1}$, by pasting of the 2-arrows
as by pasting the following 2-arrows.
VI) By III) - V), we conclude that $(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big)$ is obtained by pasting the following 2-arrows.
VII) By pasting the 2-arrows
we obtain the following 2-arrow.
VIII) By pasting the 2-arrows
we obtain the following 2-arrow.
Pasting the 2-arrows
we thus obtain the following 2-arrow.
By VI) - VIII), we conclude that $(f \cdot \zeta_{1} \cdot g_{0}) \circ \big( (f \circ f_{1}) \cdot \zeta_{0} \big)$ is obtained by pasting the following 2-arrows, as we wished to show.
5) Let
be a 2-arrow of $\mathcal{C}$, and let
be a 2-arrow of $\mathcal{C}$. Then the following diagram commutes.
This follows immediately from 4). Indeed, we let $f_{0}$, $f_{1}$, and $f$ in 4) all be
We let $g_{0}$ in 4) be the 1-arrow $f_{1}$ that we have here, and let $g_{1}$ in 4) be the 1-arrow $f_{0}$ that we have here. We let $\zeta_{0}$ in 4) be the 2-arrow $\zeta_{1}$ that we have here, and let $\zeta_{1}$ in 4) be the 2-arrow $\zeta_{0}$ that we have here.
6) Let
be a 2-arrow of $\mathcal{C}$, and let
be a 2-arrow of $\mathcal{C}$. Then the following diagram commutes.
This follows immediately from 4). Indeed, we let $f_{0}$ in 4) be the 1-arrow $f_{0}$ that we have here, and let both $f_{1}$ and $f$ in 4) be
We let $g_{0}$ and $g_{1}$ in 4) be the 1-arrows $g_{0}$ and $g_{1}$ that we have here respectively. We let $\zeta_{0}$ and $\zeta_{1}$ in 4) be the 2-arrows $\zeta_{0}$ and $\zeta_{1}$ that we have here respectively.
We can now begin our demonstration that the diagram
commutes.
1) The following diagram commutes.
The first square from the top commutes by 2) in #41. The second commutes by 3) in #42. The third commutes by 4) in #43. The fourth commutes by 4) in #43.
2) The following diagram commutes.
The first square from the top commutes by 5) in #44. The second commutes by 6) in #44. The third commutes by 4) in #43.
3) By 1) and 2), we have that the following diagram commutes.
The two unlabelled arrows (omitted for lack of space) are as follows.
4) Since $\eta$ and $\epsilon$ are the unit and counit natural transformations of the adjunction between $\mathsf{Sd}$ and $\mathsf{Ex}$, the following diagram commutes.
Hence the following diagram commutes.
5) By 3) and 4), the following diagram commutes.
6) The following diagram commutes.
The first square from the top commutes by 3) in #42. The second commutes by 4) in #43. The third also commutes by 4) in #43.
7) Since $\eta_{\mathcal{A}}$ and $\epsilon_{\mathcal{A}}$ are the unit and counit natural transformations of the adjunction between $S$ and $\left| - \right|$, the following diagram commutes.
Hence the following diagram commutes.
8) By 6) and 7), the following diagram commutes.
9) We demonstrated earlier that the diagram
commutes. Hence the following diagram commutes.
10) We deduce from 8) and 9) that the following diagram commutes.
11) We conclude from 5) and 10) that the following diagram commutes.
In other words, the following diagram commutes, as we wished to show.
In the next post, I’ll construct the natural transformations $\rho_{n}$ for $n \geq 2$, and thereafter the natural transformation $\rho$ that we are aiming for.
This concludes the post which began with #32.
1 to 45 of 45