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: Quantifiers as adjoints and equality

Jencel Panic (Nov 12 2023 at 09:52):

This is a spinoff to the discussion we have on "Beginner questions" on the topic of quantifiers as adjoints. I want to point out some connections that I see between the adjunctions and categorical equivalences, particularily when it comes to quantifiers. I am doing it in a separate topic, because I am not sure if I am correct and I don't want to confuse people.

My source for this is example 7.1.1.13 from Spivak's "Category theory for the sciences", namely the fact that given a function $p: A \to B$ the inverse image of this function $p^{-1} : P(B) \to P(A)$ is left adjoint of the $\forall p : P(A) \to P(B)$ and right adjoint of $\exists p : P(A) \to P(B)$.

image.png

Now, if I got the picture right, one thing I am noticing is that besides adjunctions, these pairs of functors define a "half-equivalence" or "one-direction equivalence" (I swear there was a name for this, but I don't remember it). So, on one hand we have $\forall p \circ p^{-1}= ID_{B}$ (but we don't have the other direction $p^{-1} \circ \forall p \neq ID_{A}$). And same for exists --- we have $p^{-1} \circ \exist p = ID_{B}$, but not the other direction.

Moreover, in the cases where the function $p$ is an isomorphism, this partial equivalence becomes full equivalence (I think that's not the only case, but I am not sure).

The same things can happen if we remove some elements from $P(A)$.

Here is a visualization of the example in the book --- the adjunction between the inclusion order of the natural numbers and the inclusion order of the set ${even, odd}$, that is generated by the function $isEven : \mathbb{N} \to Bool$.

Jencel Panic (Nov 12 2023 at 09:56):

B941E9DE-BF8D-499C-93C7-8EE058208FF0.jpg

Todd Trimble (Nov 12 2023 at 12:22):

It's even better to refer to specific morphisms as isomorphisms or not. So instead of wondering whether, for example, $p^{-1} \circ \exists p$ is the identity, the issue should be whether the unit of the adjunction $\exists p \dashv p^{-1}$, which is of the form

$1_B \to p^{-1} \circ \exists p,$

is an isomorphism. Of course if your categories are posets, this is asking the same thing since there is at most one morphism between these functors to begin with. But in general, it's better to ask the second question.

Todd Trimble (Nov 12 2023 at 12:23):

This is a great example to work with when learning adjoints, because the functors here are very familiar constructions. $\exists p: PA \to PB$ takes a subset $X$ of $A$ to its direct image $p(X)$, so the statement that we have an adjunction $\exists p \dashv p^{-1}$ is that for subsets $X, Y$ of $A, B$ respectively, $p(X) \subseteq Y$ if and only if $X \subseteq p^{-1}(Y)$. The unit assigns to each such $X$ a subset inclusion $X \subseteq p^{-1}(p(X))$, and the counit assigns to each such $Y$ a subset inclusion $p(p^{-1}(Y)) \subseteq Y$.

Todd Trimble (Nov 12 2023 at 12:23):

Here, the unit is an isomorphism iff $p$ is injective. For example, consider a noninjective function like the function $p: \{a, b\} \to \{1\}$. Notice that $p^{-1}(p(\{a\})) = p^{-1}(\{1\}) = \{a, b\}$, so the unit component $\{a\} \subseteq (p^{-1} \circ p)(\{a\})$ is not an isomorphism. Incidentally, in general when the unit is an isomorphism, the left adjoint part is called a coreflection.

Todd Trimble (Nov 12 2023 at 12:23):

There is also a nice exercise that the counit of $\exists p \dashv p^{-1}$ is an isomorphism iff $p$ is surjective.

Todd Trimble (Nov 12 2023 at 12:23):

It's also a nice exercise to work out the situation for $p^{-1} \dashv \forall p$. In the context of classical logic, $\forall p: PA \to PB$ is given by the formula $\neg_B \circ \exists p \circ \neg_A$ where $\neg$ denotes complement.

John Baez (Nov 12 2023 at 15:03):

Jencel Panic said:

Now, if I got the picture right, one thing I am noticing is that besides adjunctions, these pairs of functors define a "half-equivalence" or "one-direction equivalence" (I swear there was a name for this, but I don't remember it).

As Todd hinted, the relevant buzzwords include [[reflective subcategory]] and various other terms based on 'reflection' and 'coreflection'.

Jencel Panic (Nov 12 2023 at 15:21):

Thanks a lot, nice to know that I was on the right track.

Todd Trimble (Nov 12 2023 at 17:42):

Yeah, I think "reflection" and "coreflection" are supposed to be applied to the functors that behave more like retractions, so I slightly misspoke. I'll excuse myself by saying I wrote this just after I woke up this morning. One can say "reflective embedding" or similar for the functor that behaves more like the section.

Anyway, Jencel: you had omitted saying anything about $p$ being injective or surjective, so in part my comment was correcting this.

Jencel Panic (Nov 13 2023 at 02:44):

Sorry, it seems I made a mistake in the formula.

I meant to say:
$\forall p \circ p^{-1}= ID_{B}$
$\exist p \circ p^{-1} = ID_{B}$.

so the counit of Exists and the unit of Forall are isomorphisms i.e. we have a partial equivalence for both adjunctions (in different directions). This should be valid even if $p$ is not injective, I think (the $isEven$ function I am using in the graphic is not).

Jencel Panic (Nov 13 2023 at 02:48):

This is a great example to work with when learning adjoints, because the functors here are very familiar constructions.

Well, it's the only way for me to learn currently, I get lost quick in formulas, so if I don't draw a diagram of something I usually cannot grasp it at all.

Todd Trimble (Nov 13 2023 at 12:41):

As I said, $\exists p \circ p^{-1} = 1_{PB}$, i.e., the counit of $\exists p \dashv p^{-1}$ is an isomorphism, iff $p$ is surjective.

Jencel Panic (Nov 13 2023 at 12:48):

Aha, thanks, makes sense.

Todd Trimble (Nov 13 2023 at 12:53):

Similarly, $1_{PB} = \forall p \circ p^{-1}$, i.e., the unit of $p^{-1} \dashv \forall p$ is an isomorphism, iff $p$ is surjective.

Jencel Panic (Nov 13 2023 at 12:57):

Yes, I got the picture, units/counits that are from $B$ to $A$ are isomorphisms if $p$ is surjective and ones from $A$ to $B$ --- if it is injective. The only thing that I still don't know is why.

Todd Trimble (Nov 13 2023 at 13:06):

The following may be higher-brow than necessary, but since both $\exists p$ and $p^{-1}$ are left adjoints, they preserve colimits, i.e., unions, and since every subset is a union of singletons, it suffices to check what's happening with singletons. (And this I'll leave as an exercise.)