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

Topic: lifting operations

Christian Williams (May 06 2020 at 01:03):

Let's say we have an operation $op:A\times B\to C$. We can lift this operation to subsets, $\bar{op}:P(A)\times P(B)\to P(C)$ by defining $\bar{op}(U,V) = \{op(a,b)\; | \; a\in U\land b\in V\}$. We do this all the time, for example when we add and multiply ideals of a ring.

Christian Williams (May 06 2020 at 01:03):

This works because the subset functor, $P(-):\mathrm{Set\to Pos}$ is lax monoidal with respect to product; there is a canonical map $\sqcap_{AB}:P(A)\times P(B)\to P(A\times B)$ given by $(U,V)\mapsto U\times V\subset A\times B$.

Christian Williams (May 06 2020 at 01:04):

Since $P(-):\mathrm{Set\to Pos\subset Cat}$ is an indexed category, we can apply the Grothendieck construction to get the category $\int P$ whose objects are set-subset pairs $(A,U)$ and morphisms $(A,U)\to (B,V)$ are functions $f:A\to B$ so that $f(U)\subset V$.

Christian Williams (May 06 2020 at 01:05):

A nice consequence $(P,\sqcap)$ being lax monoidal is that this gives $\int P$ products, defined as one might expect: $(A,U)\times (B,V)=(A\times B, U\times V)$.

Christian Williams (May 06 2020 at 01:06):

Currently, I'm very interested in the fact that $\int P$ also has an internal hom.

Christian Williams (May 06 2020 at 01:08):

Given $U\subset A$ and $B\subset V$, it's natural to consider the set of functions for which $f(U)\subset V$. We can define $(A,U)\multimap (B,V) := ([A,B],\{f:A\to B\; | \; x\in U\Rightarrow f(x)\in V\})$.

Christian Williams (May 06 2020 at 01:12):

If you think about this for a while, you can see that this gives an internal hom for $\int P$. We have a natural isomorphism $\int P((C,Z)\times (A,U),(B,V)) \simeq \int P((C,Z),(A,U)\multimap (B,V))$. The reason why is really just because the condition $f(U)\subset V$ is baked into the definition of morphism from the start.

Christian Williams (May 06 2020 at 01:14):

However, I haven't found a good reference for this construction yet. I can see that this is something that works for any topos; we can repeat this construction for subobjects in any category with enough structure. Does someone know where I can find an explication of this structure -- the "cartesian closed subobject fibration"?

Christian Williams (May 06 2020 at 01:28):

In Jacobs' Categorical Logic and Type Theory, they discuss "fiberwise structure" -- an indexed category $F:C\to \mathrm{Cat}$ has "fibered --'s" if every $F(c)$ has "--" and reindexing functors $F(f):F(c)\to F(d)$ preserve those "--'s".

Christian Williams (May 06 2020 at 01:31):

So for example, $P:\mathrm{Set\to Pos}$ really gives Heyting algebras, which are cartesian closed. If we use the covariant version, then direct image $P(f):P(A)\to P(B)$ does not in general preserve implication. But the contravariant one, given by preimage, does. I guess this is a classic example of what would be called a "cartesian closed fibration".

Christian Williams (May 06 2020 at 01:32):

But I'm still catching up on all this -- I arrived at the hom another way, and I'm wondering whether the way I constructed it is a consequence of this idea, or whether it is somehow distinct.

Christian Williams (May 06 2020 at 01:35):

This is how I originally constructed the hom. subhom.png

Christian Williams (May 06 2020 at 01:39):

This constructs it in stages: given $(U,V)$, we can form $(U\times [A,B], \{(a,f)\; | \; f(a)\in V\}$. Then we use the Heyting algebra implication to form the set $\{(a,f)\; | \; a\in U\Rightarrow f(a)\in V\}$. This is the part that's doing the hard work, and also destroying a lot of information. Then finally, we just throw away the first component.

Christian Williams (May 06 2020 at 01:40):

Since I haven't found a reference that takes a "cartesian closed indexed category" $F$ and gives the explicit construction of how $\int F$ is cartesian closed, I'm not sure whether or not the above construction is a general method.

Christian Williams (May 06 2020 at 01:41):

All thoughts are welcome. Right now I'm going to go for a walk.

Paolo Capriotti (May 06 2020 at 06:16):

One observation that might be useful is that your $\int P$ is equivalent to the quasitopos of separated presheaves on the walking arrow, where the arrow itself is a cover.

sarahzrf (May 06 2020 at 07:27):

this seems apropos https://ncatlab.org/nlab/show/external+tensor+product

sarahzrf (May 06 2020 at 07:27):

i haven't really read that page—i pulled it up while looking for "external tensor product" b/c i recalled the operation you were doing as resembling the "external tensor product" described on the page for Day convolution

Morgan Rogers (he/him) (May 06 2020 at 09:26):

The forgetful functor from $\int P$ to $\mathrm{Set}$ has a left and a right adjoint (sending a set $A$ to $(A,\emptyset)$ and $(A,A)$ respectively). From your definition, it preserves the cartesian-closed structure too. It looks like both of the adjoints preserve a bunch of limits and colimits respectively. Even if you can't usefully apply a monadicity result because the forgetful functor isn't the conservative one, that functor likely preserves enough structure that you can recover the structure on $\int P$ as a lifting of that in $\mathrm{Set}$.

Matteo Capucci (he/him) (May 06 2020 at 18:48):

I guess you're describing (something really close to) the most basic example of tripos, i.e. the tripos of subobjects of the topos Set. It's also similar to how realizability triposes are defined, especially in the definition of the internal hom.

Matteo Capucci (he/him) (May 06 2020 at 18:49):

I find van Oosten's Categorical Realizability quite readable if you have some logical intuition.

Mike Shulman (May 06 2020 at 19:41):

I said this to you privately, but I'll add it to the discussion here too in case anyone else wants to add to it. The objects of your $\int P$ are monomorphisms in Set; if you remove this restriction and look at just the arrow category of Set, and regard it as the Artin gluing of the identity functor $\mathrm{Set} \to \mathrm{Set}$, i.e. the comma category $(\mathrm{Id}_{\mathrm{Set}} \downarrow \mathrm{Id}_{\mathrm{Set}} )$, then this is the usual construction of cartesian-closed structure on a gluing category, which happens to preserve monos.

Christian Williams (May 07 2020 at 16:42):

Thanks for the helpful ideas. This is enough to keep me learning for now.

Christian Williams (May 07 2020 at 16:47):

A couple other things I was wondering... How does this map $\multimap: P(A)^{op}\times P(B)\to P([A,B])$ relate to lax closed structure of the subobject functor? We have a map $\lambda:P([A,B])\to [P(A),P(B)]$ given by the currying of the product-lax evaluation. It also has a right adjoint $\rho:[P(A),P(B)]\to P([A,B])$ which I care about. How might this be connected with the subobject hom? Does $\multimap$ possibly have an adjoint? I've been trying to find one, but it doesn't seem like it.

Christian Williams (May 07 2020 at 16:50):

$\lambda (S)(U) = \{f(u)\; | \; f\in S, u\in U\}$ and $\rho(F) = \{f:A\to B\; | \; \forall U\in P(A).\; \exists_f(U)\subset F(U)\}$.