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: ✔ extensive categories in constructive mathematics

Nico Beck (Jul 26 2023 at 21:04):

Does somebody know a constructively usuable version of the definition of an extensive category, and of a connected object?

Context: I have a category $C$, and I want to assume that it is infinitarily extensive and that $\mathbf 1$ is connected. I want to show that this implies that each $p:\mathbf 1\to \bigsqcup_{x:A}X(x)$ must factor through exactly one of the inclusion maps $X(p_1)\to \bigsqcup_{x:A}$. That is I need sth along the lines of proposition 3.1 in this article but the problem is that my base category of sets does not have LEM and that the proof is constructively invalid.

The definition of an extensive category itself seems a bit questionable constructively (I don't have so much experience). I.e. the intersection of any two coproduct inclusions with non-equal indices is disjoints. Proofs often start with "let a,b be two indices, either they are equal or not" and that doesn't work anymore. Are there good alternatives?

(Remark. The category $C$ in question is actually the category of internal sets, and I have a constructive way to produce the index $p_1$. It is the composite of $p:\mathbf 1\to \bigsqcup_{x:A}X(x)$ with the map $\pi:\bigsqcup_{x:A}X(x)\to A$ whose $x:A$-component is the map which sends everything in $X(x)$ to $x$. )

Graham Manuell (Jul 26 2023 at 22:02):

I don't know if Proposition 3.1 is true constructively or not, but in general, I imagine the definition of extensivity that asks the canonical map $\prod_i C/X_i \to C/(\coprod_i X_i)$ to be an equivalence is the right one. The nlab gives 4 equivalent definitions of (infinitary) [[extensive category]] and all but the first one should still work constructively. Possibly there is even a way to phrase disjointness that makes sense constructively, but I don't know what it is.

Jacques Carette (Jul 26 2023 at 23:48):

This definition of extensive seems to work fine here is it in agda-categories. Definition 2.1 of [[connected+object]] should also work out fine constructively.

Mike Shulman (Jul 26 2023 at 23:49):

Yes, there's no problem with finitary extensive categories; the question is about the definition of infinitary extensive category.

Jacques Carette (Jul 26 2023 at 23:50):

Indeed - I read too quickly, I missed that part. Never mind then, sorry for the noise!

Mike Shulman (Jul 26 2023 at 23:52):

The constructive version of disjointness says that for any two indices $i,j$, the pullback of the two injections $X_i \to \coprod_k X_k$ and $X_j \to \coprod_k X_k$ is a coproduct of $i=j$ copies of $X_i$ (or, equivalently, of $X_j$). Here by $i=j$ I mean the [[subsingleton]] set corresponding to the proposition $i=j$. So classically, this set is either empty or a singleton, and those two cases respectively give you the two conditions that distinct injections have initial pullback (the initial object being the coproduct of zero copies of anything) and that each injection is monic (since a morphism is monic iff its pullback along itself is its domain, and the coproduct of 1 copy of any object is that object).

Mike Shulman (Jul 26 2023 at 23:53):

(Conveniently, this definition also makes clear why the two parts of the definition of "disjoint coproduct" naturally go together.)

Mike Shulman (Jul 26 2023 at 23:54):

However, while this constructive notion of disjointness fixes the first definition of infinitary extensive category, I don't think it does anything to rescue Prop. 3.1. I think constructively you just have to work with connectedness defined in terms of arbitrary coproducts.

Mike Shulman (Jul 26 2023 at 23:58):

I'm not entirely sure what you mean by "internal sets", but it is constructively true in the category of sets that 1 is connected in this sense.

Nico Beck (Jul 27 2023 at 13:52):

Mike Shulman said:

I'm not entirely sure what you mean by "internal sets", but it is constructively true in the category of sets that 1 is connected in this sense.

Thanks, I will try my luck with the coproduct over the equality type! I am actually using your stack semantics, so by internal set I mean sth in a fiber of the self indexing (or a splitting of the self indexing) of some base category.

Nico Beck (Jul 27 2023 at 13:55):

Graham Manuell said:

I don't know if Proposition 3.1 is true constructively or not, but in general, I imagine the definition of extensivity that asks the canonical map $\prod_i C/X_i \to C/(\coprod_i X_i)$ to be an equivalence is the right one. The nlab gives 4 equivalent definitions of (infinitary) [[extensive category]] and all but the first one should still work constructively. Possibly there is even a way to phrase disjointness that makes sense constructively, but I don't know what it is.

You are right, this version works of extensive categories works well! I should have thought about it a bit longer before asking a question. I wonder if this definition is constructively equivalent to "coproducts are preserved by pullbacks" + "intersections are disjoint" (in Mike Shulman's version above) :thinking:

Notification Bot (Jul 27 2023 at 14:09):

Nico Beck has marked this topic as resolved.

Mike Shulman (Jul 27 2023 at 14:44):

What is a "sth"? You've used it twice but that's not an English word I know.

John Baez (Jul 27 2023 at 14:47):

An abbreviation of "something", I guess. I imagine people who write a lot of text messages use this.

John Baez (Jul 27 2023 at 14:48):

Luckily I'm retired so I have a lot of spare time and can write whole words.

Mike Shulman (Jul 27 2023 at 14:52):

o i c

Mike Shulman (Jul 27 2023 at 14:54):

Nico Beck said:

I wonder if this definition is constructively equivalent to "coproducts are preserved by pullbacks" + "intersections are disjoint" (in Mike Shulman's version above)

I'm 99% sure it is, and 98% sure the same proof should work (with appropriate constructive modifications), but I don't have time to check it myself right now.