Category Theory
Zulip Server
Archive

You're reading the public-facing archive of the Category Theory Zulip server.
To join the server you need an invite. Anybody can get an invite by contacting Matteo Capucci at name dot surname at gmail dot com.
For all things related to this archive refer to the same person.

Stream: learning: questions

Topic: On the models of the product of two algebraic theories

Arturo De Faveri (Oct 13 2024 at 14:22):

Good morning to everyone,

this is something I've been thinking a lot recently, but I wasn't able to sort it out. My apologies if it's trivial or well-understood.

Let $\mathbf{A}, \mathbf{B}$ be (one-sorted, finitary) algebraic theories. Let $M$ be a model of $\mathbf{A} \times \mathbf{B}$. Of course, by a model I mean a finite-products preserving functor $\mathbf{A} \times \mathbf{B} \to \mathbf{Set}$. I want to prove that $M$ somehow decomposes into a model of $\mathbf{A}$ and a model of $\mathbf{B}$. Natural candidates of these models are the left kan extensions along the projections.

First observe that one can prove (although the proof I found is not completely trivial) that the left kan extension of $F \in \mathrm{Mod}(\mathbf{T})$ along any functor $K: \mathbf{T} \to \mathbf{S}$ preserves finite products, hence at least the left kan extension produces indeed a model of $\mathbf{S}$.

Now, let $p_\mathbf{A}: \mathbf{A} \times \mathbf{B} \to \mathbf{A}$ and $p_\mathbf{B}: \mathbf{A} \times \mathbf{B} \to \mathbf{B}$ be the two projections. I claim that $M \simeq \mathrm{Lan}_{p_\mathbf{A}} M \circ p_\mathbf{A} \times \mathrm{Lan}_{p_\mathbf{B}} M \circ p_\mathbf{B}$. Note that the unit $\eta_\mathbf{A}: M \Rightarrow \mathrm{Lan}_{p_\mathbf{A}} M \circ p_\mathbf{A}$ is "well-typed" to be the projection, and the same for $\mathbf{B}$. Using the formalism of coend calculus one has:

$$M(1) \simeq \int^n \mathbf{A}(n,1) \times \mathbf{B}(n,1) \times M(n)$$

where I used the way products are computed in the category of theories, and

$$\mathrm{Lan}_{p_\mathbf{A}} M ( p_\mathbf{A}(1)) \simeq \int^n \mathbf{A}(n,1) \times M(n)$$

and the same for $\mathbf{B}$.

But now I'm stuck and I don't know how to conclude, nor if this the best way to go about it.

Two days ago I found out that Lawvere wrote this in 1968 (Some algebraic problems in the context of functorial semantics of algebraic theories): "a bit of computation is needed to deduce from general principles that $\mathrm{Mod}(\mathbf{A} \times \mathbf{B})$ consists of algebras which canonically split as sets into a product $X \times Y$, where $X$ carries the structure of $\mathbf{A}$-algebra and $Y$ carries the structure of $\mathbf{B}$-algebra".
Which at least gives me hope that what I'm trying to do is not senseless.

Therefore my questions are:

1. can my line of reasoning be fixed to get the desired conclusion?
2. do yo have any idea about the "bit of computation" that Lawvere had in mind?

Thanks a lot.

John Baez (Oct 13 2024 at 14:41):

I have a very elementary question: by $\mathbf{A} \times \mathbf{B}$ do you mean the product in the category of 1-sorted algebraic theories, not the product in $\mathsf{Cat}$?

If we think of $\mathbf{A}$ as a category with finite products it has one object for each natural number, say $1, x, x^2, x^3, \dots$ and similarly $\mathbf{B}$ has objects $1, y, y^2, y^3, \dots$ so the product in $\mathsf{Cat}$ is naturally a 2-sorted algebraic theory with objects $x^m \times y^n$. But we can extract from that a 1-sorted algebraic theory with only the 'diagonal' objects $x^m \times y^m$. Is that what you mean by $\mathbf{A} \times \mathbf{B}$?

Arturo De Faveri (Oct 13 2024 at 14:46):

Exactly!

John Baez (Oct 13 2024 at 14:49):

Okay, so you're saying $\mathbf{A} \times \mathbf{B}$ is indeed the product in the category (or 2-category) of 1-sorted algebraic theories, and the projections $p_\mathbf{A} : \mathbf{A} \times \mathbf{B} \to \mathbf{A}$, $p_\mathbf{A} : \mathbf{A} \times \mathbf{B} \to \mathbf{B}$ have to be understood as morphisms in that category, not $\mathsf{Cat}$. Personally I would start by making sure I really understood these projections quite well. Maybe you already do.

Arturo De Faveri (Oct 13 2024 at 15:20):

Yes, $\mathbf{A} \times \mathbf{B}$ is the product in the category of theories. A theory $\mathbf{A}$ has a denumerable set of objects $\{1, x, x^2, \ldots\}$ – which for brevity I will denote by $\{0, 1, 2, \ldots\}$ since it's not at all important the 'name' of the generating object $x$ – and some unspecified morphisms $n \to 1$ (of course there are the $n$ projections but possibly more) which we may call the $n$-ary terms of the theory.

If $\mathbf{B}$ is another theory then the morphisms $n \to 1$ in $\mathbf{A} \times \mathbf{B}$ are pairs of $n$-ary terms $(s,t)$ of $\mathbf{A}$ and $\mathbf{B}$ respectively. The projection $p_\mathbf{A}: \mathbf{A} \times \mathbf{B} \to \mathbf{A}$ acts on the objects stupidly (as every morphism of theories does, sending $k$ to $k$ for every $k$) and maps the morphism $(s,t)$ to $s$.

By the way, do not confuse the product with the "tensor product" of two theories. A model of the tensor $\mathbf{A} \otimes \mathbf{B}$ is indeed a set in which somehow the $\mathbf{A}$-structure and the $\mathbf{B}$-structure coexist.

John Baez (Oct 13 2024 at 15:30):

Right, I've thought more about the tensor product.

Thanks for the clarification about $\mathbf{A} \times \mathbf{B}$.

Chaitanya Leena Subramaniam (Oct 16 2024 at 01:39):

Arturo De Faveri said:

2. do yo have any idea about the "bit of computation" that Lawvere had in mind?
   

I'm not sure what computation Lawvere had in mind, but here's one way of looking at it:

A single-sorted algebraic theory is given by an identity-on-objects and finite-product-preserving ("fpp") functor $\mathrm{Fin}^{op}\to A$, where $\mathrm{Fin}$ is (a skeleton of) the category of finite sets. A morphism of single-sorted algebraic theories is a commutative triangle.
Then the product (in the category of single-sorted algebraic theories) of two single-sorted algebraic theories $(\mathrm{Fin}^{op}\to A)$ and $(\mathrm{Fin}^{op}\to B)$ is the algebraic theory $\mathrm{Fin}^{op}\to A\boxtimes B$ obtained by the (identity-on-obects, fully faithful) factorisation of the fpp functor $\mathrm{Fin}^{op}\to (A\times B)$ (where $A\times B$ is the ordinary product of categories).

Since (as you noted) the left Kan extension of a fpp functor to $\mathrm{Set}$ is also fpp, we get a coreflective subcategory
$[A\boxtimes B,\mathrm{Set}]_{\mathrm{fpp}} \hookrightarrow [A\times B,\mathrm{Set}]_{\mathrm{fpp}}$.

The unit of this adjunction is the natural isomorphism you're looking for :)

Remark: The 2-category of finite-product categories and fpp functors has finite biproducts (in a 2-categorical sense)—so we have a canonical equivalence
$[A\times B,\mathrm{Set}]_{\mathrm{fpp}} \simeq [A,\mathrm{Set}]_{\mathrm{fpp}}\times[B,\mathrm{Set}]_{\mathrm{fpp}}$.

Side note regarding your calculation: Let $M_A$ and $M_B$ be the left Kan extensions of $M$ along the projections $A\boxtimes B\to A$ and $A\boxtimes B\to B$ respectively, and let $M_{A\times B}$ be the left Kan extension along the inclusion $A\boxtimes B\hookrightarrow A\times B$. Then we have $M_A(1) = M_{A\times B}(1,0)$ and $M_B(1)=M_{A\times B}(0,1)$.
Therefore $M_A(1)\times M_B(1) = M_{A\times B}(1,0)\times M_{A\times B}(0,1)=M_{A\times B}(1,1) = M(1)$.

Vincent Moreau (Oct 16 2024 at 09:27):

Hi Chaitanya, nice explanation! This seems to suggest that even if one is only interested in single-sorted algebraic theories, the "unsorted" framework of all small cartesian categories -- which is where the Lan ⊣ precomposition adjunction is best formulated, is a nice place to work in before going back to the single-sorted case using the bo-ff factorization system. Is there a document where the properties of the 2-category of small cartesian categories are spelled out, like the fact that it has biproducts?

Vincent Moreau (Oct 16 2024 at 09:30):

By the way, is there a generalization of the tensor product of single-sorted algebraic theories to a tensor product of small cartesian categories, from which we could deduce the single-sorted tensor product by bo-ff factorization?

Chaitanya Leena Subramaniam (Oct 16 2024 at 16:01):

Vincent Moreau said:

Is there a document where the properties of the 2-category of small cartesian categories are spelled out, like the fact that it has biproducts?

I can't think of a document off the top of my head. But I would suspect that a statement like "Given a symmetric monoidal $n$-category $\mathcal{C}$ (where $n\leq\infty$), coproducts in the category $\mathrm{CMon}(\mathcal{C})$ of (fully) commutative monoids in $\mathcal{C}$ are given by the underlying tensor product in $\mathcal{C}$" should be true (and should be provable from/has been proved somewhere in Lurie's Higher Algebra?)

So when $\mathcal{C}$ is a cartesian monoidal $n$-category, coproducts of monoids are biproducts.

Mike Shulman (Oct 16 2024 at 16:03):

I feel like the case of cartesian 1-categories must exist in the non-$\infty$ literature somewhere...

Vincent Moreau (Oct 16 2024 at 16:09):

At least in the case of n = 1, this is explained in section 6.5 of Categorical Semantics of Linear Logic, in the dual case of symmetric comonoids.

Chaitanya Leena Subramaniam (Oct 16 2024 at 16:13):

Vincent Moreau said:

By the way, is there a generalization of the tensor product of single-sorted algebraic theories to a tensor product of small cartesian categories, from which we could deduce the single-sorted tensor product by bo-ff factorization?

The tensor product of small finite-product categories is the one that makes the functor $[-,\mathrm{Set}]_{\mathrm{fpp}}$ from small finite-product categories to locally (finitely) presentable categories a monoidal functor. It takes an $S$-sorted theory and an $S'$-sorted theory to an $S\times S'$-sorted theory. (By the way, a similar fact is more generally true when $S$ is a category of sorts---shameless plug of my thesis :upside_down:)

The biproduct of small finite-product categories takes an $S$-sorted theory and an $S'$-sorted theory to an $S+ S'$-sorted theory.

Vincent Moreau (Oct 16 2024 at 16:13):

What you are saying is that these biproducts have nothing to do whatsoever with the cartesian aspects of the categories at stake, but it all comes from the fact that cartesian categories form a full subcategory of monoidal categories in a cartesian 2-category, right?

Chaitanya Leena Subramaniam (Oct 16 2024 at 16:15):

If by "monoidal categories" (in a cartesian 2-category) you mean "commutative monoid", then yes.

Vincent Moreau (Oct 16 2024 at 16:17):

I see, yes I meant "a full subcategory of symmetric monoidal categories, which are commutative pseudomonoids in a cartesian 2-category".

Vincent Moreau (Oct 16 2024 at 16:24):

Chaitanya Leena Subramaniam said:

The tensor product of small finite-product categories is the one that makes the functor $[-,\mathrm{Set}]_{\mathrm{fpp}}$ from small finite-product categories to locally (finitely) presentable categories a monoidal functor. It takes an $S$-sorted theory and an $S'$-sorted theory to an $S\times S'$-sorted theory. (By the way, a similar fact is more generally true when $S$ is a category of sorts---shameless plug of my thesis :upside_down:)

Very simple question, but which monoidal structure do you consider on lfp categories for that matter?

Chaitanya Leena Subramaniam (Oct 16 2024 at 16:29):

The one that classifies bi-cocontinuous functors (i.e. the one inherited from cocomplete categories).

John Baez (Oct 16 2024 at 16:36):

Chaitanya Leena Subramaniam said:

Vincent Moreau said:

Is there a document where the properties of the 2-category of small cartesian categories are spelled out, like the fact that it has biproducts?

I can't think of a document off the top of my head. But I would suspect that a statement like "Given a symmetric monoidal $n$-category $\mathcal{C}$ (where $n\leq\infty$), coproducts in the category $\mathrm{CMon}(\mathcal{C})$ of (fully) commutative monoids in $\mathcal{C}$ are given by the underlying tensor product in $\mathcal{C}$" should be true (and should be provable from/has been proved somewhere in Lurie's Higher Algebra?)

So when $\mathcal{C}$ is a cartesian monoidal $n$-category, coproducts of monoids are biproducts.

By the way, for anyone seeking references for folklore facts, the case $n = 2$, using plain old bicategory theory, can be found as Theorem 5.2 here:

• D. Schäppi, Ind-abelian categories and quasi-coherent sheaves. Math. Proc. Camb. Philos. Soc., 157(3):391–423, 2014. Available as arXiv:1211.3678.

He shows that given symmetric pseudomonoids M and M′ in a symmetric monoidal bicategory (C, ⊗, I), there is a natural way to make M ⊗ M′ into a symmetric pseudomonoid, which makes it into the bicategorical coproduct in the bicategory of symmetric pseudomonoids in (C, ⊗, I).

He doesn't just hand-wave the argument: he puts the proof in Appendix A, and he uses some string diagrams. But I'll admit I haven't carefully checked the proof because the result is so 'obvious'!

Mike Shulman (Oct 16 2024 at 16:41):

Thanks! Is that recorded on the nLab somewhere?

Mike Shulman (Oct 16 2024 at 16:43):

I guess for the cartesian case, one then needs to check that if $M$ and $M'$ are cartesian monoidal categories (or, more generally I guess, cartesian objects in a 2-category with finite products), then the "natural" symmetric pseudomonoid structure on $M\times M'$ is also cartesian.

John Baez (Oct 16 2024 at 16:52):

Mike Shulman said:

Thanks! Is that recorded on the nLab somewhere?

I don't know. I have a feeling that I dug up this paper when Joe Moeller, Todd Trimble and I needed this result. Where should this result go?

Chaitanya Leena Subramaniam (Oct 16 2024 at 17:03):

Mike Shulman said:

I guess for the cartesian case, one then needs to check that if $M$ and $M'$ are cartesian monoidal categories (or, more generally I guess, cartesian objects in a 2-category with finite products), then the "natural" symmetric pseudomonoid structure on $M\times M'$ is also cartesian.

This should follow from cartesian monoidal categories being a reflective subcategory of symmetric monoidal categories (at least in the case of the 2-category Cat).

Mike Shulman (Oct 16 2024 at 17:09):

Isn't that rather like crushing a gnat with a sledgehammer?

Chaitanya Leena Subramaniam (Oct 16 2024 at 17:13):

I wonder if the case of cartesian objects in a 2-category can be explained by "freely adjoining adjoints"