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: Category theory in a topos

Patrick Nicodemus (Nov 01 2023 at 17:28):

Let $E$ be a Boolean topos satisfying the internal axiom of choice.
This is a question about doing set theory internal to $E$. Not "$E$ as model of structural set theory" but closer to "models of set theory in $E$".
Actually the set theory I am interested in here is more material than structural, as I am interested in subsets of $A$ modelled as predicates $A\to\Omega$, so we have extensionality and so on.
Let $A$ be an object in $E$.

Patrick Nicodemus (Nov 01 2023 at 17:34):

There should, I think, be an internal category structure in $E$ where $\Omega^A$ is the object of objects. The arrows in this category are "functions between subsets of $A$". I am not talking about functions that respect the subset inclusion into A (which are unique if they exist) - the functions in this category can be arbitrary.
I have three different ideas for exactly what the object of arrows should be, which I'll discuss later.

The basic question is: Treating $\Omega^A$ as the objects of the "category of subsets of A", what assumptions can we impose on $A$ so that the subcategory of "small subsets of $A$" (for a suitable definition of "small") has the good properties we want of a category of sets? For example, finite products, finite coproducts, exponentials, limits and colimits indexed by a map $B\to \Omega^A$ for a "small" object $B$, and so on.

Even without "smallness" assumptions, I would expect that if $A$ is infinite in the appropriate sense then $\Omega^A$ has finite products and coproducts, as $A+A$ and $A\times A$ should admit an embedding into $A$. What definitions of "infinite" work here?

Patrick Nicodemus (Nov 01 2023 at 17:36):

My motivations here are practical.
My question is really about the theorem prover Isabelle/HOL, whose logic is very close to that of a Boolean topos satisfying the internal axiom of choice. I want to develop category theory in Isabelle/HOL.
This analogy is not perfect. The most important distinction I have noticed is that the "subobject classifier" in Isabelle actually gives something strictly weaker: for every predicate $\phi : A \to \mathsf{bool}$ such that $\exists x.\phi(x)$, there is a subobject of $A$ classified by $\phi$; but it is essential that the predicate be true for at least one element. This category has no initial object and every object is equipped with a canonical map from the terminal object. Still, for practical purposes it appears one can get away with the constantly-false predicate on an object every time one appears to need the initial object, and so there is no real harm done. It would be a valuable contribution of the categorical logic community if anyone wants to work out what exactly the internal logic of such a category is and how it relates to topos theory, or prove an equivalence between fragments of logic, as this is actually a real world logic that literally thousands of people use! It's very important!

Patrick Nicodemus (Nov 01 2023 at 17:37):

The fact that this is a "real world problem" (I want to actually prove theorems in this logic) is relevant here because it biases me away from verbose solutions to problems which will become unwieldy later on even if they're more categorically elegant.

In the definition of the morphisms of $\Omega^A$, the one could do this with functions as relations on $A$, i.e. if $X,Y\subset A$ then $R\subset A\times A$ is a function from $X\to Y$ if $\forall x y. (\lnot R x y \lor (x\in X\land y \in Y))$ and $\forall x\in X.\exists y\in Y. R x y$. My instinct is that relations instead of functions would get pretty unwieldy in actually proving theorems in this logic (I want to use terms to denote values) and so I want to work with a subset of $A^A$. There are two relevant definitions that jump out at me here:

Patrick Nicodemus (Nov 01 2023 at 17:40):

• $A$ is assumed to be equipped with a distinguished morphism $c : 1\to A$. For subsets $X,Y$ of $A$, we define $Y^X$ to be the subset of $A^A$ consisting of all those $f$ such that $f(x)\in y$ for $x\in X$ and $f(x)=c$ for $x\notin X$. This is easier in the sense that it avoids quotienting.
• Take the subset of $A^A$ with $f(x)\in Y$ for all $x\in X$ and quotient out this object by the relation $f\sim f'$ if $f(x)=f'(x)$ for all $x\in X$.

Patrick Nicodemus (Nov 01 2023 at 17:47):

Perhaps all these definitions are isomorphic when $A$ is inhabited, I have not thought through that yet.

In conclusion I propose three basic definitions of the "internal category of subsets of $A$ and arbitrary functions between them" and ask, for whichever choice of definition you care to investigate, what do we need to assume about $A$ in order to do mathematics?

• under what assumptions on $A$ does this internal category have finite products, equalizers, coproducts, coequalizers and so on?
• under what assumptions of $A$, and for what definition of "small", does this internal category have small limits of small sets, small colimits of small sets and so on?
• under what assumptions on $A$, and possibly the topos $E$ in general, does this category of $A$-sets admit the construction of free monoids, free groups and other algebraic structures? Can we get an internal category of $A$-monoids which is monadic over the category of subsets of $A$?

Reid Barton (Nov 01 2023 at 18:04):

Since $E$ is Boolean and satisfies choice, via the internal language of $E$, we can turn these questions back into questions about ordinary classical set theory, right?

Reid Barton (Nov 01 2023 at 18:05):

The question is about the category of all sets that are (isomorphic to) subsets of some fixed set $A$.

Reid Barton (Nov 01 2023 at 18:06):

Then the answers would be (0) these definitions of the morphisms are equivalent, (1) this category has finite (co)limits as soon as $A$ is infinite, (2) the category will be closed under small colimits but not under small limits, (3) again as soon as $A$ is infinite (or in general, big enough compared to the size of the algebraic theory)

Reid Barton (Nov 01 2023 at 18:07):

About 2: the category will not have a product of $A$ copies of an object with two elements, by Cantor ($2^A > A$).

Reid Barton (Nov 01 2023 at 18:07):

Usually the good way to build a "category of sets" in classical mathematics is to fix a universe--let's say $A$--of "classes", and make the objects be subsets of $A$ of cardinality smaller than $A$.

Reid Barton (Nov 01 2023 at 18:08):

Then, good cardinal features of $A$ will translate into good features of the resulting category of sets.

Patrick Nicodemus (Nov 01 2023 at 18:09):

Yes, that all makes sense. In that case I will need to formalize a little bit of cardinal arithmetic and/or import some additional libraries.

Patrick Nicodemus (Nov 01 2023 at 18:12):

I was hoping for a little more of a lightweight solution but it is certainly the most robust.