January Update 2
These past two weeks I developed some theory about unital magmoids, and (separately) returned to the adjunctions of a duploid’s shift functors.
Duploids
Subcategories of a Unital Magmoid
Let me briefly define the subcategories of a unital magmoid \(\M\) (this is a nicer typeset copy of the comments in Subcategories.v):
- \(\Cl\M\) has all objects and linear morphisms.
- \(\Ct\M\) has all objects and thunkable morphisms.
- \(\Clt\M\) has all objects and linear-and-thunkable morphisms.
- \(\Cn\M\) has negative objects and thunkable morphisms.
- \(\Cp\M\) has positive objects and linear morphisms.
- \(\Cnl\M\) has negative objects and linear-and-thunkable morphisms.
- \(\Cpt\M\) has positive objects and linear-and-thunkable morphisms.
The inclusion functors are depicted in the below commutative diagram, where all but the four vertical arrows depict fully faithful functors.
Shift Functors
When \(\D\) is a duploid, we get from its shifts two non-functorial maps on objects and morphisms \(\downshift : \D \to \Cp\D\) and \(\upshift : \D \to \Cn\D\). When restricted to \(\Ct\D\) and \(\Cl\D\) respectively, they define functors \(\downshift : \Ct\D \to \Cpt\D\) and \(\upshift : \Cl\D \to \Cnl\D\) which moreover take part in an adjoint equivalence with the inclusion functor. Important adjunctions are listed below.
Note that, though they are not literally the same functors, I will write all shift-based functors (or non-functors) with \(\upshift\) or \(\downshift\) respectively, with inclusions to be inferred. When I write \(F \dashv G : \C \to \D\), I mean that \(F : \D \to \C\) is left-adjoint to \(G : \C \to \D\).
We have the following isomorphisms of homsets:
\[\begin{align*} \morsof{\Cl\D}{\downshift a}{b} &\simeq \morsof{\D}{\downshift a}{b} \\ &\simeq \morsof{\D}{a}{b} \\ &\simeq \morsof{\D}{a}{\upshift b} \simeq \morsof{\Ct\D}{a}{\upshift b} \end{align*}\]
This isomorphism is natural in \(a : \Ct\D\) and \(b : \Cl\D\). However, even though only the two endpoints of this isomorphism are actually functorial, each isomorphism is actually “natural” even for \(a : \D\) and \(b : \D\), in the sense that the naturality square still commutes. Thus \(\downshift \dashv \upshift : \Cl\D \to \Ct\D\) forms an adjunction of functors, which can be extended to \(\downshift \dashv \upshift : \Cp\D \to \Cn\D\) and \(\downshift \dashv \upshift : \Cpt\D \to \Cnl\D\).
There are a few more adjunctions, in fact:
-
\(I \dashv \downshift : \Ct\D \to \Cpt\D\) is an adjoint equivalence with unit \(\wrap : \Id_{\Cpt\D} \to \downshift I\) and counit \(\unwrap : I \downshift \to \Id_{\Ct\D}\). Dually, \(I \dashv \upshift : \Cl\D \to \Cnl\D\) is an adjoint equivalence with unit \(\delay : \Id_{\Cnl\D} \to \upshift I\) and counit \(\force : I \upshift \to \Id_{\Cl\D}\).
-
There is an adjunction the other way too: \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\). In Guillaume’s thesis, an important result is that all duploids are equivalent to the duploid arising from this adjunction.
In the formalisation, the inclusions cause a lot of grief when trying to define all the adjunctions without just repeating myself; I attempted to write the proofs last week using explicit units and counits in the hope that I would be able to reuse more of the proofs. Although proving all of \(\delay\) and \(\wrap\) etc. to be natural was fine, the composition of natural transformations and their adjunctions was too inconvenient, and doesn’t play nicely with the lack of associativiy in unital magmoids.
I think instead I will return to the homset-isomorphism-based definitions since they compose nicer even for the non-functorial portions of the isomorphism above. Units and counits generated by the homset adjunction did have some extra identity morphisms floating about, which I felt was a little ugly, but I think it is a small price to pay. I will still have to figure out how to prove the final adjunction above nicer.
Yoneda for Unital Magmoids
I thought it would be an interesting study of how the Yoneda lemma generalises to unital magmoids. After all, most theorems about categories should give rise to a similar theorem about unital magmoids with extra side-conditions on associativity. And if I do find a direct Rezk completion of unital magmoids, then when the magmoid is a category we will have a Rezk completion of categories, so looking at the existing Rezk completion of the latter via Yoneda might give insight for unital magmoids. Of course, the category of presheaves remains a category even if we generalise to unital magmoids so long as composition happens in \(\Set\), meaning we won’t get an equivalent unital magmoid back right away, but it was a fun exercise to see what happens.
In order to see what associativity conditions we might need, here is a statement and pedantic proof of Yoneda’s lemma in categories:
- Given a category \(\C\) and an object \(a : \C\), let \(h_a\)
denote the functor \(\C^\op \to \Set\) which maps objects \(b :
\C\) to \(\morsof{\C}{b}{a}\) and morphisms \(f : b’ \to b\) to the
precomposition function \(h_a(f)(g : \morsof{\C}{b}{a})
= f \cdot g : \morsof{\C}{b’}{a}\).
- This preserves identities: \(h_a(\id_b)(g) = \id_b \cdot g = g\) by left-identity.
- This preserves composition: \(h_a(f \cdot f’)(g) = (f \cdot f’) \cdot g = f \cdot (f’ \cdot g) = (h_a(f’) \cdot h_a(f))(g)\) by associativity.
- Given a morphism \(k : \morsof{\C}{a}{b}\), let \(h_k\) denote the
natural transformation \(h_a \Rightarrow h_b\) given pointwise by
postcomposition with \(k\): \(h_k (c : \C) (g : h_a(c)) = g \cdot
k : h_b(c)\).
-
This is natural: fix a morphism \(f : \morsof{\C}{c}{d}\). We need that \(h_k(c) \cdot h_b(f) = h_a(f) \cdot h_k(d)\). By function extensionality fix \(g : h_a(c)\), so that we need only \(h_b(f)(h_k(c)(g)) = h_k(d)(h_a(f)(g))\).
Unfolding definitions gives \(f \cdot (g \cdot k) = (f \cdot g) \cdot k\), which is precisely associativity.
-
- Let \(h_{-}\) denote the functor \(\C \to [\C^{\op}, \Set]\) given on
objects by \(h_a\) and morphisms by \(h_f\) as defined above.
- This preserves identities: \(h_{\id_a}\) gives post-composition by \(\id_a\), which is the identity by right-identity of \(\C\).
-
This preserves composition: given \(f : a \to b\) and \(g : b \to c\), \(h_{f \cdot g}\) is the post-composition with \(f \cdot g\), and we need to prove \(h_{f \cdot g} = h_f \cdot h_g\).
By function extensionality, fix \(h : h_a(d)\). We now need only prove \(h \cdot (f \cdot g) = (h \cdot f) \cdot g\), which is once again precisely associativity.
-
Fix a functor \(F : [\C^{\op}, \Set]\) and object \(a : \C\).
Define the map \(\varphi : \morsof{[\C^{\op}, \Set]}{h_a}{F} \to Fa\) as \(\varphi(\alpha) = \alpha(a)(\id_a)\).
Define the map \(\psi : Fa \to \morsof{[\C^{\op}, \Set]}{h_a}{F}\) as \(\psi(x : Fa)(b : \C)(f : b \to a) = F(f)(x) : Fb\).
- This is natural in \(b : \C\): fix a morphism \(f : c \to b\), for which we will need to prove \(h_a(f) \cdot \psi(x)(c) = \psi(x)(b) \cdot F(f)\). By function extensionality, fix \(g : b \to a\). Unfolding all the definitions requires us to prove \(F(f \cdot g)(x) = F(f)(F(g)(x))\), which is precisely composition-functoriality of \(F\).
- \(\varphi\) and \(\psi\) form an isomorphism \(\morsof{[\C^{\op}, \Set]}{h_a}{F} \simeq Fa\).
-
For any element \(x : Fa\), \(\varphi(\psi(x)) = \psi(x)(a)(\id_a) = F(\id_a)(x) = x\) by identity-functoriality of \(F\).
-
For any natural transformation \(\alpha : h_a \Rightarrow F\), \(\psi(\varphi(\alpha)) = \alpha\). By function extensionality (twice), we have \(\psi(\varphi(\alpha))(b : \C)(f : b \to a) = \psi(\alpha(a)(\id_a))(b)(f) = F(f)(\alpha(a)(\id_a)) = \alpha(b)(f)\) by naturality of \(\alpha\).
-
-
(This isomorphism is also natural in \(a\) and \(F\) but gosh I have not gone there yet)
- Corollary of the isomorphism: \(h_{-}\) is fully faithful.
Generalizing to unital magmoids, the associativity conditions fail in general, thus:
- \(h_a\) for \(a : \M\) is not quite a functor; it preserves identities but not composition in general. If we replace \(C^\op\) in the above with \(\Ct\M\), so that we precompose with a thunkable morphism, then functoriality is recovered.
- \(h_k\) for \(k : \morsof{\M}{a}{b}\) is not natural in general, but is when \(k\) is linear.
- \(h_{-}\) is not quite a functor; it also preserves identities but not composition in general. Restricting to \(\Cl\M\) recovers functoriality.
- \(\varphi\) and \(\psi\) can both be defined just fine, although \(h_a\) fails to be in \([\M^{\op}, \Set]\) for its lack of functoriality. Instead, we can consider the category of not-quite-functors (those which do not preserve composition) and unnatural transformations denoted, say, \([\M^{\op}, \Set]_0\), since \(\psi\) fails to yield a natural transformation in general.
- Isomorphism of \(\varphi : \morsof{[\M^{\op}, \Set]_0}{h_a}{F} \to Fa\) and
\(\psi : Fa \to \morsof{[\M^{\op}, \Set]_0}{h_a}{F}\) does almost work out:
-
\(\psi\) is still a section of \(\varphi\) (\(\psi \cdot \varphi = \id_{Fa}\)), since not-quite-functors still preserve identities.
-
\(\psi\) is still a retraction of \(\phi\) (\(\varphi \cdot \psi = \id_{\morsof{[\M^{\op}, \Set]_0}{h_a}{F}}\)) when restricted to “natural” transformations (with the naturality square commuting even if \(h_a\) is not a functor), but not in general. However, the proof only requires naturality when the unnatural transformation \(\alpha : h_a \to F\) is applied to the identity (precisely the \(F(f)(\alpha(a)(\id_a)) = \alpha(b)(f)\) term in 5.2), which is satisfied both by \(h_k\) and \(\psi\) itself.
-
- 5.1 means that \(h_{-}\) is still faithful (even if not quite a functor). 5.2 gives a subset of unnatural transformations that make it full.
Agenda
These are the things I would particularly like to discuss:
- The proofs of the adjunctions that Guillaume uses are all based on the adjoint equivalence, and set-theoretic arguments about certain homsets being equal. I wonder how we can more nicely use the adjoint equivalence and the properties of the inclusion functors to reason similarly.
- I am wondering what names to give the functors which only preserve
identities and not composition. In the formalisation I have
currently called them
notfunctorand “not-quite-functor” in prose, which is funny but not a great name for something. I also do not know what to make of such functors (\(\upshift\) and \(\downshift\) are also not-quite-functors, in fact). - A related naming problem is that of a duploid arising from an adjunction. I have named it the “oblique” duploid after the term “oblique morphisms” used by [1].
- I’m not at all sure what to make of this weird Yoneda thing. It was fun but will it be useful? I don’t know. Maybe it will help when thinking about duploids, where objects and morphisms can be shifted as needed.
My plan for next week (when I am not working on other coursework) is to shift my attention back to duploids again, to see how well the main result relating duploids to the oblique one arising from their \(\upshift \dashv \downshift : \Cnl\D \to \Cpt\D\) adjunction works, or else to extend the theory of split duploids further.