Want to take part in these discussions? Sign in if you have an account, or apply for one below
Vanilla 1.1.10 is a product of Lussumo. More Information: Documentation, Community Support.
I have started an article countable chain condition. So far most of the discussion is about topological spaces. (Additional small recent edits at separable space and metric space.)
That’s a lot of info!
I wonder what the “right” constructive version of this condition is. The notion of antichain doesn’t seem very constructive as-is.
These and other nLab things I’ve started are notes made on the side as I dip occasionally in Kunen’s set theory book, which I took with me on a recent vacation, thinking that I might try once and for all to do a sympathetic reading of consistency results as written by ZF-ists (more or less). Their style is somewhat alien to me.
I didn’t try to think too hard about constructive versions, but I agree this would be nice to know. Maybe Toby has thought some about this.
The more general case of the -cc for regular is what is mostly used, and to preserve power sets on taking sheaves. Since the notion of regular cardinal is a bit difficult without AC, I expect for the constructive definition of ccc one really wants a statement that would usually be a theorem in classical maths.
More generally, I believe there should be a relative form of this. Given a fibration of sites a la Moerdijk, there should be a relative -cc, corresponding to the case when the (inverse image part of the) induced geometric morphism preserves the appropriate power objects.
Sorry, I’m being a bit slow. Here’s a nice perspective on ccc (and -cc) that I came up with a little while ago. The exact statement may have to be fine tuned, but it was something like: a poset satisfies the ccc (resp. -cc) if (and only if?) sieves (on ? possibly for all objects) for the double-negation topology can be refined by sieves generated by no more that -many maps (resp. -many). Equivalently, I think, there is an equivalent site equipped with merely a coverage such that all covering families have size bounded by (). A set theorist put it to me once as: there’s not much difference between an maximal antichain and a dense subset, the latter obviously
I’m not sure if this is best phrased (in the general case) as: the (indexing set of the) family of maps in such a covering family is a subquotient of . This plays well with the situation with sheaves as I mentioned above, and has clear extensions to arbitrary sites, not just
Wow, neat! I can sort of vaguely see how that might work, but it would be nice to have it written out. Does that mean that the -topology is an “-ary site” as here?
Maybe just a weakly -ary site, for a poset satisfying -cc, and here is the minimum possible. The prelimit stuff might be related to what is called being -directed (or poss the related -closed). Note one can get off-by-one errors here (as in, these are ordinals, so there’s a version)
Ah, right. Anyway, cool! If you ever feel like adding that proof to the page, it would be great…
Daniel, while this is very nice and should be put somewhere on the nLab, here it is unfortunately out of place.
I’ll rescind my last comment. It doesn’t look so out of place to me today.
1 to 12 of 12