Add category of compact Hausdorff spaces #160
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,146 @@ | ||
| INSERT INTO category_property_assignments ( | ||
| category_id, | ||
| property_id, | ||
| is_satisfied, | ||
| reason | ||
| ) | ||
| VALUES | ||
| ( | ||
| 'CompHaus', | ||
| 'locally small', | ||
| TRUE, | ||
| 'This is trivial.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'generator', | ||
| TRUE, | ||
| 'The one-point space is a generator because it represents the forgetful functor to $\Set$, which is faithful.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'products', | ||
| TRUE, | ||
| 'By the Tychonoff product theorem, a product in $\Top$ of compact Hausdorff spaces is compact; it is also clearly Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'equalizers', | ||
| TRUE, | ||
| 'The equalizer in $\Top$ of two continuous functions $f, g : X \rightrightarrows Y$ between compact Hausdorff spaces is a closed subspace of $X$, and therefore it is also compact Hausdorff. Since the forgetful functor from $\CompHaus$ to $\Top$ is fully faithful, this limit is reflected in $\CompHaus$ as well.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'cocomplete', | ||
| TRUE, | ||
| '$\CompHaus$ is a reflective subcategory of $\Top$, with the reflector being the Stone-Čech compactification functor. See <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#StoneCechCompactification" target="_blank">nLab</a> for example. Therefore, as usual, we can form colimits in $\CompHaus$ by forming colimits in $\Top$ and then applying Stone-Čech compactification.' | ||
| ), | ||
| ( | ||
| -- TODO: rework this when Barr-exact property is added | ||
| 'CompHaus', | ||
| 'regular', | ||
| TRUE, | ||
| 'The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#compact_hausdorff_spaces_are_monadic_over_sets">nLab</a>. Therefore, by <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">this result</a>, $\CompHaus$ is Barr-exact and in particular is regular.' | ||
| ), | ||
| ( | ||
| -- TODO: rework this when Barr-exact property is added | ||
| 'CompHaus', | ||
| 'effective congruences', | ||
| TRUE, | ||
| 'The forgetful functor from $\CompHaus$ to $\Set$ is monadic; see for example <a href="https://ncatlab.org/nlab/show/compact+Hausdorff+space#compact_hausdorff_spaces_are_monadic_over_sets">nLab</a>. Therefore, by <a href="https://ncatlab.org/nlab/show/colimits+in+categories+of+algebras#exact">this result</a>, $\CompHaus$ is Barr-exact, and in particular it has effective congruences.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'cogenerator', | ||
| TRUE, | ||
| 'The unit interval $[0, 1]$ is a cogenerator: Suppose we have $f, g : X \rightrightarrows Y$ with $f \ne g$. Choose $x\in X$ such that $f(x) \ne g(x)$. Then by Urysohn''s lemma, there is a continuous function $h : Y \to [0, 1]$ such that $h(f(x)) = 0$ and $h(g(x)) = 1$. Therefore, $h\circ f \ne h\circ g$.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'extensive', | ||
| TRUE, | ||
| 'This follows as for $\Top$ or $\Haus$ since finite coproducts in $\CompHaus$ are formed as disjoint union spaces with the disjoint union topology.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'epi-regular', | ||
| TRUE, | ||
| 'First, any epimorphism $f : X\to Y$ is surjective: if not, its image would be a proper subset of $Y$, which is compact and hence closed. Then by Urysohn''s lemma, there would be a non-zero continuous function $g : Y \to [0, 1]$ which is $0$ on the image; but then $g \circ f = 0 \circ f$, giving a contradiction.<br> | ||
| Now the identity morphism from $Y$, with the quotient topology of $f$, to $Y$ with its given topology is a bijective continuous function between compact Hausdorff spaces, so it is a homeomorphism. In other words, $f$ is a quotient map. Therefore, we see that if $g, h : E \rightrightarrows X$ is the kernel pair of $f$, and $U : \CompHaus \to \Top$ is the forgetful functor, then $U(f)$ is the coequalizer of $U(g)$ and $U(h)$. Since $U$ is fully faithful, that implies $f$ is the coequalizer of $g$ and $h$.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'semi-strongly connected', | ||
| TRUE, | ||
| 'Every non-empty compact Hausdorff space is weakly terminal (by using constant maps).' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'coregular', | ||
| TRUE, | ||
| 'It suffices to show that pushouts preserve (regular) monomorphisms in $\CompHaus$. Thus, suppose we have a pushout square | ||
| $$\begin{CD} | ||
| A @> i >> B \\ | ||
| @V f VV @VV g V \\ | ||
| C @>> j > D, | ||
| \end{CD}$$ | ||
| with $i : A \hookrightarrow B$ a monomorphism. Then for any pair of distinct elements $c, c'' \in C$, by Urysohn''s lemma there exists $\gamma : C \to [0, 1]$ with $\gamma(c) = 0$ and $\gamma(c'') = 1$. Also, by Tietze''s extension theorem, there exists $\beta : B \to [0, 1]$ such that $\beta \circ i = \gamma \circ f$. By the pushout property, there is a unique $\delta : D \to [0, 1]$ such that $\delta \circ g = \beta$ and $\delta \circ j = \gamma$. Since $\delta(j(c)) \ne \delta(j(c''))$, we conclude that $j(c) \ne j(c'')$. This shows that $j$ is injective, so it is a regular monomorphism.' | ||
|
ScriptRaccoon marked this conversation as resolved.
|
||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'cofiltered-limit-stable epimorphisms', | ||
| TRUE, | ||
| 'Suppose we have a cofiltered diagram of epimorphisms $(f_i : X_i \to Y_i)$, and $y = (y_i) \in \lim_i Y_i$. Then by <a href="/lemma/cofiltered-limit-of-non-empty-compact">this result</a>, the limit of $f_i^{-1}(\{ y_i \})$ is non-empty. If $x$ is in this limit, that implies that $(\lim_i f_i)(x) = y$.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'locally copresentable', | ||
| TRUE, | ||
| 'A proof can be found <a href="/pdf/comphaus_copresentable.pdf">here</a>.' | ||
|
Owner
There was a problem hiding this comment. Please also add an original reference for this result (see my comments). Either here or in the pdf. Otherwise, readers might get a wrong impression with regards to orginality. In any case, I think it is very good if we offer a well-written proof directly in CatDat. Thank you for adding it! |
||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'Malcev', | ||
| FALSE, | ||
| 'This is clear since $\FinSet$ is not Malcev and can be interpreted as the subcategory of finite discrete spaces.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'skeletal', | ||
| FALSE, | ||
| 'This is trivial.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'regular subobject classifier', | ||
| FALSE, | ||
| 'The proof is almost identical to the one for <a href="/category/Haus">$\Haus$</a>.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'natural numbers object', | ||
| FALSE, | ||
| 'Let $I := [0, 1]$. If a natural numbers object $(N, z : 1 \to N, s : N \to N)$ existed, then we could iterate the initial conditions $I\to I\times I$, $x \mapsto (x, x)$ and the recursive step function $I\times I \to I \times I$, $(x, y) \mapsto (x, xy)$ to get a continuous function $N \times I \to I \times I$ such that $(s^n(z), x) \mapsto (x, x^n)$ for $x\in I$, $n \in \IN$. The sequence $(s^n(z)) \in N$ has a convergent subnet $(s^{n_\lambda}(z))_{\lambda \in \Lambda}$, say with limit $y$. Thus, for any $x\in I$ and $\lambda \in \Lambda$, we have $(s^{n_\lambda}(z), x) \mapsto (x, x^{n_\lambda})$. Taking limits, we see $(y, x) \mapsto (x, 0)$ if $x \ne 1$ or $(y, x) \mapsto (x, 1)$ if $x = 1$. In other words, $(y, x) \mapsto (x, \delta_{x, 1})$ for all $x\in I$. However, that contradicts the fact that the composition | ||
|
ScriptRaccoon marked this conversation as resolved.
|
||
| $$I \overset{y \times \id}\longrightarrow N\times I \to I\times I \overset{p_2}\longrightarrow I,$$ | ||
| $$x \mapsto (y, x) \mapsto (x, \delta_{x,1}) \mapsto \delta_{x,1},$$ | ||
| would have to be continuous.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'filtered-colimit-stable monomorphisms', | ||
| FALSE, | ||
| 'The proof is similar to <a href="/category/Haus">$\Haus$</a>. For $n \geq 1$ let $X_n$ be the pushout of $[1/n, 1] \hookrightarrow [0, 1]$ with itself. That is, $X_n$ is the union of two unit intervals $[0, 1] \times \{ 1 \}$ and $[0, 1] \times \{ 2 \}$ where we identify $(x,1) \equiv (x,2)$ when $x \geq 1/n$. As in the construction for $\Haus$, we see that the colimit in $\Haus$ is $[0, 1]$ where all corresponding points of both unit intervals are identified. Since this is compact Hausdorff, it also provides the colimit in $\CompHaus$. Again, the injective continuous maps $\{1,2\} \to X_n$, $i \mapsto (0,i)$ (where $\{1,2\}$ is discrete) become the constant map $0 : \{1,2\} \to [0,1]$ in the colimit, which is not a monomorphism.' | ||
| ), | ||
| ( | ||
| 'CompHaus', | ||
| 'exact cofiltered limits', | ||
| FALSE, | ||
| 'Consider the $\IN$-codirected systems $X_n := [0, 1] \times [0, 1/n]$ with the maps $X_{n+1} \to X_n$ being inclusion maps, and $Y_n := [0, 1+1/n]$ with the maps $Y_{n+1} \to Y_n$ also being inclusion maps. We define $f_n : X_n \to Y_n$, $(x, y) \mapsto x$ and $g_n : X_n \to Y_n$, $(x, y) \mapsto x+y$. It is straightforward to check these give morphisms of $\IN$-codirected systems in $\CompHaus$.<br> | ||
| Now for each $n$, the coequalizer of $f_n$ and $g_n$ is a single-point space. On the other hand, $\lim X_n \simeq [0, 1] \times \{ 0 \}$; $\lim Y_n \simeq [0, 1]$; and $\lim f_n = \lim g_n$, $(x, 0) \mapsto x$. Thus, the coequalizer of $\lim f_n$ and $\lim g_n$ is $[0, 1]$, showing that this coequalizer is not preserved under limits.' | ||
|
Owner
There was a problem hiding this comment. Can wee add the proof that the coequalizer of We need to prove that every (continuous) map More generally, let Case 1: Values on Case 2: Values on |
||
| ); | ||
|
|
||
| -- properties that should be ignored by the redundancy check script | ||
| UPDATE category_property_assignments | ||
| SET check_redundancy = FALSE | ||
| WHERE category_id = 'CompHaus' | ||
| AND property_id IN ('products', 'equalizers'); | ||
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
maybe?