Timeline for Unnecessary uses of the axiom of choice
Current License: CC BY-SA 4.0
8 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Feb 20, 2022 at 22:24 | comment | added | Todd Trimble | @PeterLeFanuLumsdaine That's a fair point. | |
| Feb 20, 2022 at 10:17 | comment | added | Peter LeFanu Lumsdaine | @ToddTrimble: morally the AFT doesn’t require choice — but it’s often stated in the literature in forms that do require choice, by taking the completeness assumption as mere existence of limits, but requiring an actual functor in the conclusion. Of course the real culprit here is a mismatched choice of definitions — the “universal object” conditions should either all be stated as chosen functions (so the input includes chosen limits) or all stated as mere existence conditions (so the output is representability conditions, or an adjoint anafunctor). | |
| Feb 18, 2022 at 21:28 | comment | added | Todd Trimble | @Z.M No, the adjoint functor theorems (whether SAFT or GAFT or some variant) don't use choice. | |
| Feb 18, 2022 at 19:43 | comment | added | Z. M | Related to the comment above: does the adjoint functor theorem rely on the axiom of choice? Or weaker, the criterion for representable presheaves? It is also "unique" in some sense. | |
| Feb 18, 2022 at 16:41 | comment | added | Tim Campion | @TomLeinster Yes, I certainly wasn't trying to suggest that there should be a general metatheorem saying that unique existence should imply independence of choice, but I didn't actually know any counterexamples, so thanks for the link! | |
| Feb 18, 2022 at 13:25 | comment | added | Tom Leinster | I'm sure you know this, Tim, but let me just record here that unique existence is no guarantee that AC is unnecessary. There's a whole MO question about this. | |
| S Feb 18, 2022 at 13:00 | history | answered | Tim Campion | CC BY-SA 4.0 | |
| S Feb 18, 2022 at 13:00 | history | made wiki | Post Made Community Wiki by Tim Campion |