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: deprecated: topos theory

Topic: Finite objects

Morgan Rogers (he/him) (May 10 2020 at 17:08):

There are a few notions of internal finiteness in a topos (or indeed in a more general category). The most widespread seems to be Kuratowski-finiteness (K-finiteness from here on). Here's a problem I'm wrestling with.
In Sketches of an Elephant, Johnstone often argues that conditions involving finite limits or colimits are elementary, so make sense anywhere; it's only once we pass to "infinite" limits or colimits that we need to worry about indexing (indexed categories, indexed adjoints, indexed completeness...) In particular, inverse image functors of geometric morphisms are required to preserve finite limits in this elementary sense.
However, in a typical topos $\mathcal{E}$ there are "non-trivial" finite objects: objects which aren't just finite coproducts of copies of the terminal object, and hence there can be more finite internal categories which can serve to index diagrams and hence limits. What I mean by this is that, taking this topos as a base, by 'pulling back' (applying inverse image functors) these finite categories in $\mathcal{E}$ can be used to index internal diagrams in toposes over $\mathcal{E}$. If I have a geometric morphism over $\mathcal{E}$, is it really the case that the inverse image preserving finite limits in the elementary sense ensures that these internal limits are preserved?

Morgan Rogers (he/him) (May 10 2020 at 17:19):

As a contrasting case, a geometric morphism $p: \mathcal{F} -> \mathcal{E}$ is tidy if the direct image of its slice over any object of $\mathcal{E}$ preserves internal filtered colimits. This is definitely not the same as these direct images just preserving filtered colimits in general; in fact it is much weaker, because it seems we can construct geometric morphisms which do that but fail to even be proper (so that the sliced geometric morphisms preserve $\mathcal{E}$-indexed filtered colimits of subterminal objects). Yet the definition of filtered colimit is almost as elementary as the definition of finiteness!
It's possible my supposed example is wrong (I can describe it properly if anyone is dubious), but what I really want to know is: how far removed can internal finiteness be from external/"elementary" finiteness?

sarahzrf (May 10 2020 at 17:43):

it's interesting that you'd say that k-finiteness is the most widespread given that bishop-finiteness is the most common thing i see "finite" meaning when working internally to constructive math :o

sarahzrf (May 10 2020 at 17:46):

also, i'm not very well-equipped to answer your question in general, but i do wanna ask: what kind of constraints do you have in mind as to what sort topos you have? are you thinking only of grothendieck topoi here, say?

Reid Barton (May 10 2020 at 18:21):

I think it is true that K-finiteness is what is traditionally meant by "finite" and my sense is that it's a historical accident, probably related to, in commutative algebra, "finitely generated module" coming prior to "finitely presented module" (it being a more obvious notion if you phrase it in terms of elements, and good enough if you only work with Noetherian rings, and a lot of rings of interest are Noetherian).

Reid Barton (May 10 2020 at 18:22):

I'm sure that "finite (co)product" internally ought to be interpreted as finite in the Bishop sense, though.

Reid Barton (May 10 2020 at 18:23):

Otherwise you cannot reduce them to binary and nullary ones, I think.

Reid Barton (May 10 2020 at 18:23):

just as an example

sarahzrf (May 10 2020 at 18:34):

hmm, i dont know about tradition :shrug: off the top of my head, the nlab page https://ncatlab.org/nlab/show/finite+set defines plain "finite" as bishop-finite, and the coq stdpp library defines Finite like this

Class Finite A `{EqDecision A} := {
  enum : list A;
  (* [NoDup] makes it easy to define the cardinality of the type. *)
  NoDup_enum : NoDup enum;
  elem_of_enum x : x ∈ enum
}.

sarahzrf (May 10 2020 at 18:35):

(which is equivalent to bishop-finite)

Morgan Rogers (he/him) (May 11 2020 at 08:40):

Sorry for not replying yesterday (now I'll have to wait for you both to come online again oops)
sarahzrf said:

it's interesting that you'd say that k-finiteness is the most widespread given that bishop-finiteness is the most common thing i see "finite" meaning when working internally to constructive math :o

Similarly interesting that there are separate nLab pages for finite object and finite set and Bishop's name doesn't feature in the former, although the concept of Bishop-finiteness does. For me personally, the definition as the internal version of "is in bijection with $[n]$" feels too restrictive, but that's a vague argument.
An alternative is that K-finiteness coincides with internal compactness: from Proposition 3.4 on the finite object page, an object $X$ in $\mathcal{T}$ is K-finite iff $\mathcal{T}/X \to \mathcal{T}$ is a proper geometric morphism (so $\mathcal{T}/X \to \mathcal{T}$ is compact as a topos over $\mathcal{T}$). But this is only not circular because there is an equivalent characterisation of proper geometric morphisms in terms of Beck-Chevalley conditions.

Morgan Rogers (he/him) (May 11 2020 at 08:42):

sarahzrf said:

also, i'm not very well-equipped to answer your question in general, but i do wanna ask: what kind of constraints do you have in mind as to what sort topos you have? are you thinking only of grothendieck topoi here, say?

I'm actually curious about whether that matters. Is "finite limit/colimit" a consistent internal/external concept in Grothendieck toposes but not some other toposes?

Reid Barton (May 11 2020 at 12:42):

Morgan Rogers said:

An alternative is that K-finiteness coincides with internal compactness: from Proposition 3.4 on the finite object page, an object $X$ in $\mathcal{T}$ is K-finite iff $\mathcal{T}/X \to \mathcal{T}$ is a proper geometric morphism (so $\mathcal{T}/X \to \mathcal{T}$ is compact as a topos over $\mathcal{T}$).

At proper geometric morphism there's an expanded version of the statement which includes the addendum: $\mathcal{T}/X \to \mathcal{T}$ is tidy (i.e., $\mathcal{T}/X$ is strongly compact as a topos over $\mathcal{T}$) if and only if $X$ is also decidable (i.e., Bishop finite).

Morgan Rogers (he/him) (May 11 2020 at 13:10):

That's really nice, I hadn't spotted that :big_smile: I have since spotted this, though:

If filtered category means admitting cocones of every Bishop-finite diagram, then a set is Bishop-finite iff it is a finitely presented object in Set and it is Kuratowski-finite iff it is a finitely generated object in Set,

which partially answers my question about the kind of filteredness that's used in the definition of proper/tidy morphisms. The main question remains, though... do both kinds of internal finiteness in $\mathcal{E}$ gives limits which inverse images of geometric morphisms (over $\mathcal{E}$, say, so that indexing over them makes sense) respect?

Reid Barton (May 11 2020 at 13:48):

My hunch is that you need B-finiteness, though that is based on very little. It's possible that K-finiteness is enough: for instance, perhaps every K-finite diagram has a cofinal functor from a B-finite diagram?

sarahzrf (May 11 2020 at 14:02):

Morgan Rogers said:

sarahzrf said:

also, i'm not very well-equipped to answer your question in general, but i do wanna ask: what kind of constraints do you have in mind as to what sort topos you have? are you thinking only of grothendieck topoi here, say?

I'm actually curious about whether that matters. Is "finite limit/colimit" a consistent internal/external concept in Grothendieck toposes but not some other toposes?

well, for example, not every elementary topos has an nno (FinSet doesn't!)

sarahzrf (May 11 2020 at 14:02):

so i'm not sure you can even define finiteness in a plain elementary topos, in which case grothendieck topos mightve been a reasonable assumption to make about your question

sarahzrf (May 11 2020 at 14:03):

but if you didn't mean that, then...? just also an nno, or what

sarahzrf (May 11 2020 at 14:04):

also, re "An alternative is that K-finiteness coincides with internal compactness"—perhaps, but "finite" sounds stronger to me than "compact"—although maybe that's just circular, since i'm used to thinking of "finite" as meaning b-finite :)

Morgan Rogers (he/him) (May 11 2020 at 14:06):

sarahzrf said:

Morgan Rogers said:

sarahzrf said:

also, i'm not very well-equipped to answer your question in general, but i do wanna ask: what kind of constraints do you have in mind as to what sort topos you have? are you thinking only of grothendieck topoi here, say?

I'm actually curious about whether that matters. Is "finite limit/colimit" a consistent internal/external concept in Grothendieck toposes but not some other toposes?

well, for example, not every elementary topos has an nno (FinSet doesn't!)

There's an equivalent characterisation on the finite set page which uses power objects rather than a nno, so that works in any topos :shrug:

sarahzrf (May 11 2020 at 14:06):

oh really :eyes:

Morgan Rogers (he/him) (May 11 2020 at 14:07):

(although it is a bit worse to work with, so I'm happy to assume the presence of a natural number object if it would simplify things)

sarahzrf (May 11 2020 at 14:07):

oops!

sarahzrf (May 11 2020 at 14:07):

in my defense, it's very impredicative :>

sarahzrf (May 11 2020 at 14:09):

yeah ok maybe i shouldn't've butted in on this issue :zip_it:

Morgan Rogers (he/him) (May 11 2020 at 14:10):

To be clear, I'm not looking for a "right" definition of finiteness; I'm happy to be presented with a bouquet of them. :bouquet: I just want to figure out how internal and external/elementary concepts of finiteness relate to one another.

sarahzrf (May 11 2020 at 14:11):

its a goddamn mess is how

sarahzrf (May 11 2020 at 14:11):

is what i can only assume.

sarahzrf (May 11 2020 at 14:11):

given that all subsingletons are subfinite

Mike Shulman (May 12 2020 at 15:50):

In constructive mathematics, Bishop-finiteness is almost always what you want to mean by unadorned "finite". However, note that when interpreted in a topos this refers to internal Bishop-finiteness, which is more general than the "external" sense (the latter is I believe what the Elephant calls a "finite cardinal"). In some cases the distinction doesn't matter, but when it does it's almost always B-finiteness that you want.

Mike Shulman (May 12 2020 at 15:51):

As for the original question, I believe the answer is yes, because you can prove both internally and externally that preserving "finite limits" is equivalent to preserving pullbacks and the terminal object, hence both kinds of preservation are equivalent to each other.

sarahzrf (May 12 2020 at 15:52):

by 'the "external" sense', do you mean something which is an external b-finite coproduct of 1s?

Mike Shulman (May 12 2020 at 15:54):

I mean something that is a classified by a global element of the NNO (what the Elephant calls a "finite cardinal").

sarahzrf (May 12 2020 at 16:03):

ah, so that's actually weaker than what i said, right?

Morgan Rogers (he/him) (May 12 2020 at 16:05):

Mike Shulman said:

As for the original question, I believe the answer is yes, because you can prove both internally and externally that preserving "finite limits" is equivalent to preserving pullbacks and the terminal object, hence both kinds of preservation are equivalent to each other.

That would be a relief, I hope you're right. I need to finish having a good read of section D5.2 in the Elephant before I come back with questions; I didn't realise when I first posted this how nuanced finiteness would be.

Mike Shulman (May 12 2020 at 16:08):

sarahzrf said:

ah, so that's actually weaker than what i said, right?

Yes. For instance, in $\mathrm{Set}\times\mathrm{Set}$, $(2,3)$ is a finite cardinal, but not an externally-finitely-indexed coproduct of copies of 1.

Reid Barton (May 22 2020 at 23:35):

I realize I was too hasty earlier in suggesting that products over B-finite sets could be reduced to terminal objects and binary products. After seeing https://github.com/b-mehta/topos/issues/22, I've realized there's a problem with trying to apply the usual construction, because you have to pick an order to build the product in and different orders may produce different (though of course isomorphic) objects. It seems the best that you can conclude is that there is a "weakly contractible" category of products, or that there is a product anafunctor.

Reid Barton (May 22 2020 at 23:38):

In section A.1.2 of the Elephant (which claims to work without choice by default) there is the usual list of equivalent formulations of "the category C has finite limits", but the proof is simply "See any good textbook on category theory" and there is no discussion about what "finite" might mean.

Reid Barton (May 22 2020 at 23:41):

Despite the fact that the very next paragraph is careful to explain that "C has such-and-such limits" is intended to mean that one has selected a limit for each diagram of the kind in question, so as to avoid requiring choice to construct a family of limits.

Reid Barton (May 22 2020 at 23:56):

In HoTT and using univalent categories I think you could fix this, although I don't see this construction in UniMath.

Mike Shulman (May 24 2020 at 00:46):

Ah, a good point. Yes, univalence should solve that problem nicely, but I think you're right that in a constructive set-theoretic metatheory you'll only get a product anafunctor. Perhaps by "finite" Johnstone intended to mean a set equipped with a bijection to $\{1,\dots,n\}$, i.e. an ordering?

Reid Barton (May 25 2020 at 13:49):

I guess it must be. I tried reading the next few sections but I didn't come across any case where this distinction would matter.

Dan Doel (May 26 2020 at 04:49):

@Reid Barton https://hub.darcs.net/dolio/agda-share/browse/cubical/GroupoidProduct.agda

Dan Doel (May 26 2020 at 04:56):

Technically that isn't the product definition part, just the part that fixes the issue (I think). But I think the premises there are reasonable expectations of how you construct finite products from binary products and a terminal object.

Reid Barton (May 26 2020 at 12:11):

I see, right. I was imagining some higher-level argument along the lines of "univalent categories see weak equivalences of categories as equivalences", applied to {sets equipped with a bijection to some fin n} -> {sets which merely admit a bijection to some fin n}, but I don't know if that really works.

Dan Doel (May 26 2020 at 13:29):

Perhaps it does, but it is a lot more work to develop all that. :slight_smile:

Dan Doel (May 26 2020 at 13:30):

It was already difficult to figure out what I did do.

Paolo Capriotti (May 26 2020 at 14:22):

Reid Barton said:

I see, right. I was imagining some higher-level argument along the lines of "univalent categories see weak equivalences of categories as equivalences", applied to {sets equipped with a bijection to some fin n} -> {sets which merely admit a bijection to some fin n}, but I don't know if that really works.

Maybe I misunderstand what you mean, but {sets equipped with a bijection to some fin n} is not a univalent category.

Reid Barton (May 26 2020 at 14:23):

Right, I'm thinking of univalent categories as some kind of local objects in all categories.

Paolo Capriotti (May 26 2020 at 14:24):

Ah, I see, you're saying that it induces an equivalence of the exponentials.