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.
Ralph Sarkis (Oct 30 2022 at 21:40):The usual proof to obtain any limit out of products and equalizers relies on the axiom of choice (to choose the products, since we only need existence of the equalizer, we don't need to choose one). Can we prove this without the axiom of choice?
Morgan Rogers (he/him) (Oct 30 2022 at 21:47):This question confuses me. The result you're quoting is the construction of the limit of a given diagram as an equalizer of a pair of arrows between products determined by the diagram (assuming the latter exist). If the choice you're talking about it the choice of a specific representative of the product in order to form the equalizer diagram, how could the construction possibly avoid such a choice? But moreover, how does that depend on the axiom of choice?
Ralph Sarkis (Oct 30 2022 at 22:09):Ralph Sarkis said:
Can we prove this without the axiom of choice?
I was using "this" (rather clumsily) to refer to the statement: If has products and equalizers, then it is complete. The usual way to prove this is by giving a construction (the one you described) that uses choice. Is there another way to prove existence of the limits without necessarily constructing them?, or constructing them without choice?
Morgan Rogers (he/him) (Oct 30 2022 at 22:33):But in a constructive setting, "having products and equalizers" means "having specified products and equalizers"; there's no choice involved
Ralph Sarkis (Oct 30 2022 at 22:45):I see. Thanks!
Morgan Rogers (he/him) (Oct 30 2022 at 22:58):I said that rather authoritatively, but it's true that there's some subtlety here: in Set we need choice to assert that we can construct an element of a product, but the "construction" of the product itself is choice free. On the other hand, when we construct one category from another, the new category may inherit structure such as products but without inheriting a specified choice, and so asserting that it "has products" in the sense of specified products requires some form of choice. I don't have good examples to hand, but Johnstone discusses this at some point in Sketches of an Elephant (if it's of interest I can find the ref tomorrow)
Ralph Sarkis (Oct 30 2022 at 23:20):It's ok, I was just wondering whether I should point out the choice we make when I teach this proof, but I think this subtlety goes too far.
David Michael Roberts (Oct 31 2022 at 12:58):One could consider the anafunctor approach à la Makkai, and have the limit-assigning functor be an anafunctor, and leverage this to construct a limit-assigning anafunctor for an arbitrary diagram shape. No choice needed at all.
Mike Shulman (Oct 31 2022 at 15:57):Morgan Rogers (he/him) said:
when we construct one category from another, the new category may inherit structure such as products but without inheriting a specified choice, and so asserting that it "has products" in the sense of specified products requires some form of choice.
This is technically true, but examples of this sort are quite rare. In the vast majority of cases, when a constructed category inherits limits and colimits from its inputs, it does so in a constructive "specified" way. The only counterexamples I know of are "homotopy category" type constructions where one quotients the "natural" morphisms by some equivalence relation, and constructing limits or colimits requires a choice of representatives for some equivalence classes of morphisms. This is even rarer than it might appear, because the average "homotopy category" doesn't even have all limits and colimits, even classically (and those that it does have, like products and coproducts, don't have arrows as inputs and hence don't require choice either). The only naturally-occurring example I'm aware of where a "homotopy category" does have limits and colimits is the one in the Elephant, namely "exact completion" constructions. Not that these aren't important, but one shouldn't overstate the magnitude of the issue (and there are also other ways to think about exact completions).
Mike Shulman (Oct 31 2022 at 15:59):Furthermore, unless I'm missing something, I think the usual construction of limits from products and equalizers works just fine constructively if we interpret both the products/equalizers and the limits in an unspecified way. To prove that unspecified limits exist, all you need is that one product and one equalizer exist, not that there is a specified choice of all of them.
Morgan Rogers (he/him) (Oct 31 2022 at 16:48):Mike Shulman said:
Not that these aren't important, but one shouldn't overstate the magnitude of the issue (and there are also other ways to think about exact completions).
Fair enough. I was vaguely picturing a situation where we construct a category over another in which the fibers are groupoids with no specified section, but didn't have a specific construction in mind.