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: theory: applied category theory

Topic: Rel(Cat) construction and epimorphisms in Cat from a less...


view this post on Zulip Avi Craimer (Mar 07 2025 at 19:01):

Hi,

I've long been interested in the potential of the category of sets in relations for use in practical applications like knowledge representation. I recently was reading on the nlab page about a generalization of the construction of Rel from set for any regular category. https://ncatlab.org/nlab/show/Rel#relations_in_a_category

I was working through this construction to try to fill in the details as concretely as possible. I wrote up these notes.
Generalizing the Rel Construction to Regular Categories.pdf

I'll share them here in case it's useful for anyone, and also so that those with more knowledge than me can point out any mistakes.

The next thing I want to do is try to work out a similarly concrete description of the construction for Rel(Cat). I am struggling with understanding the definition of an epimorphism in Cat, which is necessary for the final step of the construction when you split the projection from the pullback in order to get the actual composition of subcategories.

I read this post about it
https://math.stackexchange.com/questions/693970/monomorphisms-and-epimorphisms-in-the-category-of-small-categories

Which refers to an article Epimorphisms and domininions, III by John Isbell.

I found the paper itself somewhat forbidding, and I'm wondering if anybody might know of a resource that explains the zig zag theorem a little bit more pedagogically and step-by-step (with pictures if possible!)

view this post on Zulip Spencer Breiner (Mar 07 2025 at 19:22):

You should note that Cat is not regular. One of the requirements is pullback-stability of reg-epis, and this fails in Cat (or even Pos).

The simplest example involves a pair of arrows 232+22\to 3 \leftarrow 2+2, where 22 and 33 are the walking arrow 010\to 1 and the walking composite 0120\to 1\to 2.

view this post on Zulip Avi Craimer (Mar 07 2025 at 19:53):

Oh, thanks that probably saves me a lot of time :face_with_peeking_eye:

So I guess then you can't use the Rel(C) construction for Cat?

I wonder if there are any work arounds? I have some ideas of my own for defining a practical notion of a Relator which is to a functor what a relation is to a function. I'm pretty sure it's possible to define a category where categories are objects and relators are morphisms.

I've proven that Relators from C to D are isomorphic to subcategories of C x D.

Here: https://github.com/AviCraimer/relational-calculus-library-lean4/blob/rel-cat/RelationalCalculus/CategoryTheory/Relator.lean

I think the Relator definition, even though it's equivalent to subcategory of product is possibly useful for applied settings where we want to define relations between categories in terms of ordinary relations.

For those who don't speak Lean, here is the definition in notation.

Definition Relator

Let C\mathcal{C} and D\mathcal{D} be categories. A relator RR from C\mathcal{C} to D\mathcal{D} consists of:

A relation RobOb(C)×Ob(D)R_{ob} \subseteq Ob(\mathcal{C}) \times Ob(\mathcal{D})

A relation RmorphMorphism(C)×Morphisms(D)R_{morph} \subseteq Morphism(\mathcal{C}) \times Morphisms(\mathcal{D})

Note: RobR_{ob} and RmorphR_{morph} are just regular relations between sets satisfying the following conditions:

  1. Identities for related objects:

For all objects COb(C)C \in Ob(\mathcal{C}) and DOb(D)D \in Ob(\mathcal{D}),

(C,D)Rob(C, D) \in R_{ob} if and only if, (idC,idD)Rmorph(id_C, id_D) \in R_{morph}.

  1. Objects Endpoints for Related Morphisms:

For all objects C,COb(C)C, C′ \in Ob(\mathcal{C}) and D,DOb(D)D, D′ \in Ob(\mathcal{D}), and for all morphisms fC[C,C],gD[D,D]f \in \mathcal{C}[C, C′], g \in \mathcal{D}[D, D′]

if (f,g)Rmorph(f, g) \in R_{morph}, then

(C,D)Rob(C, D) \in R_{ob} and (C,D)Rob(C′, D′) \in R_{ob}

This ensures that for any related morphisms, the object endpoints of those morphisms are also related.

  1. Composition for related composable pairs of morphims:

For any f1:C1C2f₁: C₁ \to C₂ and f2:C2C3f₂: C₂ \to C₃ in C\mathcal{C} and corresponding g1:D1D2g₁: D₁ \to D₂ and g2:D2D3g₂: D₂ \to D₃ in D\mathcal{D}

If (f1,g1)Rmorph(f₁, g₁) \in R_{morph} and (f2,g2)Rmorph(f₂, g₂) \in R_{morph}, then

(f2f1,g2g1)Rmorph(f₂ \circ f₁, g₂ \circ g₁) \in R_{morph}.

view this post on Zulip John Baez (Mar 07 2025 at 21:02):

Is a 'relator' from CC to DD the same as a subcategory of C×DC \times D? It looks like it to me, though I didn't take a lot of time to check everything.

view this post on Zulip John Baez (Mar 07 2025 at 21:03):

Very often when people try to generalize relations from Set\mathsf{Set} to Cat\mathsf{Cat} they work with [[profunctors]] between categories.

view this post on Zulip Avi Craimer (Mar 07 2025 at 21:37):

I said in my post above that a Relator is equivalent to a subcategory. I proved it in the Lean code I linked to.

I think the Relator definition, even though it's equivalent to subcategory of product is possibly useful for applied settings where we want to define relations between categories in terms of ordinary relations.

I am aware of the idea that Profunctors generalize relations for a categorical setting. But as far as I can tell Profunctors act like generalized relations for objects of categories, but they still operate deterministically on morphisms of categories. I'm trying to find a definition that allows relational mappings of both objects and mrophisms. I'd consider this more in keeping with the spirit of relations between sets. That's basically a sub-category.

I'm still working on formalizing the composition of relators, but the basic idea is this.

R;Sob:=Rob;SobR;S_{ob} := R_{ob};S_{ob}

For morphisms you do a preliminary composition:

RSpremorph:=Rmorph;SmorphRS_{premorph} := R_{morph};S_{morph}

Then you add any compositions of morphisms related in R;SpremorphR;S_{premorph}.

R;Smorph(f:cc)(g:ee):=RSpremorphfgR;S_{morph} (f: c \to c')(g: e \to e') := RS_{premorph} f g \vee
(f1,f2)(g1,g2),RSpremorph(f1,g1)RSpremorph(f2,g2)f=f1;f2g=g1;g2 \exists (f_1, f_2) (g_1, g_2), RS_{premorph} (f1, g1) \wedge RS_{premorph}( f2, g2) \wedge f = f_1;f_2 \wedge g = g_1;g_2

I need to check about identities, but at least for composition closure I think this should results in R;S being a Relator. I also need to check associativity.

view this post on Zulip Kevin Carlson (Mar 07 2025 at 21:49):

No, profunctors don't give a deterministic mapping between morphisms. A profunctor includes both a span on objects and a (closely related) span on morphisms. For instance, the profunctor from the walking arrow A=01A=0\to 1 to A+AA+A with a single heteromorphism connecting each object ii in the domain to each of its two copies in the codomain, and in which all possible squares commute, represents the relation relating the arrow of AA to both its copies in the codomain.

view this post on Zulip Kevin Carlson (Mar 07 2025 at 21:54):

It is critical to the usefulness of relations that they correspond to boolean-valued functions on the cartesian product. Boolean-valued functors correspond only to certain very strong full subcategories (sieves), which is why we generalize to set-valued functors, i.e. profunctors.

You can represent an arbitrary relator RA×BR\subseteq A\times B via a profunctor by adding a heteromorphism hab:abh_{ab}: a\to b whenever aRba R b and adding relations saying fhabg=habf\cdot h_{ab} \cdot g=h_{a'b'} whenever (f,g):(a,b)(a,b)(f,g):(a',b)\to (a,b') and fRg.f R g.

view this post on Zulip John Baez (Mar 07 2025 at 23:05):

Avi Craimer said:

I said in my post above that a Relator is equivalent to a subcategory.

Sorry, I didn't notice that!

I'm curious whether the (2-)category of categories and relators (and some sort of transformations between relators) is a sub-(2-)-category of categories and profunctors (and natural transformations between profunctors).

(The parenthetical stuff could be skipped on a first pass, but we really need natural transformations between profunctors, much as Mac Lane said he and Eilenberg invented categories and functors mainly in order to be able to talk about natural transformations. So, if you can figure out how to compose relators, it might then pay to study transformations between them.)

view this post on Zulip Avi Craimer (Mar 08 2025 at 00:34):

Well @John Baez thanks for that idea.

And thanks to @Kevin Carlson for the clarification about profunctors and non-determinism. I wanted to ask a follow up, which is that the other way in which profunctors could be less relational with respect to morphisms is that you can't have partial relations between morphisms if the endpoint objects are related.

This also speaks to John's question about whether every relater is a certain kind of profunctor. I think about a following potential counterexample.

Start with a category C which has at least one non-identity morphism. Define a relator D: C -> C that discretizes C, that is it relates every object to itself, and every identity morphism to itself, but does not relate any other morphisms. I don't think that would be possible as a profunctor since the functorality would require us to map all the morphisms. But, I don't understand the profunctor-as-relation interpretation that well, so maybe there is some way of interpreting a certain kind of functorial mapping as effectively throwing away unrelated pairs of morphisms.

view this post on Zulip Avi Craimer (Mar 08 2025 at 01:19):

Kevin Carlson said:

You can represent an arbitrary relator RA×BR\subseteq A\times B via a profunctor by adding a heteromorphism hab:abh_{ab}: a\to b whenever aRba R b and adding relations saying fhabg=habf\cdot h_{ab} \cdot g=h_{a'b'} whenever (f,g):(a,b)(a,b)(f,g):(a',b)\to (a,b') and fRg.f R g.

If you have a chance to explain this a bit more I'd be grateful. I don't really understand what you mean by a heteromorphism.

view this post on Zulip Kevin Carlson (Mar 08 2025 at 01:24):

One way to describe a profunctor is simply as a category CC that contains AA and BB as disjoint full subcategories, there are no other objects, and such that there are no morphisms from bb's to aa's, only in the other direction. Morphisms from aa's to bb's can be called "heteromorphisms", because they're like morphisms that cross between different categories. The way to recover the definition as a functor on Aop×BA^{\mathrm{op}}\times B is by mapping (a,b)(a,b) to the set C(a,b)C(a,b) of heteromorphisms crossing from aa to b.b. So you can construct profunctors by asserting the existence of some certain heteromorphisms, requiring some relations such as, in the case I gave, afab=agbba'\stackrel{f}{\to} a \to b= a'\stackrel{g}{\to}b'\to b when aRb,aRb,fRg,aRb, aRb',fRg, and then freely generating the category resulting from those relations. The fact that morphisms only run from AA across to BB means the resulting category has no new morphisms between aa's or between bb's, as required by the definition.

view this post on Zulip Kevin Carlson (Mar 08 2025 at 01:27):

That much is standard; I don't actually know anything about the properties of my suggested construction of a profunctor from a relator, which I just made up. But I bet something like that will subsume anything you'd want to do with relators, and I wonder whether attempts to compose relators (which might get weird due to the irregularity of Cat) will more naturally push you into profunctor composition anyway. That said, a simpler and more widely-applicable way to work with a relation-like structure in a non-regular category is to use plain spans.

view this post on Zulip Ryan Wisnesky (Mar 08 2025 at 01:50):

This paper describes in detail two notions of pro-functor presentation, including the one described by Kevin, and a "curried" version similar to relational conjunctive queries: https://arxiv.org/abs/2404.01406