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: Comonoids in partial functions

James Wood (Jun 04 2021 at 14:39):

I know that every object in Set gives rise to a unique comonoid. Are comonoids in the category of sets and partial functions (with the (1, ×) monoidal structure) similarly trivial? My intuition is that the comultiplication still has to be duplicate (from the unit laws), and because the comultiplication determines the counit, those comonoids are unique.

James Wood (Jun 04 2021 at 14:47):

Furthermore, duplicate and delete exist for any object (with delete being the total function mapping each element to * ∈ 1).

Robin Piedeleu (Jun 04 2021 at 14:49):

Wouldn't the restriction of the standard comonoid on $X$ to a subset $S\subseteq X$ give a different comonoid structure on $X$? Its comultiplication is given by the partial function (in relational form) $\{(x,(x,x)) | x \in S\}$ with counit the set $S$ itself?

Joe Moeller (Jun 04 2021 at 14:49):

The general fact here is that comonoids in a cartesian monoidal category are trivial.

Joe Moeller (Jun 04 2021 at 14:49):

Similarly, monoids in a cocartesian monoidal category are trivial.

Joe Moeller (Jun 04 2021 at 14:50):

So the question now is whether times is the cartesian product in the category of partial functions.

Robin Piedeleu (Jun 04 2021 at 14:50):

Partial functions with $\times$ as monoidal product are not Cartesian

Joe Moeller (Jun 04 2021 at 14:52):

Great, then there's a chance for non-trivial examples.

Robin Piedeleu (Jun 04 2021 at 14:52):

One way to see it is that it's equivalent to the category of pointed sets.

Robin Piedeleu (Jun 04 2021 at 14:53):

It has natural diagonals but not natural projections.

Joe Moeller (Jun 04 2021 at 14:53):

Right. I like your example. You're saying that you can take a (trivial) comonoid in Set and just restrict to any subset, and that should define a partial comonoid on X?

Joe Moeller (Jun 04 2021 at 14:54):

I wonder if there are any examples that don't fall into this description. In other words: Is there a partial comonoid which does not extend to a well-defined (and thus trivial) comonoid?

James Wood (Jun 04 2021 at 15:13):

Robin Piedeleu said:

Wouldn't the restriction of the standard comonoid on $X$ to a subset $S\subseteq X$ give a different comonoid structure on $X$? Its comultiplication is given by the partial function (in relational form) $\{(x,(x,x)) | x \in S\}$ with counit the set $S$ itself?

For relations, one of the unit laws is that $\exists y.~\mu(x,(y,x')) \wedge \eta(y)$ iff $x = x'$. Letting $x'$ be $x$ and reading from right to left, there must be a $y$ in the counit such that $\mu(x,(y,x))$. Symmetrically, there must be some $z$ in the counit such that $\mu(x,(x,z))$. But if $\mu$ is deterministic, $y$ and $z$ must both be $x$, so I think $\mu$ has to be total (and particularly the total diagonal).

The direct counterexample to the quoted construction would be to take some $x \notin S$. Then, there must be a $y$ in the counit such that $\mu(x) = (y, x)$. In particular, $\mu(x)$ cannot be undefined.

Robin Piedeleu (Jun 04 2021 at 15:18):

Good point! My counterexample is not one because it does not satisfy the counit law. It's only a co-associative binary operation.

James Wood (Jun 04 2021 at 15:21):

The unit laws feel quite strong in this setting.

James Wood (Jun 04 2021 at 15:37):

And yeah, I've convinced myself that neither is 1 terminal (0 is) nor is × the limit-defined product (there is no pairing for partial functions that disagree on definèdness on any element of their domain). Maybe there is a product for partial functions, at least assuming excluded middle, but I don't think I want to use it. So I don't get to reuse the nice theorem about Cartesian monoidal structure.

Tobias Fritz (Jun 04 2021 at 16:10):

With string diagrams drawn from bottom to top, the category of sets and partial functions is such that the canonical comultiplications are natural, in that the following equation holds for every partial function $f$:
det.png

Tobias Fritz (Jun 04 2021 at 16:11):

On the other hand, the counits are not natural: the following equation holds if and only if $f$ is a total function:
counit.png

Tobias Fritz (Jun 04 2021 at 16:15):

If the comonoid structure on every object is indeed still unique, then it may be possible to prove this using reasoning similar to the Remarks 10.18 and 11.29 in this paper. Note that this is a setting in which the naturality equation for the counit is assumed to hold for every $f$, while the one for the comultiplication need not. So the context is exactly opposite to yours and those arguments will not apply in the same form. But perhaps this can still inspire a proof in terms of string diagrams. In particular, I think that the category of sets and partial functions still satisfies the positivity axiom introduced in Definition 11.22, and this may be helpful.

EDIT: I forgot to mention that the positivity axiom holds with the word "deterministic" replaced by "total".

Chad Nester (Jun 04 2021 at 16:27):

Sets and partial functions form a cartesian restriction category, which is equivalently a symmetric monoidal category in which every object is equipped with a commutative comonoid, satisfying the usual coherence conditions, in which the comultiplication is natural. (As Tobias explains above).

Chad Nester (Jun 04 2021 at 16:29):

In fact, sets and partial functions are a discrete cartesian restriction category, which from this perspective means that there is a "multiplication" map as well, and that the multiplication and comultiplication together satisfy the special frobenius axioms. This appears in our POPL paper, although it doesn't look like the version on arxiv has the proof (it's not too hard).

Chad Nester (Jun 04 2021 at 16:30):

I also gave a talk about this at SYCO5/STRINGS3 (there's a video/slides)

Chad Nester (Jun 04 2021 at 16:33):

Notice that as a consequence of all this, the partial functions that are natural with respect to the counits (i.e., that delete properly) are precisely the total functions.

Chad Nester (Jun 04 2021 at 16:44):

James Wood said:

And yeah, I've convinced myself that neither is 1 terminal (0 is) nor is × the limit-defined product (there is no pairing for partial functions that disagree on definèdness on any element of their domain). Maybe there is a product for partial functions, at least assuming excluded middle, but I don't think I want to use it. So I don't get to reuse the nice theorem about Cartesian monoidal structure.

It turns out that the kind of product and terminal object (called "restriction products" and "restriction terminal object") that exist in sets and partial functions are limits, after a fashion. Specifically they arise as formal limits in the 2-category of restriction categories, restriction semifunctors, and lax transformations thereof. The discrete cartesian restriction categories are the ones with all limits in this sense.

Chad Nester (Jun 04 2021 at 16:45):

The reference is this, although frankly the literature on this is scattered and relatively inaccessible.

Nathanael Arkor (Jun 04 2021 at 16:50):

The discrete cartesian restriction categories are the ones with all limits in this sense.

All limits, or just the discrete limits (in both senses of the word "discrete")?

Chad Nester (Jun 04 2021 at 16:56):

All limits.

Chad Nester (Jun 04 2021 at 16:57):

Ahh sorry. All finite limits. My mistake.

Chad Nester (Jun 04 2021 at 17:00):

I guess the cartesian restriction categories (not necessarily discrete) would be the ones with all finite discrete limits... which is confusing.

Nathanael Arkor (Jun 04 2021 at 17:01):

Why do discrete cartesian restriction categories have restriction pullbacks?

Chad Nester (Jun 04 2021 at 17:03):

It's easier to explain why they have a kind of equalizer. Essentially the codiagonal map ("multiplication") is a kind of partial equality test -- defined iff its inputs are equal.

Chad Nester (Jun 04 2021 at 17:06):

In the literature these are called "latent equalizers", with "latent limits" being the sort of limits I'm talking about. Splitting restriction idempotents moves us to another 2-category (all the 0-cells have split restriction idempotents, and the 1-cells are restriction functors instead of restriction semifunctors). Limits in this other 2-category are called "restriction limits", and if we restrict to the 0-cells that happen to be discrete cartesian restriction categories (with split restriction idempotents), then this is equivalent to the 2-category of categories with finite limits, finite limit preserving functors, and natural transformations.

Chad Nester (Jun 04 2021 at 17:07):

More concretely: If I have a discrete cartesian restriction category with split idempotents, then the category of total maps has finite limits. Conversely, the category of partial maps (spans with monic left leg) in any category with finite limits is a discrete cartesian restriction category with split restriction idempotents.

Chad Nester (Jun 04 2021 at 17:09):

If we drop the "with split restriction idempotents" part then we have to work with the "latent" limits, and in the weird 2-category, to obtain that discrete cartesian restriction categories are the ones with all finite (formal) limits.

Chad Nester (Jun 04 2021 at 17:09):

... but you can do it!

Nathanael Arkor (Jun 04 2021 at 17:09):

Oh, so a discrete cartesian restriction category has all finite latent limits, and if it is split, it additionally has all finite restriction limits (essentially by definition)?

Chad Nester (Jun 04 2021 at 17:09):

Yes.

Nathanael Arkor (Jun 04 2021 at 17:09):

Chad Nester said:

If we drop the "with split restriction idempotents" part then we have to work with the "latent" limits, and in the weird 2-category, to obtain that discrete cartesian restriction categories are the ones with all finite (formal) limits.

Right, got it, thanks!

Nathanael Arkor (Jun 04 2021 at 17:10):

There are lots of interesting subtleties with restriction categories.

Chad Nester (Jun 04 2021 at 17:11):

Everything gets harder when you don't want to insist on split restriction idempotents :exhausted:

James Wood (Jun 05 2021 at 07:26):

By any chance, is there a well behaved notion of rig object in a Cartesian restriction category (given that I secretly care about partial rigs and whether they're interesting)? I think the naïve definition of partial rig is ill behaved because partial modules over such a partial rig have no 0 object, or something like that.

Chad Nester (Jun 06 2021 at 09:53):

I guess the obvious notions of partial rig are where the multiplication is a partial function, the addition is a partial function, or both are partial functions. I think you get a sensible category of partial rigs in all three cases, although I don’t know about the modules. Has anyone studied this? (I’d be interested to know!)

Karem (May 07 2022 at 02:37):

I am new to zulip if I wish to discuss algebraic geometry argument which channel do I use?

John Baez (May 07 2022 at 04:34):

Hi! Go to #theory: algebraic geometry

Karem (May 07 2022 at 05:01):

Thanks! Zulip is pretty cool!