Timeline for Adjusting the definition of a well-powered category to category theory with universes: size issues
Current License: CC BY-SA 4.0
14 events
| when toggle format | what | by | license | comment | |
|---|---|---|---|---|---|
| Oct 24, 2019 at 7:05 | vote | accept | Jxt921 | ||
| Oct 22, 2019 at 13:05 | comment | added | Dmitri Pavlov | @Jxt921: You do not need such a roundabout way to show this (i.e., reduction to products and equalizers). Rather, the same data of a limit cone is also a limit cone for an isomorphic diagram. | |
| Oct 22, 2019 at 8:29 | comment | added | Jxt921 | admitting products depends only on the index set being isomorphic to an element $\mathcal{U}$ not being itself being a $\mathcal{U}$-set (if it not a $\mathcal{U}$-set, we can reindex by the isomorphic $\mathcal{U}$-set and obtain the same product up to isomorphism). | |
| Oct 22, 2019 at 8:27 | comment | added | Jxt921 | @DmitriPavlov Yeah, that was essentially my point, that the set of equivalence classes of subobject being only isomorphic to an element of $\mathcal{U}$ is not a problem, since if a category $\mathsf{D}$ admits limits indexed by categories $\mathsf{C}$ with $\mathsf{Ob(C)}$ and $\mathsf{Mor(C)}$ being $\mathcal{U}$-sets, then it also admits limits indexed by categories $\mathsf{C}$ with $\mathsf{Ob(C)}$ and $\mathsf{Mor(C)}$ being merely isomorphic to $\mathcal{U}$-sets. This follows, for example, from the construction of a limit by products and equivalizers, since | |
| Oct 21, 2019 at 19:12 | comment | added | Andrej Bauer | Yes, as I said, the book probaly makes false claims. No wonder you can derive $\bot$ from them. To derive a contradiction, you would need only true claims and correct reasoning which results $\bot$. Or are all the claim in the book true, yet they imply $\bot$? But perhaps we can drop this, as it is not pertinent to the question, it's just a logician's quibble. | |
| Oct 21, 2019 at 17:30 | comment | added | Dmitri Pavlov | @AndrejBauer: I added more details. And there is a contradiction in the formal sense: starting from the definitions and claims made in the book, we can derive ⟂. | |
| Oct 21, 2019 at 17:26 | history | edited | Dmitri Pavlov | CC BY-SA 4.0 |
added 136 characters in body
|
| Oct 21, 2019 at 8:37 | comment | added | Andrej Bauer | Well then you should perhaps change your answer, because it reads as if you're claiming that Definition 4.1.2 contradicts Axiom 1.1.7. A definition can never create a logical inconsistency, only its uses can. And Borceaux does not reach a contradiction, he make a false statement (that certain categories are well-powered when according to his setup they are not), but that is not a contradiction. A contradiction would be reached if he proved $A$ and $\lnot A$. | |
| Oct 20, 2019 at 23:56 | comment | added | Dmitri Pavlov | @Jxt921: What is important for the special adjoint functor theorem is that you can take limits indexed by the category of all subobjects. So if your categories admit limits indexed by categories with a U-set of morphisms, then the proof goes through. Normally, when one defines completeness in this setting, admitting limits with respect to such categories is part of the definition of completeness. | |
| Oct 20, 2019 at 23:49 | comment | added | Dmitri Pavlov | @AndrejBauer: I really do mean contradiction in the strictest possible logical sense. Borceux claims immediately after Definition 4.1.2 that sets, groups, and topological spaces are well-powered categories, which is false using his definition as stated. | |
| Oct 20, 2019 at 19:55 | comment | added | Andrej Bauer | What you call a contradiction isn't really a logical contradiction, is it? I mean, the definitions are formally OK, although one might not get very many interesting large well-powered categories this way. | |
| Oct 20, 2019 at 19:32 | comment | added | Jxt921 | by categories whose sets of objects and morphisms of $\mathcal{U}$-sets. This stems from the obsevation that if $I$ is isomorphic to an element of $\mathcal{U}$ and $(X_i)_{i \in I}$ if a family of objects, then we can find an element $J$ of $\mathcal{U}$ and reindex $X_i$'s by $j \in J$. Hence, a category admits (co)products whose index sets are $\mathcal{U}$-small if and only if it admits (co)products whose index sets are $\mathcal{U}$-sets. | |
| Oct 20, 2019 at 19:30 | comment | added | Jxt921 | Dear Dmitri, regarding your definition of a well-powered category, will it work if we demand $Q$ to be a $\mathcal{U}$-set, working with universes via the second approach mentioned in my question as in DHKS and Cisinksi). I thought about it regarding Special Adjoint Functor Theorem, and it seems fine since a category admits (co)limits indexed by categories whose sets of objects and morphisms are $\mathcal{U}$-small (in the sense of being isomorphic to an element of $\mathcal{U}$) if and only if it admits (co)limits indexed | |
| Oct 20, 2019 at 14:59 | history | answered | Dmitri Pavlov | CC BY-SA 4.0 |