I’ll rescind my last comment. It doesn’t look so out of place to me today.
]]>Daniel, while this is very nice and should be put somewhere on the nLab, here it is unfortunately out of place.
]]>Added template on countability properties.
]]>Ah, right. Anyway, cool! If you ever feel like adding that proof to the page, it would be great…
]]>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)
]]>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?
]]>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
]]>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.
]]>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.
]]>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.
]]>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.
]]>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.)
]]>