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: predicative finiteness

Jem (May 11 2020 at 15:53):

I don't think we need impredicativity or a NNO to define what a finite sobject is. Couldn't we say that $X$ is finite iff it has decidable equality,
(i) there exists a (necessarily unique) least map $f:(X \to 2) \to 2$ (under the pointwise ordering) satisfying the property that $f(\lambda x. 0) = 1$ and for any $a$ in $X$ and $m$ with $f(m) = 1$ , we have $f(m \lor (=a)) = 1$ and
(ii) this $f$ also satisfies $f(\lambda x.1) = 1$ ?

Jem (May 11 2020 at 15:53):

This says the same as the impredicative finitary definition given on the nlab (give or take), but doesn't need power set (as $X$ has decidable equality), and has the existence of 'the collection of finite subobjects' as a requirement as part of the definition, as opposed to something which we know exists already.

Jem (May 11 2020 at 15:54):

Not sure how this could be extended to subfiniteness or k-finiteness, though.

sarahzrf (May 11 2020 at 15:56):

what exactly does f do here?

Jem (May 11 2020 at 15:58):

Characterises the finite decidable subsets - for $m$ the characteristic map of a decidable subset, we should have $f(m)$ iff $m$ is a finite subset.

sarahzrf (May 11 2020 at 15:59):

hmm...

Reid Barton (May 11 2020 at 15:59):

It seems like you would get K-finiteness just by dropping the hypothesis of decidable equality, right?

sarahzrf (May 11 2020 at 16:01):

well, you have no way of stating this w/o either impredicativity or deceq

Jem (May 11 2020 at 16:01):

No, because you can't gaurantee that $m \lor (=a)$ is then a decidable subset.

Reid Barton (May 11 2020 at 16:01):

Why do you need to use $2$ ?

sarahzrf (May 11 2020 at 16:01):

because having a subobject classifier is impredicative

sarahzrf (May 11 2020 at 16:02):

(so this is not directly relevant to topoi, of course—but maybe to finiteness in other kinds of categories)

Reid Barton (May 11 2020 at 16:02):

oh, I don't know about these silly things :upside_down:

sarahzrf (May 11 2020 at 16:04):

@Jem hmm, i think

youd want least rather than minimal
youd want it to be least satisfying condition (i), and then condition (ii) holds of it to make the whole object finite

Jem (May 11 2020 at 16:05):

Yeah, that's what I meant to mean. >.<

Dan Doel (May 11 2020 at 17:21):

If you can define B-finite, then you can define the others in terms of B-finite sets, can't you? K-finite is 'admits a surjection from a B-finite set'.

Jem (May 11 2020 at 17:22):

Yes, that works if you have quantification over types or an enumeration of B-finite sets.

Jem (May 11 2020 at 17:23):

I don't think we have either of those in the internal logic of an arbitrary topos (or LCCC) though, do we?

Morgan Rogers (he/him) (May 11 2020 at 17:23):

Huh? Why do you need those?

Jem (May 11 2020 at 17:24):

Well presumably you'd formalise "admits a surjection from a B-finite set" as "there exists a B-finite set and a surjection from that B-finite set", and in order to state that you'd need one of those.

Dan Doel (May 11 2020 at 17:24):

You'd need it to internalize the notion of (e.g.) K-finite, but not to exhibit that any particular thing is K-finite.

Jem (May 11 2020 at 17:24):

Yeah.

zigzag (May 11 2020 at 17:37):

@Jem But if I take $X$ to be a non-trivial subobject of $1$ , wouldn't that be finite according to your definition ?

Jem (May 11 2020 at 18:29):

I don't see why it would be (as we would need it to be inhabited to actually adjoin an element) but also don't see why it wouldn't be (the idea I had sketched fell through on closer inspection). What did you have in mind?

Jem (May 11 2020 at 18:29):

The definition can be amended by adding "any decidable subset of $X$ is empty or inhabited" to exclude cases like that.

Jem (May 11 2020 at 18:30):

So hopefully that would fix it.

Morgan Rogers (he/him) (May 11 2020 at 18:31):

Not to be dismissive, but I'm happy to work impredicatively/with power objects if it simplifies things enough to get to an answer to what I was asking about :sweat_smile:

Jem (May 11 2020 at 19:08):

Split the topic off so both can be talked about without interfering with each other

zigzag (May 11 2020 at 20:21):

mmm roughly, if you reason internally to some weak set theory, suppose that you have $A \subseteq \{*\}$ and you want to show it is finite using $\lambda p. 1$ as witness (it trivally satisfies the closure property of i) and ii)). So you want to show that any $f$ such that $f(\emptyset) = 1$ and with $f(p) = 1 \Rightarrow f(p \cup \{a\}) = 1$ is in fact constanty $1$ .

To this end, assume you are given some $p : A \to 2$ . If $f(p) = 1$ we are fine, otherwise $f(p) = 0$ . In that case, I would claim that $A$ is empty, because, if you suppose that you are given the $* \in A$ you can show that you have only two $p : A \to 2$ with $f(p) = 1$ because of the closure properties. But if $A$ was empty, then $p = \lambda x. 0$ and, by your first closure property, $f(p) = 1$ , which is a contradiction.

I don't know about the fix, but I would remain very cautious until I see a proof that it coincides with the usual notion. Finiteness is a tricky topic :)

Jem (May 11 2020 at 20:36):

Oh, no, it's meant to be "there is a least f satisfying (i), and this least f also satisfies (ii)", not "there is a least f satisfying both (i) and (ii)".
sarahzrf pointed out earlier that I'd been unclear in that regard, but I didn't edit the post to clarify it then. I'll do that now.

zigzag (May 11 2020 at 20:46):

ah, sorry, I misread your post; the $f$ I considered in that argument only satisfied i) as I can currently read it (i.e., $f(\emptyset) = 1$ and $f(p \cup \{x\}) = 1$ if $f(p) = 1$ (for $p$ decidable ofc)). Let me also edit my post so that everyone gets confused afterwards (hopefully it should not be the case :))