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: deprecated: id my structure

Topic: initial model of the theory of distributive categories

Tobias Heindel (Feb 27 2023 at 15:57):

Is it (well-)known what the initial model of the essentially algebraic theory of categories with

finite products
finite coproducts and
distributivity
is ? Is it a common example? Are there even references?

Ryan Wisnesky (Feb 27 2023 at 16:21):

Tobias Heindel (Feb 27 2023 at 16:41):

Ryan Wisnesky said:

possibly related: http://www.tac.mta.ca/tac/volumes/8/n5/n5.pdf

so, I guess, a related question might be: what if we do require distributivity “on top”
(the reference might be interesting)
alas, we have

(Note that we are not assuming any sort of distributivity.) [op. cit., p. 71]

Tobias Fritz (Feb 27 2023 at 17:07):

Not exactly an answer, but pretty similar: A universal characterization of standard Borel spaces shows that the category of standard Borel measurable spaces and measurable maps is the initial countably complete Boolean countably extensive category. A very intriguing result!

Nathanael Arkor (Feb 27 2023 at 17:14):

The free [[distributive category]] on a category $\mathbf C$ is given by the free [[cocartesian category]] on the free [[cartesian category]] on $\mathbf C$ . Is this the kind of answer you're looking for? (Obviously the initial model can be given quite trivially syntactically, but presumably you're looking for a more categorical description.)

John Baez (Feb 27 2023 at 23:35):

This is nice. The free cartesian category on 1 object is $\mathsf{FinSet}^{\rm {op}}$ , and the free cocartesian category on that should also admit some nice description. I think one description goes like this: take the category of presheaves on $\mathsf{FinSet}^{\rm {op}}$ , and take the full subcategory consisting of finite coproducts of representables. So, this subcategory should be the free distributive category on 1 object.

John Baez (Feb 27 2023 at 23:39):

$\mathsf{FinSet}^{\mathrm{op}}$ is also the category of finite boolean algebras, say $\mathsf{FinBool}$ . So, to get the free distributive category on 1 object, we can also take the category of presheaves on $\mathsf{FinBool}$ , and take the full subcategory consisting of finite coproducts of representables.

John Baez (Feb 27 2023 at 23:39):

But it would be nice to have a more charismatic description.

Tobias Heindel (Feb 28 2023 at 10:57):

Thanks a lot for all the interesting pointers!

In fact, it now seems called for to clarify the question I wanted to ask: Given an essentially algebraic theory T such that to give a model for T is to give a distributive category, is there a well-known (simple) characterization of its initial model, i.e., the initial object in $\mathrm{Mod}(\mathit{T})=\mathrm{Lex}(\mathit{T}, \mathsf{Set})$ (cf. essentially algebraic theory).
Note, by distributive category, I mean a category with finite products and finite co-products that is distributive, i.e., the canonical map A × B + A × C → A × (B + C) is invertible.

As it happens, we are currently working on the project geb, which piggybacks on the conjecture that the category we are describing above is equivalent to $\mathsf{FinSet}$ via the evident functor. The result seems very intuitive, but we have found no references either confirming or denying it. Artem has formalized almost everything in Agda (up to atrocious details https://github.com/anoma/geb/tree/main/geb-agda). Hence, we were wondering if someone has had an observation akin to the describe one, which we could cite?

TL;DR; we want the answer to be $\mathsf{FinSet}$ -- and someone must have had this observation, no?

Reid Barton (Feb 28 2023 at 11:00):

Just to check, the morphisms between distributive categories are then meant to be functors that preserve finite coproducts and finite products?

Tobias Heindel (Feb 28 2023 at 11:13):

Reid Barton said:

Just to check, the morphisms between distributive categories are then meant to be functors that preserve finite coproducts and finite products?

yes, as all the structure that the theory T talks about must be prserved on the nose

Reid Barton (Feb 28 2023 at 11:14):

Oh I missed that you were talking about 1-categorical models.

Reid Barton (Feb 28 2023 at 11:28):

Is that the essential part of your question? It seems pretty easy to prove that any distributive category admits an essentially unique functor from FinSet that preserves finite coproducts and products (in the usual up-to-isomorphism sense). Sketch: Finite-coproduct-preserving functors from FinSet to a category C with finite coproducts are essentially determined by where they send the one point set; in order to also preserve the empty product, they have to set it to the terminal object of C; then we need to check that this thing preservses all binary products, and we can use the distributivity of C to do it.

Reid Barton (Feb 28 2023 at 11:30):

Then there should be some way to deduce that the initial strict model of your T is equivalent to FinSet but I'm not very good at that stuff.

Nathanael Arkor (Feb 28 2023 at 12:40):

@Tobias Heindel: that the initial model is FinSet follows from my earlier message. In particular, if you have no base sorts or constants, then you consider the free cartesian category on the empty category, which is just the one-object category $1$ , and then the free cocartesian category on $1$ , which is FinSet.

Nathanael Arkor (Feb 28 2023 at 12:41):

In general, the initial model of "the theory of X's" is "the free X" (essentially by definition).

Nathanael Arkor (Feb 28 2023 at 12:48):

(Note that it is initial amongst distributive categories with chosen products and coproducts, so strictly speaking you may need to take an equivalent subcategory ~~skeleton~~ of FinSet, otherwise it only satisfies the universal property up to equivalence rather than isomorphism.)

Reid Barton (Feb 28 2023 at 12:52):

I don't think you want a skeleton, but rather a fluffed-up version of the skeleton with one object for each expression you can write using $0$ , $1$ , $+$ , $\times$ .

Reid Barton (Feb 28 2023 at 12:57):

I think this syntax is just simple enough that you could prove by hand (i.e., without appealing to general strictification results) that the strictly initial distributive category also has the "up to equivalence" universal property.

Reid Barton (Feb 28 2023 at 13:04):

In particular, it's convenient that the rules for constructing objects don't depend on morphisms at all, and so in particular they don't involve quotienting by any relations.

John Baez (Feb 28 2023 at 22:04):

Tobias Heindel said:

TL;DR; we want the answer to be $\mathsf{FinSet}$ -- and someone must have had this observation, no?

This is not an answer to your question, but it might still be mildly interesting:

There's a concept more general than 'distributive category' called a [[rig category]]: it has symmetric monoidal structures $\otimes$ and $\otimes$ , with $\otimes$ distributing over $\oplus$ up to coherent isomorphism, but we don't require that $\otimes$ be product or $\oplus$ be coproduct.

A while ago I conjectured that the initial rig category is the groupoid of finite sets and bijections, with the usual $\times$ of sets as $\otimes$ and the usual $+$ of sets as $\otimes$ . (These are not product and coproduct in the groupoid of finite sets.)

John Baez (Feb 28 2023 at 22:04):

This has subsequently been proved, it seems, though the original proof had mistakes.

John Baez (Feb 28 2023 at 22:05):

Since every distributive category is a rig category there should be a map from the initial rig category to the initial distributive category.

John Baez (Feb 28 2023 at 22:06):

And if the initial distributive category is the category of finite sets and functions, then this map should be the obvious one!

Tobias Heindel (Mar 01 2023 at 07:38):

John Baez said:

And if the initial distributive category is the category of finite sets and functions, then this map should be the obvious one!

This indeed is very interesting. ~~Is the proof available and, if so, could you share a link?~~ https://ncatlab.org/nlab/show/rig%20category#baezs_conjecture

Tobias Heindel (Mar 01 2023 at 07:43):

Thanks a lot everybody!

John Baez (Mar 01 2023 at 16:03):

Yes, there are links to a number of proofs at [[rig category]]. For someone with a strong interest in this subject, Elgueta's earlier failed proof may also be interesting: it may at least serve to make people read the newer proofs with caution, looking for mistakes (which I have not yet done).