# How to be concrete when you don’t have a choice

I forgot to write a post about this a year ago, but I gave a talk at AustMS2020 detailing some work that Martti Karvonen and I did, originating in a discussion on the category theory Zulip chat server. The main gist of the project is removing the need for Global Choice from a pair of theorems in pure category theory dealing with concrete and non-concrete categories. The most famous example (shown by Freyd) of a non-concrete locally small category is the homotopy category of $\mathbf{Top}$, which is the category whose objects are topological spaces, but whose morphisms are homotopy classes of continuous maps. It is a quotient of the concrete category of topological spaces, by a congruence on its hom-sets. The first theorem that we improved, due to Kučera, is that this is as bad as it gets: every locally small category is the quotient of a concrete category by a congruence like this. The proof constructs a concrete category, but it’s not very nice or workable, so it’s really just an existence result.

Unfortunately the original proof starts by well-ordering the universe of sets, which really makes me itch: category theory is generally rather constructive in nature, or at least can be reformulated to have some kind of constructive content. A purely category-theoretic statement that needs the axiom of Global Choice seems non-optimal to me. And, thankfully, this is the case. Martti came up with a way to remove Choice (even normal AC) from the construction, and then I figured out how to do the whole thing in Algebraic Set Theory with the assumption of Excluded Middle (i.e. the category with class structure is Boolean).

Then we turned out attention to a theorem of Freyd that gives a precise characterisation of which categories are concretizable, albeit we started from Vinárek’s cleaner and shorter proof. It shows that a necessary condition for concreteness, due to Isbell, is also sufficient. Isbell gave examples of non-concretizable categories, but they were artificial, specifically constructed to violate his condition. Like Kučera’s theorem, even Vinárek’s improved proof used Global Choice to pick a well-ordering of the universe. We were able to re-do the theorem in ZF, and more generally in (Boolean) algebraic set theory, with the additional assumption that the universal object has a well-ordered stratification by small objects (roughly, it has a small map to the object of ordinals). This last assumption is validated in any membership-based set theory where some cumulative hierarchy exhausts the class of all sets, say the von Neumann hierarchy for ZF, or some weaker set theories where a hierarchy, or a rank function, is posited axiomatically (see eg this paper).

The paper is in preparation, and would have been done by now, had I not been distracted by other projects. Martti is being very patient with me! For now, let me point to the slides for my talk, which you can see here.

# Substructural fixed-point theorems and the diagonal argument: theme and variations

This is just to give a pre-release sneak peek of a pre-preprint I want to put on the arXiv very shortly. It’s a slightly odd beast, since I think it might be of some interest to logicians/philosophers, computer science types and possibly also category theorists, but I can’t tell. It’s a further analysis of Lawvere’s diagonal argument/fixed point theorem, reducing the assumptions beyond what is probably sensible, and giving a few different versions of the fixed point theorem more general than Lawvere’s. Here’s the abstract:

This note generalises Lawvere’s diagonal argument and fixed-point theorem for cartesian categories in several ways. Firstly, by replacing the categorical product with a general, possibly incoherent, magmoidal product with sufficient diagonal arrows. This means that the diagonal argument and fixed-point theorem can be interpreted in some substructural type theories, and semantically in categories with a product functor satisfying no coherence axioms, for instance relevance categories. The second way is by showing that both of Lawvere’s theorems as stated for cartesian categories only concern the well-pointed quotient, and giving a version of the fixed-point theorem in the internal logic of an arbitrary regular category. Lastly, one can give a uniform version of the fixed-point theorem if the magmoidal category has the appropriate endomorphism object, and has a comonad (i.e. an (S4) necessity modality) allowing for potentially `discontinuous’ dependence on the initial data.

Perhaps it is just a bit of a curio, and really waiting for a killer app, but it’s been sitting on my plate for a while, and I think some level of feedback is warranted, since I really can’t tell how it will land with people inside and outside my sphere of expertise. Grab your copy here.

# Correction to the definition of the String crossed module, part 4: the coherence equation

In the last post I showed that the paper BCSS contains a contradictory definition, namely of a particular 1-form $\beta_p$, and that flipping the sign out the front fixes it up. now I need to make sure that I ensure the main theorem is still valid, since it implicitly depends on that sign, through the conclusion of Proposition 3.1. My claim in the first post in this series is that the issue is hiding in equation (5) of BCSS, whereas Urs Schreiber cautioned me that the equation should be checked against the $L_\infty$-algebra literature, rather than just aiming for internal consistency. In particular the paper “Strongly homotopy Lie algebras” by Lada–Markl (arXiv), which is the cited source for the definition and conventions for $L_\infty$-algebras. The definition that needs to be used is that of ‘weak map’, except the description is slightly indirect, and there are several layers of interacting sign conventions that I felt I was going to come unstuck on. In this post I will deal with my workaround to arrive at what I hope is a definitive answer.

Continue reading “Correction to the definition of the String crossed module, part 4: the coherence equation”

# Correction to the definition of the String crossed module, part 3: arriving at the contradiction, and the fix

Continuing on from the previous post, I need to finish off the calculation that shows the definition of the 1-form

$\beta_p = -2\int_0^{2\pi} \langle \Theta,p(\theta)^{-1}\partial_\theta p(\theta)\rangle\,d\theta \in \Omega^1(P\Omega G)$

in BCSS leads to a contradiction, for $G$ a suitable compact connected Lie group, taken to be $SU(2)$ for concreteness. Recall that I had calculated the difference between a pair of connections on the $U(1)$-bundle $\widehat{\Omega SU(2)}\to \Omega SU(2)$, one arising from the construction of Murray and Stevenson, and the other being the pullback of this along the lift of $Ad_p\colon \Omega SU(2) \to \Omega SU(2)$ for $p$ a path in $SU(2)$ starting at the identity matrix. This lift is defined in BCSS using $\beta_p$. In actual fact, we did the calculation on the trivial bundle over $P\Omega SU(2)$ that is the pullback of the one I care about, and arrived at the formula

$ev_{2\pi}^*(\widehat{Ad}_p^*\mu - \mu - \beta_p) = 2\int_{[0,2\pi]}ev^*(d\beta_p)$

where $ev_{2\pi}\colon P\Omega SU(2)\to \Omega SU(2)$ evaluates a path at the endpoint. I can show that for a careful choice of $p$, path $f\colon [0,2\pi]\to \Omega SU(2)$ and tangent vector at $f$ that is vertical for $ev_{2\pi}$, the right hand side fails to vanish. The left hand side is identically zero for vertical tangent vectors, and this will be the contradiction.

Continue reading “Correction to the definition of the String crossed module, part 3: arriving at the contradiction, and the fix”

# Correction to the definition of the String crossed module, part 2: triangulation

After the previous post was shared on Twitter, and I tagged Urs Schreiber, one of the authors of the paper in question (‘BCSS‘), he rightly pointed out that I had merely found a discrepancy in the coherence equations between BCSS and HDA VI. The true source of equation (5) of BCSS (which I claimed last time was in error) should be, he says, the theory of weak maps of $L_\infty$ algebras, going back to Lada and Markl’s Strongly homotopy lie algebras (or free arXiv version). I totally agree with this point, but I felt daunted by having to unwind the various definitions that unravel to equation (5). So I wanted to explore the issue a bit more. I know that the sign in front of the 1-form

$\beta_p = -2\int_0^{2\pi} \langle \Theta,p(\theta)^{-1}\partial_\theta p(\theta)\rangle\,d\theta$

in the proof of Proposition 3.1 cannot be correct, since it leads to a contradiction in a geometric calculation independent of all the $L_\infty$-algebra material. I should note that this geometric calculation is nothing exotic; a correspondent let me know I muddied the water in the previous post by discussing it in the context of a larger project with more novel constructions. As a result, I will give the calculation later below the fold.

What I did not realise when I wrote the first post is that the sign error in $\beta_p$ is linked not only the an overall sign in equation (5) of BCCS, but also to a plus sign implicit in the definition of the comparison functor from 2-term $L_\infty$-algebras to (semistrict) Lie 2-algebras, which are possibly weak Lie algebra objects in the 2-category of groupoids internal to $\mathbf{Vect}$. This functor is constructed in HDA VI, in Theorem 4.3.6 (=Theorem 36 in the arXiv version), and here is the relevant version

This was invisible to me, until I checked a different article generalising HDA VI, namely Roytenberg’s On weak Lie 2-algebras (or free arXiv version), where a generalisation of the comparison functor to weaker objects is given. Here is included a minus sign on what turns out to be the troublesome piece of data arising from the crossed module of Lie algebras, arising from the sign on $\beta_p$.

So now in fact one can see the sign on $\beta_p$ as being a combination of two signs: one from the comparison functor, and one from the coherence equation (5), just that in BCSS, the first of these is a $+$, and the second is a $-$ .

Continue reading “Correction to the definition of the String crossed module, part 2: triangulation”

# Correction to the definition of the String crossed module

I have been very slowly working, with my colleague Raymond Vozzo, on a project that involves a very explicit calculation for bundle gerbes, and in particular with the gerbe underlying the crossed module of Lie groups introduced by Baez, Crans, Schreiber and Stevenson (BCSS), which presents the String 2-group $\mathrm{String}_G$ of a suitable compact simply-connected Lie group G. However, there was a particular step where we got thoroughly stuck, where a certain calculation involving the comparison of two explicitly described connections on (a pullback of) the universal central extension $U(1) \to \widehat{\Omega G} \to \Omega G$ of Fréchet Lie groups.

Aside from needing to overcome a sign convention around the Stokes theorem for integration along a fibre of a family of manifolds with boundary, there was still an issue where I got a formula that implied a certain non-zero 2-form was equal to its own negative. The origin of this negative sign is, ultimately, the minus sign in the definition of a certain family of 1-forms $\beta_p$ on $\Omega G$ appearing in the proof of Proposition 3.1 in BCSS. In my own notation it is

$\beta_p = -2\int_0^{2\pi} \langle \Theta,p(\theta)^{-1}\partial_\theta p(\theta)\rangle\,d\theta$

where $p\colon [0,2\pi]\to G$ is a smooth path starting at the identity element, $\Theta$ is the left-invariant Maurer–Cartan form on $\Omega G$ and $\langle \cdot , \cdot\rangle$ is a suitably normalised version of the (pointwise-evaluated) Killing form on $\mathfrak{g}$. So I really couldn’t figure out what was going wrong, since I was fairly confident in our computations. This computation fed into a much larger computation, where if I ignored this problem and pressed on, trusting my instincts, things seemed to be going smoothly, and reproducing something like what we’d expect. I also had another (slow-burn) project involving this same comparison of connections, where the sign issue was also arising. The theory there pointed in one direction, the computation in another.

Continue reading “Correction to the definition of the String crossed module”

# The strange adventure of the Universal Coefficient Theorem in the night

If you trawl the internet for more exotic Universal Coefficient Theorems, then you’ll come across comments to the effect that there isn’t a UCT for cohomology with local coefficients in general (for instance, here, for group cohomology, which is ordinary cohomology of a $K(G,1)$, or the Groupprops wiki page, which only gives the trivial coefficients version). I had reason to want a UCT for group cohomology with coefficients a nontrivial module, to try to clear some hypotheses using formal properties of group homology (it’s better behaviour with respect to filtered colimits, in particular). The only reference I could find for a suitable UCT was an exercise in Spanier’s venerable book:

I found a reference in a 2018 paper, that said “there is a version [of the local coefficient UCT] in [Spanier], p. 283, though its application is limited”. Up until this point, I had not actually seen the statement written out anywhere! In particular, it’s not clear what Spanier’s assumptions are (it might be he is assuming $R$ is a PID throughout this section, but I couldn’t see it on a quick search), and in particular, something must break for this to be of “limited” application.

Continue reading “The strange adventure of the Universal Coefficient Theorem in the night”

# Update on formal anafunctors

After some very helpful comments, I have managed to finish updating my paper on formal anafunctors (original release announcement post) and have now sent it back to the journal. The length increased by about 60%, as I had missed including the proof that the associator isomorphisms were natural (7 pages! Including the diagram in this post) and that middle-four interchange holds. The referee also pointed out that the covering maps don’t really form a subcanonical pretopology, but something a bit weaker, and this weaker notion is all I use. It wasn’t so much a matter of tweaking the definition, but recognising the weakness of the definition.

So here it is: The elementary construction of formal anafunctors, arXiv:1808.04552.

For amusement, two of the new diagrams…

Now I need to write the cospans paper

# Just some Xy-pic

I know it’s not TikZ ¯\_(ツ)_/¯ but this is how I roll