Not signed in

Want to take part in these discussions? Sign in if you have an account, or apply for one below

• Forgot your password?
• Apply for membership

1. • CommentRowNumber1.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 12th 2012
   • (edited Oct 12th 2012)
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexI am wondering, if we are working in Choice-free foundations, about the bifurcation of the sorts of finite (co)limits we can have. To save typing, I will only consider limits, and also because they seem to be what I need to think about for what I'm working on. We have the standard result in usual foundations that terminal object, binary products and equalisers implies all finite limits, but in the case where we have the existence of non-finite D-finite sets, do we still get this? In particular, might it be the case that really we would like the existence of the smaller class $tbe$ of limits generated by terminal object, binary products and equalisers? For the sort of simple reasoning I'm envisaging, these are certainly all I'd want. It seems to be only theorems do we usually get given an arbitrary finite diagram of which we need to take the limit. But could these really be referring to $tbe$-limits? (Hammering the point, I know, but I'm genuinely curious.) Of course, I've probably just hidden the non-finite, D-finite sets in the definition of 'generated', but can we adjust that definition so it is something along the lines of 'generated by a finite sequence involving $t$, $b$ and $e$, which is in bijection with a standard numeral'?

   I am wondering, if we are working in Choice-free foundations, about the bifurcation of the sorts of finite (co)limits we can have. To save typing, I will only consider limits, and also because they seem to be what I need to think about for what I’m working on.

   We have the standard result in usual foundations that terminal object, binary products and equalisers implies all finite limits, but in the case where we have the existence of non-finite D-finite sets, do we still get this? In particular, might it be the case that really we would like the existence of the smaller class $tbe$ of limits generated by terminal object, binary products and equalisers? For the sort of simple reasoning I’m envisaging, these are certainly all I’d want. It seems to be only theorems do we usually get given an arbitrary finite diagram of which we need to take the limit. But could these really be referring to $tbe$-limits? (Hammering the point, I know, but I’m genuinely curious.) Of course, I’ve probably just hidden the non-finite, D-finite sets in the definition of ’generated’, but can we adjust that definition so it is something along the lines of ’generated by a finite sequence involving $t$, $b$ and $e$, which is in bijection with a standard numeral’?

2. • CommentRowNumber2.
   • CommentAuthorMike Shulman
   • CommentTimeOct 12th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexI don't see anything that goes wrong with the usual proof that any finite limit is constructible from nullary and binary products and equalizers. Are you asking whether you can also construct non-finite D-finite limits? That seems doubtful to me.

   I don’t see anything that goes wrong with the usual proof that any finite limit is constructible from nullary and binary products and equalizers. Are you asking whether you can also construct non-finite D-finite limits? That seems doubtful to me.

3. • CommentRowNumber3.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 12th 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexThat's pretty much it. If I have a diagram $S\to C$ where $S$ is non-finite D-finite, I suppose we need to take a non-finite D-finite product in constructing its limit, and I have a hard time imagining that in terms of binary products, as I tend to think of an iterated product described thus as a rooted binary tree.

   That’s pretty much it. If I have a diagram $S\to C$ where $S$ is non-finite D-finite, I suppose we need to take a non-finite D-finite product in constructing its limit, and I have a hard time imagining that in terms of binary products, as I tend to think of an iterated product described thus as a rooted binary tree.

4. • CommentRowNumber4.
   • CommentAuthorMike Shulman
   • CommentTimeOct 12th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexSince finite sets are, by definition, the sets you can obtain by starting with nothing and repeatedly taking a binary coproduct with a singleton, you aren't going to be able to get to any non-finite set that way, regardless of whether it is D-finite. (-:

   Since finite sets are, by definition, the sets you can obtain by starting with nothing and repeatedly taking a binary coproduct with a singleton, you aren’t going to be able to get to any non-finite set that way, regardless of whether it is D-finite. (-:

5. • CommentRowNumber5.
   • CommentAuthorDavidRoberts
   • CommentTimeOct 12th 2012
   • PermaLink
   Author: DavidRoberts
   Format: MarkdownItexAh, so the word finite in the result really does mean the strongest sort of finite in the absence of Choice. That's what is was worried about. I've been thinking about toposes internal to toposes - specifically models of ZF - and the requirement for finite limits got me mildly worried. Because really I suppose we would ask for the existence of tbe limits.

   Ah, so the word finite in the result really does mean the strongest sort of finite in the absence of Choice. That’s what is was worried about. I’ve been thinking about toposes internal to toposes - specifically models of ZF - and the requirement for finite limits got me mildly worried. Because really I suppose we would ask for the existence of tbe limits.

6. • CommentRowNumber6.
   • CommentAuthorMike Shulman
   • CommentTimeOct 13th 2012
   • PermaLink
   Author: Mike Shulman
   Format: MarkdownItexThere are of course all sorts of [different notions of finiteness](http://ncatlab.org/nlab/show/finite+set#Constructivist) in constructive mathematics, but the unadorned word "finite" is usually used to mean the strongest one.

   There are of course all sorts of different notions of finiteness in constructive mathematics, but the unadorned word “finite” is usually used to mean the strongest one.