Timeline for Reflection principle vs universes
Current License: CC BY-SA 4.0
19 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Jan 30, 2021 at 22:27 | comment | added | David Roberts♦ | These all sound like arguments in favour of having Kerodon contain these more sophisticated treatments | |
| Jan 30, 2021 at 19:59 | comment | added | Peter Scholze | OK, we seem to agree on "Probably yes, but you have to put some effort in". Your last argument convinced me: One should definitely get credit for a translation into ZFC. Later tonight, I'll try to write another longer answer to some questions that came up. | |
| Jan 30, 2021 at 18:37 | comment | added | Tim Campion | Well, I'm certainly rambling now, but I think we can at least say we've reached the conclusion that the question is MO-hard. | |
| Jan 30, 2021 at 18:23 | comment | added | Tim Campion | One more precisification: If a bright young professor were to rewrite HTT in a weaker formal system and then proudly present the results to the tenure committee as the centerpiece of their resume, should they get tenure? Of course, the question is still too ill-defined to answer as stated. Coming into this, I would have been somewhat sympathetic to the answer of "no", but I think after looking at these examples, I'd be more inclined to champion the cause of this hypothetical researcher. | |
| Jan 30, 2021 at 18:19 | comment | added | Tim Campion | Here's another precisification: If we were to rewrite HTT in a weaker formal system and then, before publishing our new book, upload its theorem statements onto wikipedia articles, would our edits be taken down for being "original research"? Again I think the the test cases we've seen suggest the answer is "yes". | |
| Jan 30, 2021 at 18:15 | comment | added | Tim Campion | It's difficult to reach a clear conclusion on an ambiguous question like "Does the book essentially work in a weaker formal system". Here's a slightly more precise version of that question: "To rewrite the book in a weaker formal system, would it be easier to keep the same theorem numbering and just make some line-by-line edits, or rather to invest time in rethinking the basic organization of the book, and write a new book which closely mirrors the original but does not attempt to be a direct translation?" I think the test cases we've seen suggest that the answer is the latter. | |
| Jan 30, 2021 at 15:35 | comment | added | Tim Campion | To start, we'll have to strengthen the statement of Thm 5.1.5.6, where the existence of $P(f)$ is deduced from the model category considerations of Lem 5.1.5.5. We might have to go back to earlier chapters and construct more model categories cut off at regular cardinals, using versions of the small object argument with various cardinal parameters inserted. At this point it feels to me at any rate that we're starting to need new mathematical ideas to push things through. So although I still agree that Grothendieck universes are really a convenience, it underscores just how convenient they are. | |
| Jan 30, 2021 at 15:35 | comment | added | Tim Campion | @PeterScholze I agree that should probably work. It's a bit annoying, because the logic of the book as written (as in most treatments of presentability) is (1) work out the properties of presheaf categories, then (2) apply this to properties of subcategories of presheaf categories. With this approach, it looks like we'll be weaving in some considerations from (2) to the treatment of (1). | |
| Jan 29, 2021 at 22:21 | comment | added | Peter Scholze | OK, I think this is a case where it's better to cut at a regular cardinal, so take say sets of size $\leq \kappa_0$; this has all colimits of size $\leq \kappa_0$, and has a corresponding freeness property. This is related to the fact that in the theory of presentable categories, all cuts happen at regular cardinals (and those cuts are basically independent of the "universe" cuts). | |
| Jan 29, 2021 at 21:51 | comment | added | Tim Campion | Or maybe I've misunderstood -- I assumed that $Set$ was the category of $\kappa_0$-small sets, but perhaps you're taking $\tilde P(C)$ to be category of $V_{\kappa_1}$-definable functors from $C^{op}$ to the category of $\kappa_1$-small sets. | |
| Jan 29, 2021 at 21:45 | comment | added | Tim Campion | @PeterScholze Interesting. How do we know that $\tilde{ \mathcal P}(f)$ exists? Is there some sense in which we should expect $\tilde{\mathcal P}(C)$ to be a free cocompletion of $C$? After all, $Set$ doesn't have all small colimits ($V_{\kappa_0}$ just thinks it does), so I don't expect that $\tilde{\mathcal P}(C)$ has all small colimits. Of course, for these purposes having small colimits is less important than the freeness of those colimits, but it gives me pause. Or -- do we not need to know it exists, since the proof actually verifies the existence of a left adjoint abstractly? | |
| Jan 29, 2021 at 21:21 | comment | added | Peter Scholze | Thanks! Here's a cheap fix: Besides the "definable" version of $\mathcal P(C)$, one also has the version $\tilde{\mathcal P}(C)$ of functors $C^{op}\to \mathrm{Set}$ in $V_{\kappa_1}$. The proof works as written for $\tilde{\mathcal P}$, but both $\tilde{\mathcal P}(f)$ and $\tilde{G}$ preserve the subcategory $\mathcal P(C)\subset \tilde{\mathcal P}(C)$ (inducing $\mathcal P(f)$ and $G$), so one gets an induced adjunction on these full subcategories which is we one we want. | |
| Jan 29, 2021 at 17:27 | comment | added | Tim Campion | Sorry, I've misunderstood the proof of 5.2.6.3 a bit. The functor $P(f)$ was constructed earlier and is already known to be functorial. So the peculiar form of the proof is for some other reason which I don't fully understand. But at the very least, the proof does not work as written in the proposed formal system, even when the definitions involved are understood to have been modified. | |
| Jan 29, 2021 at 16:25 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 67 characters in body
|
| Jan 29, 2021 at 16:00 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 2564 characters in body
|
| Jan 29, 2021 at 15:54 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 2564 characters in body
|
| Jan 29, 2021 at 5:43 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 227 characters in body
|
| Jan 29, 2021 at 5:30 | history | edited | Tim Campion | CC BY-SA 4.0 |
added 2 characters in body
|
| Jan 29, 2021 at 5:24 | history | answered | Tim Campion | CC BY-SA 4.0 |