Classifying topoi and generalised abstract syntax [008J]
For any small category \(\mathscr {C}\), Fiore treats \(\mathscr {C}\)-sorted abstract syntax in the functor category \({\mathopen {}\left [\mathscr {C},\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}{\mathscr {C}}\right )\mathclose {}}\right ]\mathclose {}}\) where \(\operatorname {\mathbb {L}}\) is some 2-monad on \(\mathbf {Cat}\); any such functor \(P\) denotes a set that is indexed in sorts and contexts (where the 2-monad \(\operatorname {\mathbb {L}}\) takes a category of sorts to the corresponding category of contexts). When \(\mathscr {C}\) is a set and \(\operatorname {\mathbb {L}}\) is either finite limit or finite product completion, we recover the standard notions of many-sorted abstract syntax; in general, we get a variety of forms of dependently sorted or generalised abstract syntax.
We will assume here that \(\operatorname {\mathbb {L}}\) is the free finite limit completion 2-monad; our goal is to study Fiore’s general substitution monoidal structure from the point of view of classifying topoi, building on Johnstone’s analogous observations (Elephant, D3.2) on the non-symmetric monoidal structure of the object classifier. The topos theoretic viewpoint that we will explore is nothing more than a rephrasing of Fiore’s account in terms of the Kleisli composition in a 2-monad; nonetheless the perspective of classifying topoi is enlightening, as it provides an explanation for precisely what internal geometrical structure one expects in a given topos for abstract syntax, potentially leading to improved internal languages.
For any small category \(\mathscr {C}\), the category of presheaves \(\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}\mathscr {C}\right )\mathclose {}}\) corresponds to the classifying topos of diagrams of shape \(\mathscr {C}\). Following Anel and Joyal, we shall write \(\mathbb {A}^{\mathscr {C}}\) for this “affine” classifying topos; under the conventions of op. cit., we may then identify the category of sheaves \(\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\) with the presheaf category \(\operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}{\mathscr {C}}\right )\mathclose {}}\).
The universal property of \(\mathbb {A}^{\mathscr {C}}\) as the classifying topos of \(\mathscr {C}\)-diagrams means that for any topos \(\mathcal {X}\), a diagram \({\mathscr {C}}\xrightarrow {{P}}{\operatorname {Sh}{\mathcal {X}}}\) corresponds essentially uniquely (by left Kan extension) to a morphism of topoi \({\mathcal {X}}\xrightarrow {{\bar {P}}}{\mathbb {A}^{\mathscr {C}}}\). We have a generic \(\mathscr {C}\)-shaped diagram \({\mathscr {C}}\xrightarrow {{\mathrm {G}_{\mathscr {C}}}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\) corresponding under this identification to the identity map on \(\mathbb {A}^{\mathscr {C}}\). More explicitly, the diagram \(\mathrm {G}_{\mathscr {C}}\) is the following composite:
\[
\mathrm {G}_{\mathscr {C}} :\equiv \mathscr {C}\xrightarrow {\eta _\mathscr {C}} \operatorname {\mathbb {L}}\mathscr {C}\xrightarrow {よ_{\mathscr {C}}} \operatorname {Pr}{\mathopen {}\left (\operatorname {\mathbb {L}}\mathscr {C}\right )\mathclose {}} = \operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\]Given a morphism of topoi \({\mathcal {X}}\xrightarrow {{f}}{\mathbb {A}^{\mathscr {C}}}\), we may recover the diagram \(\mathscr {C}\to {\operatorname {Sh}{\mathcal {X}}}\) that it classifies as the composite \(\mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}}\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\xrightarrow {f^{*}}\operatorname {Sh}{\mathcal {X}}\).
In case \(\mathcal {X}\equiv \mathbb {A}^{\mathscr {C}}\), then, we have a correspondence between \(\mathscr {C}\)-shaped diagrams of sheaves on \(\mathbb {A}^{\mathscr {C}}\) and endomorphisms of \(\mathbb {A}^{\mathscr {C}}\); we are interested in representing the compositions of such endomorphisms as a tensor product on the functor category \({\mathopen {}\left [\mathscr {C},\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\right ]\mathclose {}}\).
In particular, let \({\mathscr {C}}\xrightarrow {{P,Q}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\) be two diagrams; taking characteristic maps, we have endomorphisms of affine topoi \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{\bar {P},\bar {Q}}}{\mathbb {A}^{\mathscr {C}}}\), which we may compose to obtain \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{\bar {Q}\circ \bar {P}}}{\mathbb {A}^{\mathscr {C}}}\); then, we will define the tensor \(P\bullet Q\) to be the diagram whose characteristic morphism of affine topoi is \(\bar {P}\circ \bar {Q}\). In other words:
\[
\begin {aligned}
P\bullet Q
&:\equiv
\mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}}
\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\xrightarrow {{\mathopen {}\left (\bar {P}\circ \bar {Q}\right )\mathclose {}}^{*}}
\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\\
&=
\mathscr {C}\xrightarrow {\mathrm {G}_{\mathscr {C}}}
\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\xrightarrow {\bar {P}^{*}}
\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\xrightarrow {\bar {Q}^{*}}
\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}
\end {aligned}
\]To give an explicit computation of the tensor product, we first compute the inverse image of any \({\mathbb {A}^{\mathscr {C}}}\xrightarrow {{f}}{\mathbb {A}^{\mathscr {C}}}\) on representables \(よ_{\mathscr {C}}\Gamma \) for \(\Gamma \in \operatorname {\mathbb {L}}\mathscr {C}\). As any left exact functor \({\operatorname {\mathbb {L}}\mathscr {C}}\xrightarrow {{H}}{\mathscr {E}}\) is the right Kan extension of \({\mathscr {C}}\xrightarrow {{H\circ \eta _\mathscr {C}}}{\mathscr {E}}\) along \({C}\xrightarrow {{\eta _\mathscr {C}}}{\operatorname {\mathbb {L}}\mathscr {C}}\), we can conclude that \(H\Gamma \cong \operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}}H{\mathopen {}\left (\eta _\mathscr {C}{d}\right )\mathclose {}}\). We will use this in our calculation below, setting \(H:\equiv f^{*}\circ よ_{\mathscr {C}}\).
\[
\begin {aligned}
f^{*}{よ_{\mathscr {C}}\Gamma }
&\cong
\operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}}
f^{*}{
よ_{\mathscr {C}}{\eta _\mathscr {C}{d}}
}
\\
&\cong
\operatorname {lim}_{\Gamma \to \eta _\mathscr {C}{d}}
f^{*}{\mathrm {G}_{\mathscr {C}}{d}}
\end {aligned}
\]We are now prepared to compute the tensor product of any \({\mathscr {C}}\xrightarrow {{P,Q}}{\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}}\).
\[
\begin {aligned}
{\mathopen {}\left (P\bullet Q\right )\mathclose {}}c
&=
\bar {Q}^{*}
\bar {P}^{*}
\mathrm {G}_{\mathscr {C}}{c}
\\
&\cong
\bar {Q}^{*}
{\mathopen {}\left (Pc\right )\mathclose {}}
\\
&\cong
\bar {Q}^{*}
\operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc}
よ_{\mathscr {C}}\Delta
\\
&\cong
\operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc}
\bar {Q}^{*}よ_{\mathscr {C}}\Delta
\\
&\cong
\operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc}
\operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}}
\bar {Q}^{*}\mathrm {G}_{\mathscr {C}}d
\\
&\cong
\operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc}
\operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}}
Qd
\end {aligned}
\]Finally, we can relate the computation above to that of Fiore in terms of coends.
\[
\begin {aligned}
{\mathopen {}\left (P\bullet Q\right )\mathclose {}}\,c
&\cong
\operatorname {colim}_{よ_{\mathscr {C}}\Delta \to Pc}
\operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}}
Qd
\\
&\cong
\int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}}
{\mathopen {}\left [よ_{\mathscr {C}}\Delta ,Pc\right ]\mathclose {}}
\cdot
\operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd
\\
&\cong
\int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}}
P\,c\,\Delta
\cdot
\operatorname {lim}_{\Delta \to \eta _\mathscr {C}{d}} Qd
\\
&\cong
\int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}}
P\,c\,\Delta
\cdot
\int _{c\in \mathscr {C}}
{\mathopen {}\left [\Delta ,\eta _\mathscr {C}{d}\right ]\mathclose {}}\pitchfork Qd
\end {aligned}
\]Above, we have written \({\mathopen {}\left (\cdot \right )\mathclose {}}\) and \({\mathopen {}\left (\pitchfork \right )\mathclose {}}\) for the tensoring and cotensoring of \(\operatorname {Sh}{\mathbb {A}^{\mathscr {C}}}\) over \(\mathbf {Set}\) respectively. Thus, the fully pointwise computation is as follows:
\[
{\mathopen {}\left (P\bullet Q\right )\mathclose {}}\,c\,\Gamma \cong
\int ^{\Delta \in \operatorname {\mathbb {L}}\mathscr {C}}
P\,c\,\Delta
\times
\int _{c\in \mathscr {C}}
{\mathopen {}\left [\Delta ,\eta _\mathscr {C}{d}\right ]\mathclose {}}\Rightarrow Q\,d\,\Gamma
\]Thanks to Marcelo Fiore and Daniel Gratzer for helpful discussions.