Repository navigation
Add category of compact Hausdorff spaces #156
Description
Activity
- added a parent issue
on May 4, 2026 This is a very interesting example we should definitely add. Do you want to work on this?
In my experience, adding a category is much easier and faster than adding a property.
Do you want to work on this?
Yes, that was my intention.
I notice in the parent issue you used CompHaus which I also like better than Comp. (I was just choosing the latter to match what nLab called it.)
Reacted by Script RaccoonYes, longer names tend to be better, because they tell the reader exactly what it is, and also they are more future-proof. When we want to add the category of compact abelian groups (which should also happen at some point), CompAb is the obvious candidate, and then having Comp and CompAb at the same time looks weird, but CompHaus and CompAb (and CompTop, CompMet, CompCRing, etc.) look nice together. For this reason I also went for SemiNormVect.
I have questions about the proof that Haus does not have filtered-colimit-stable monomorphisms, which I was considering trying to adapt to CompHaus. The main point is: did you mean to make
$X_n$ be the double line with$(\infty, -\frac{1}{n}]$ and$[\frac{1}{n}, \infty)$ identified? That would make more sense in the construction of surjective continuous maps$X_n \to X_{n+1}$ , and in the colimit in Top being the line with doubled origin.This sounds correct. I would appreciate if you fix the proof for Haus then. I'm glad it's just a "notation bug".
- linked a pull request that will close this issueAdd category of compact Hausdorff spaces #160
on May 5, 2026
I thought I'd like to take a break from the properties side of things, and add a category example of the category Comp of compact Hausdorff spaces. Among the properties which are interesting to me: