Timeline for Axiom of Replacement in Category Theory
Current License: CC BY-SA 2.5
11 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 23 at 12:09 | comment | added | David Roberts♦ | A correction to my last comment: BD can be proved using just the existence of iterated power sets $P^\alpha(\mathbb{N})$ for all countable ordinals $\aleph$, which in ZF(C) are constructed using instances of Replacement where the function has domain $\aleph$. | |
| Jun 1, 2020 at 13:02 | comment | added | David Roberts♦ | That piece of 'core maths' might have been Borel Determinacy (en.wikipedia.org/wiki/Borel_determinacy_theorem), which is known to require Replacement to prove. However, this type of descriptive set theory via games has always felt still very set-theoretic to me. | |
| Oct 14, 2010 at 16:52 | vote | accept | arsmath | ||
| Oct 6, 2010 at 3:43 | comment | added | Peter LeFanu Lumsdaine | That’s true — talking about functors between large categories forces us to deal with what set-theorists would call function-classes. But maybe this means we should call them “functor-classes”, or “large functors”? I like the definition you suggest, though I'd perhaps suggest different terminology: instead of using diagram vs. functor to make the distinction, maybe say “small diagram/functor” (well-behaved) vs. “diagram-class/functor-class with small domain” (not well-behaved without replacement)? | |
| Oct 6, 2010 at 2:19 | comment | added | Carl Mummert | @Peter: Certainly the identity functor is a functor from Set to Set, even though its domain and range are proper classes rather than sets, and so it is not a function in the ordinary set-theoretic sense. The issue is more tricky for the functors that produce small diagrams: they could be formalized as functions, or just as definable relations, depending on taste. Define a functor to be "small" if it is represented by a a function in the usual set-theoretic sense. Then if we do not assume replacement, it may be that not every small diagram is given by a small functor. | |
| Oct 6, 2010 at 2:10 | comment | added | Peter LeFanu Lumsdaine | oh, and (sorry for so many comments) yep, Borel determinacy is certainly a place where it’s needed, but is that really considered analysis? More significantly, is it used by analysts? I'd always thought of it as being descriptive set theory, and have heard it talked about by set theorists much more than by anyone else. But IANAA. | |
| Oct 6, 2010 at 1:42 | comment | added | Peter LeFanu Lumsdaine | (cont’d) As you say, though, replacement is generally assumed, implicitly or explicitly — ZFC, however we feel about it, is still pretty much the “industry standard” foundation. So most authors, I think, wouldn’t consider there to be a significant difference between the two definitions. | |
| Oct 6, 2010 at 1:33 | comment | added | Peter LeFanu Lumsdaine | At least some people do! I'm not sure which Wikipedia article(s) you're looking at, but I find “diagram” defined in terms of “functor”, in turn defined in terms of “function”, and the first definition of function given is: “One precise definition of a function is that it consists of an ordered triple of sets, which may be written as (X, Y, F). X is the domain of the function, Y is the codomain, and F is a set of ordered pairs.” As it later points out, X and/or Y are often omitted, but F is still required to be a set. | |
| Oct 6, 2010 at 1:07 | comment | added | arsmath | Do people in practice assume the latter? Wikipedia just requires the domain of the diagram functor to be a set. Likewise for Abstract and Concrete Categories. I just looked at Categories for the Working Mathematician, and MacLane explicitly imposes replacement. The usual example of where replacement is needed in analysis is Borel determinancy. | |
| Oct 5, 2010 at 19:56 | comment | added | Peter LeFanu Lumsdaine | I now realise Carl Mummert had already pointed out this ambiguity in a comment 8 hours ago! However, there wasn’t yet an answer taking it into account, so I hope this is still adding something :-) | |
| Oct 5, 2010 at 19:54 | history | answered | Peter LeFanu Lumsdaine | CC BY-SA 2.5 |