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: Descent of relations along a surjection (kernel pair invaria

Daisuke Hirota (Jan 28 2026 at 03:22):

Hi all — I have a question about when a binary relation “descends” along a quotient.

Setup: let $\rho : L \twoheadrightarrow \Sigma$ be a surjection, and let $R \subseteq L \times L$ be a relation.
I want a relation $\bar R \subseteq \Sigma \times \Sigma$ such that

$$(x,y)\in R \iff (\rho(x),\rho(y))\in \bar R. \ker(\rho)\circ R\circ \ker(\rho)=R.$$

What I think is true (Set-level): this is equivalent to $R$ being constant on $(\rho\times\rho)$-fibers, i.e. invariant under the kernel pair of $\rho$. Equivalently (viewing relations as morphisms in $\mathrm{Rel}(\mathrm{Set})$),

Questions:

1. What is the standard categorical framing/terminology for this? (e.g. “a subobject of $L\times L$ is the pullback of a subobject of $\Sigma\times\Sigma$ along $\rho\times\rho$”, or a statement purely in terms of the kernel pair / effective equivalence relations)
2. Are there references where this exact fact is stated explicitly? (regular/exact categories, allegories, etc.)

I suspect it’s standard, but I couldn’t locate a clean reference for this specific formulation.
Thanks!

Morgan Rogers (he/him) (Jan 28 2026 at 11:35):

In a regular category, the relation $\{(\rho(x),\rho(y)) | (x,y) \in R\}$ is the image of $R$, viewed as a subobject of $L \times L$, along $\rho \times \rho$. The pullback of a relation along a morphism also exists, and these two operations form an adjunction (aka a Galois connection since we're talking about posets of subobjects). So $R$ needs to be a fixed point of that Galois connection.
Potentially relevant topic: allegories (which axiomatize categories of relations)

Daisuke Hirota (Jan 29 2026 at 01:50):

@Morgan Rogers (he/him)
Thanks Morgan, this really clarified things for me :folded_hands:
I’m going to dig into the relevant nLab pages first, and if I still have questions I’ll post them here.

David Michael Roberts (Jan 29 2026 at 03:17):

What Morgan stated though is not the same as what you described [(x,y) \in R <=> (rho(x),rho(y))\in Rbar]. It's the difference between the left and right adjoint to the preimage functor on subobject posets: the image corresponds to \exists_{\rho\times\rho} R and the thing you describe is, I think, \forall_{\rho\times\rho} R

Daisuke Hirota (Jan 29 2026 at 03:57):

@David Michael Roberts
David, thanks! That makes sense. With $f = \rho \times \rho$, what Morgan described is the direct image (the $\exists_f$ side), which generally yields

$$R \subseteq f^*(\exists_f(R)).$$

There's also the opposite-direction approximation

$$f^*(\forall_f(R)) \subseteq R,$$

and in Set one can bracket

$$f^*(\forall_f(R)) \subseteq R \subseteq f^*(\exists_f(R)).$$

The picture I have in mind is precisely this "two-sided" structure. My understanding is that regular categories canonically give the $\exists_f$ side via images, but $\forall_f$ is extra structure.
Is it standard to get $\forall_f$ (right adjoints to reindexing on subobjects, stable under base change) by assuming a Heyting category?

David Michael Roberts (Jan 29 2026 at 04:03):

The existence of $\forall_f$ is the definition of a Heyting category!

Morgan Rogers (he/him) (Jan 29 2026 at 08:55):

@David Michael Roberts maybe I'm missing something, but the first condition Daisuke asked for amounts to being a fixed point for the adjunction I described, no? Why do you need universal quantification?

Morgan Rogers (he/him) (Jan 29 2026 at 09:06):

Or to put it another way, both adjunctions give a way of taking a generic $R$ and turning it into one satisfying the condition that Daisuke asked for, with $\exists$ giving the smallest relation including $R$ and $\forall$ the largest relation contained in $R$ with this property.

David Michael Roberts (Jan 29 2026 at 09:58):

It's the if and only if, no? If rho(x)=rho(x') and similarly for y,y', then (x,y) in R => (rho(x),rho(y))in Rbar =>(x',y') in R. So one needs the whole fibre over (rho(x),rho(y)) to sit inside R for that element to be in Rbar.

David Michael Roberts (Jan 29 2026 at 09:59):

I don't understand the other condition!

Morgan Rogers (he/him) (Jan 29 2026 at 10:58):

We need $\bar{R} \supseteq \exists_{\rho \times \rho}(R)$ to have the forward implication, and pulling back provides all of the pairs $(x',y')$ such that $(\rho(x'),\rho(y'))\in \bar{R}$ so $R \supseteq (rho \times \rho)^*(\bar{R})$ for the backwards implication.

David Michael Roberts (Jan 29 2026 at 11:22):

Oh, OK, thanks.