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: logic inherited by functor categories

David Egolf (Jun 08 2023 at 17:12):

Let $\mathsf{C}$ be a category that has some properties that make it suitable for doing logic in. For concreteness, let's say that $\mathsf{C}$ is a Boolean algebra. So, $\mathsf{C}$ has all finite products, all finite coproducts, and an appropriate notion of negation. That means we can talk about the "and" the "or" and the "not" of objects. I'm intuitively thinking of each object of $\mathsf{C}$ as a predicate, where there is a morphism from $a$ to $b$ under this condition: whenever some input to the predicate $a$ produces a true proposition then providing that same input to the predicate $b$ also yields a true proposition.

I'm interested in taking a setting like the above that is nice for doing logic, and obtaining a new setting that also lets us talk about the "and", "or" and "not" of objects. One idea that occurs to me is to consider sequences of objects in $\mathsf{C}$, with the aim being to model different levels of confidence. For example, we might want to consider a category where objects are 3-tuples of objects in $\mathsf{C}$, say $(c, c', c'')$, where we are "not confident" in $c$, "fairly confident" in $c'$ and "very confident" in $c''$. This leads me to consider the functor category $[3, \mathsf{C}]$, where $3$ is the thin category with three objects having this shape: $0 \to 1 \to 2$.

I am wondering if the operations "and", "or", and "not" available in $\mathsf{C}$ are also available in $[3, \mathsf{C}]$. I would like to be able to apply these operations in this setting, in order to obtain a strategy for reasoning in presence of multiple of levels of confidence.

I'm also interested in a more general question. If $\mathsf{D}$ is some small category, and $\mathsf{C}$ is a Boolean algebra, then when (if ever) does the functor category $[\mathsf{D}, \mathsf{C}]$ inherit the operations of "and", "or" and "not" from $\mathsf{C}$?

(By the way - I'm more interested in understanding how to analyze questions like this than knowing the answer for this specific case. So, general concepts and techniques related to this kind of question are of interest to me!)

Kevin Arlin (Jun 08 2023 at 17:58):

The operations of conjunction and disjunction in a Boolean algebra are examples of limits and colimits, respectively. If $\mathbf C$ is any category with (co)limits of some shape $J,$ then $[\mathbf D,\mathbf C]$ always has the same (co)limits computed pointwise. You might have seen an argument like this in a case of functors into a bigger category like $$\mathbf{Set}.$ $

Negation is more interesting! In about the simplest possible case, $\mathbf D= (0\to 1),$ we see that $[\mathbf D,\mathbf C]$ no longer has negations, i.e. is no longer a Boolean algebra, in general. Indeed, given an arrow $a\le b$ in $\mathbf C,$ its negation must be an arrow $\neg a\le \neg b$ (since $\wedge$ and $\vee$ are computed levelwise, so such an arrow is the only thing that could intersect $a\le b$ at $0$ and union with it to $1.$) But such an arrow won't generally exist--in fact, $\neg a\le \neg b$ will only be true if $a=b$! You have a better bet of this functor category being a Heyting algebra, but perhaps that's enough to say for the moment.

John Baez (Jun 08 2023 at 23:04):

Yes, not only does $[\mathsf{D},\mathsf{C}]$ inherit all the limits and colimits that $\mathsf{C}$ has, it also inherits all the -ary covariant operations $\mathsf{C}$ has, obeying all the same equations. And the idea is the same: you compute these things "pointwise".

By an $n$-ary covariant operation I just mean a functor

$F: \mathsf{C}^n \to \mathsf{C}$

If you play around a bit you can see how this gives a functor

$\hat{F} : [\mathsf{D},\mathsf{C}]^n \to [\mathsf{D},\mathsf{C} ]$

John Baez (Jun 08 2023 at 23:08):

You're probably familiar with this in the case where $\mathsf{C}$ is the set of real numbers and $\mathsf{D} = \{1,2,3,\dots, k\}$ - both sets, which can be viewed as discrete categories. Then $[\mathsf{D},\mathsf{C}]$ is the set of k-tuples of real numbers. The real numbers have a binary operation called "addition", so we get a binary operation on k-tuples of real numbers, called "addition of vectors".

John Baez (Jun 08 2023 at 23:08):

But it all works in a vastly more general way.

John Baez (Jun 08 2023 at 23:10):

@Kevin Arlin pointed out the counterexample of negation. A boolean algebra is a special kind of category, "and" and "or" are binary covariant operations, but negation is not a unary covariant operation.

John Baez (Jun 08 2023 at 23:12):

The last statement is just a fancy way of saying that "P implies Q" does not imply "not(P) implies not(Q)". I suppose people who slip and act like it does are implicitly hoping that negation is a covariant functor. :upside_down:

Mike Shulman (Jun 09 2023 at 00:37):

Kevin Arlin said:

You have a better bet of this functor category being a Heyting algebra, but perhaps that's enough to say for the moment.

In case that isn't enough to say...

A Heyting algebra is a poset (with finite limits and colimits, I guess) that is a [[cartesian closed category]]. In logico-posetal terms this means there is an "implication" operation $X\Rightarrow Y$ such that $W \le X\Rightarrow Y$ if and only if $W\wedge X \le Y$. From this you can define a "negation" as $\neg X \equiv X \Rightarrow \bot$, where $\bot$ is the bottom element ("false"). But unlike in a Boolean algebra it won't satisfy $\neg\neg X = X$, so the "logic" you get is [[constructive logic]]. (Conversely, in a Boolean algebra you can define $X\Rightarrow Y \equiv \neg X \vee Y$ to get a Heyting algebra.)

In the case of a functor category, $[D,C]$ is cartesian closed as long as $D$ is small and $C$ is complete and cartesian closed. So, for instance, if $D$ is a small category like your $3$ and $C$ is a complete Boolean (or Heyting) algebra, then $[D,C]$ is a Heyting algebra. In this case the formula for the implication in $[D,C]$ becomes

$$(F\Rightarrow G)(d) = \bigwedge_{d\le d'} (F(d') \Rightarrow G(d')).$$

David Egolf (Jun 09 2023 at 01:39):

Thanks everyone! It will take me some time to carefully read and respond to your responses, but I appreciate them very much!

David Egolf (Jul 15 2023 at 18:29):

Unfortunately, my chronic fatigue has been giving me a hard time the last few weeks. So, it's been tough for me to make speedy progress on understanding this stuff. To encourage myself, I thought I'd share my progress so far!

My first order of business is to try and understand this:

Kevin Arlin said:

The operations of conjunction and disjunction in a Boolean algebra are examples of limits and colimits, respectively. If $\mathbf C$ is any category with (co)limits of some shape $J,$ then $[\mathbf D,\mathbf C]$ always has the same (co)limits computed pointwise. You might have seen an argument like this in a case of functors into a bigger category like $\mathbf{Set}.$

Specifically, I want to first understand the argument alluded to in the final sentence. I believe I found a good starting point in Proposition 8.7 of "Category Theory" by Steve Awodey. After changing the notation a bit, the first part of this proposition states:

For any locally small category $\mathsf{C}$, the functor category $[\mathsf{C^{op}}, \mathsf{Set}]$ is complete.

I believe the idea here is that the category of functors from $\mathsf{C}^{op}$ to $\mathsf{Set}$ inherits all small limits from $\mathsf{Set}$.

(The second part of Proposition 8.7 mentions the "evaluation functor", and so I spent an enjoyable time learning about that, the concept of "exponentials", and something very cool called the "bifunctor lemma". But I'm not sure that stuff is really needed to understand the proof of the first part of Proposition 8.7).

Now, let me try to understand the proof of the quoted proposition provided by Awodey. We want to show that $[\mathsf{C^{op}}, \mathsf{Set}]$ has every small limit, assuming $\mathsf{C}$ is locally small. To do this, we consider an arbitrary small diagram in $[\mathsf{C^{op}}, \mathsf{Set}]$, and try to show it has a limit. That, is we start by considering a functor $F: J \to [\mathsf{C^{op}}, \mathsf{Set}]$, where $J$ is a small category.

If the limit of $F$ exists, it corresponds to some object $L_F$ in $[\mathsf{C^{op}}, \mathsf{Set}]$, together with a bunch of morphisms from $L_F$ to the objects in the image of $F$. Note that $L_F$ is a functor $L_F: \mathsf{C^{op}} \to \mathsf{Set}$.

The Yoneda lemma tells us that $L_F(c) \cong \mathrm{Hom}(y(c), L_F)$, for any object $c$ in $\mathsf{C^{op}}$, where $y$ is the Yoneda embedding functor. This functor $y: C \to [\mathsf{C^{op}}, \mathsf{Set}]$ sends an object $c$ to the representable functor $\mathsf{Hom}_C(-,c): \mathsf{C^{op}} \to \mathsf{Set}$.

Next, the proof makes use of the fact that "representable functors preserve limits". Understanding a proof of that will probably be my next step! But I should stop for now, because I'm getting tired.

Chris Grossack (they/them) (Jul 15 2023 at 19:36):

Here's something that someone may have told you already, but it's really good intuition for what's going on here:

If $(\mathbb{R}, +, \times, 0, 1)$ is a ring, then for any set $X$ the functions $[X,\mathbb{R}] = \{ f : X \to \mathbb{R} \}$ is also a ring! Why? Because you can define the operations pointwise: $(f +_{[X,\mathbb{R}]} g)(x) = f(x) +_\mathbb{R} g(x)$, $0_{[X,\mathbb{R}]}(x) = 0_\mathbb{R}$, and so on.

Indeed, for any algebraic structure $\mathcal{A}$, the functions into $\mathcal{A}$ form an algebra of the same type, just by working pointwise in this way.

Now, one enlightening way to view limits/colimits/etc is as certain "algebraic" structure on a category -- in much the same way that a "ring" is structure on a set. And with this intuition, you might guess that functors $[X, \mathcal{C}]$ into a category $\mathcal{C}$ will have all the same "algebraic structure" (read: limits/colimits/etc) that $\mathcal{C}$ does. This intuition is true and the proof is exactly the same!

If $\mathcal{C}$ has products, then we can compute the product in $[X,\mathcal{C}]$ as $(F \times G)(X) = F(X) \times G(X)$. But now everything is a functor, so I also have to tell you what happens to the arrows. But it's the same thing! If $\alpha : X \to Y$ then $(F \times G)(\alpha) = F(\alpha) \times G(\alpha)$ works!

More generally, you can compute limits (and colimits) pointwise too:

$(\lim^{[X,\mathcal{C}]} F_i)(X) = \lim^\mathcal{C} (F_i X)$

Chris Grossack (they/them) (Jul 15 2023 at 19:38):

The correct way to make this precise is with the language of "2-monads" but you can go pretty far just taking it as intuition, and proving whatever special cases you need by hand ^_^

David Egolf (Jul 15 2023 at 20:04):

Thanks @Chris Grossack (they/them) ! Your explanation makes a lot of sense to me. Thinking of limits (or colimits) as specifying some kind of algebraic operation seems like quite a nice perspective.

I'll still want to work through the details of the proposition I discuss above, but having a big-picture explanation should be helpful!

Chris Grossack (they/them) (Jul 15 2023 at 20:07):

Absolutely! Take your time, and there's a ton of us here willing to help out whenever you get stuck ^_^

David Egolf (Jul 15 2023 at 20:39):

Reading over your comment again @Chris Grossack (they/them), I realize that I don't follow what you said about arrows in your example with products. You indicate that we can describe how $F \times G$ acts on an arrow $\alpha: X \to Y$ by setting $(F \times G)(\alpha) = F(\alpha) \times G(\alpha)$. Unfortunately, I don't know how to compute the right-hand side here, which is the product of two arrows $F(\alpha)$ and $G(\alpha)$!

I know how to compute a kind of product on two arrows with the same source, in a category with products. If $f: c \to a$ and $g: c \to b$, then we can set $f \times g$ as the unique morphism to $a \times b$ from $c$ specified by the universal property of products.

But $F(\alpha)$ and $G(\alpha)$ aren't in general going to have the same source object. So I'm not sure what kind of product you had in mind for computing $F(\alpha) \times G(\alpha)$! I'm guessing this might be a kind of product I'm not familiar with.

If you could elaborate on this, I'd appreciate it!

Edit: I think the answer by Randall here might explain this.

David Egolf (Jul 15 2023 at 20:55):

That is, if we have a morphism $f: X \to Y$ and a morphism $f': X' \to Y'$, we can form a morphism $f \times f': X \times X' \to Y \times Y'$ as follows. We first need to make a morphism from $X \times X'$ to $Y$, and a morphism from $X \times X'$ to $Y'$. The first of these can be acquired as $f \circ \pi_X$ and the second as $f' \circ \pi_{X'}$. Then we can use the universal property of products to get a morphism from $X \times X'$ to $Y \times Y'$, which is defined in terms of $f$ and $f'$.

This seems like it could be a good way to take the product of morphisms. Although, I'm not 100% sure this is what was meant above.

Chris Grossack (they/them) (Jul 15 2023 at 21:27):

@David Egolf
Of course!

If you have maps $\alpha : X \to X'$ and $\beta : Y \to Y'$, then we want a map $\alpha \times \beta : X \times Y \to X' \times Y'$. This says that the product operation itself is a functor from $\mathcal{C}^2 \to \mathcal{C}$. Informally, what should this arrow do?

The only reasonable choice is $(\alpha \times \beta)(x,y) = (\alpha x, \beta y)$, and so we would like to express this using arrows. (There's a notion of "internal logic" for certain categories that lets you use this kind of set theoretic manipulation rigorously, but let's not get into that here. For now we'll take it as a motivating example). Unsurprisingly, when we express this operation in terms of arrows we get exactly the arrow that you built! ^_^