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: Q-Cat and hyperdoctrines

Mike Stay (Nov 15 2021 at 19:32):

A hyperdoctrine is roughly a situation where it makes sense to take preimages and there are left and right adjoints to it (the existential and universal quantifiers).

A Q-category is a category enriched in commutative involutive quantales. More concretely, a Q-category X is

• a pair $(|X|, X:|X|^2 \to Q)$

such that

• $Q$ is a commutative involutive quantale,
• $|X|$ is a set, and
• $X$ satisfies $1 \le X(x,x)$ and $X(x_2,x_3) \otimes X(x_1, x_2) \le X(x_1, x_3)$.

In the category of sets, there are two ways to express the preimage of a function. Given $f:X \to Y$ and $S \subseteq Y$,

$f^*S = \{ x | \exists y \in Y. f(x) = y \land y \in S \} = \{ x | \forall y \in Y. f(x) = y \Rightarrow y \in S \}$

Moving to Q-categories, we're given a Q-functor $f:X \to Y$ and a "Q-predicate on Y", a function $S:|Y| \to Q$. Then the preimage of $f$ should map a Q-predicate on $Y$ to a Q-predicate on $X$. The two ways above become

$\displaystyle f^{*1}S = \lambda x. \bigvee_{y \in |Y|} Y(f(x), y) \otimes S(y)$ and
$\displaystyle f^{*2}S = \lambda x. \bigwedge_{y \in |Y|} Y(f(x), y) \multimap S(y)$

These aren't equal in general. Is one guaranteed to be less than or equal than the other?

There's a natural notion of existential and universal quantifiers. Let $T$ be a Q-predicate on X. Then we get Q-predicates on Y via
$\displaystyle \exists_f T = \lambda y. \bigvee_{x \in |X|} Y(f(x), y) \otimes T(x)$
$\displaystyle \forall_f T = \lambda y. \bigwedge_{x \in |X|} Y(f(x), y) \multimap T(x)$

I've checked that $T \le f^{*1}\exists_f T$ and $\exists_f f^{*2} T \le T$. I presume that something similar holds for the universal. So this isn't quite a hyperdoctrine, but it's something close. Has anyone seen something like this elsewhere?

Mike Shulman (Nov 15 2021 at 20:23):

That's a weird notion of Q-predicate. Wouldn't a more natural notion of Q-predicate be a Q-functor $S:Y\to Q$? In that case, I think your two definitions of preimage both just reduce to $S(f(x))$, by the Yoneda and co-Yoneda lemmas.

Mike Stay (Nov 15 2021 at 20:27):

Q-functor S:Y → Q

Oh, good point! Thanks, that clears everything up.