-
Notifications
You must be signed in to change notification settings - Fork 7
Add category of compact Hausdorff spaces #160
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Draft
dschepler
wants to merge
17
commits into
ScriptRaccoon:main
Choose a base branch
from
dschepler:comphaus
base: main
Could not load branches
Branch not found: {{ refName }}
Loading
Could not load tags
Nothing to show
Loading
Are you sure you want to change the base?
Some commits from the old base branch may be removed from the timeline,
and old review comments may become outdated.
Draft
Changes from all commits
Commits
Show all changes
17 commits
Select commit
Hold shift + click to select a range
0ad868b
Add category of compact Hausdorff spaces
dschepler 174d53a
Fix the details of a proof which will be referred to in CompHaus proofs
dschepler 1403c28
Add a general result to help deducing CompHaus is well-copowered
dschepler aab318f
Add assignments for CompHaus
dschepler 9d8272d
Add special objects and morphisms for CompHaus
dschepler a499c4d
Add more property assignments
dschepler 28f922b
Other assignments have made it auto-deducible that CompHaus is not ca…
dschepler 227b570
Update databases/catdat/data/003_category-property-assignments/CompHa…
dschepler 9a1257d
Update databases/catdat/data/003_category-property-assignments/CompHa…
dschepler 2aeb245
Update databases/catdat/data/004_category-implications/002_limits-col…
dschepler f34e6a7
Update databases/catdat/data/003_category-property-assignments/CompHa…
dschepler ab80a1d
Update databases/catdat/data/003_category-property-assignments/CompHa…
dschepler 4d6e882
Update databases/catdat/data/003_category-property-assignments/CompHa…
dschepler a1198f8
Update databases/catdat/data/003_category-property-assignments/Haus.sql
dschepler f6d696a
Fix typo in nLab link
dschepler c0ef441
Address review comments on assignments, and add a new one
dschepler ae2de90
Update special morphisms proofs to address review comments
dschepler File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
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
140 changes: 140 additions & 0 deletions
140
databases/catdat/data/003_category-property-assignments/CompHaus.sql
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,140 @@ | ||
| 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 compatification 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 compatification.' | ||
| ), | ||
| ( | ||
| -- 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', | ||
| 'well-powered', | ||
| TRUE, | ||
| 'This is clear from the description of monomorphisms as closed embeddings.' | ||
| ), | ||
| ( | ||
| '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', | ||
| '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 | ||
| $$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', | ||
| 'accessible', | ||
| FALSE, | ||
| 'For any small regular cardinal $\kappa$, consider the $\kappa$-directed system $\kappa \to \CompHaus$, where for ordinal $\alpha < \kappa$ we have $\alpha \mapsto [0, \alpha]$, and for $\alpha \le \beta < \kappa$ the morphism $\alpha \to \beta$ maps to the inclusion map $[0, \alpha] \hookrightarrow [0, \beta]$. Then the direct colimit in $\Top$ of $[0, \alpha]$ is $\kappa$, so the direct colimit in $\CompHaus$ is the Stone-Čech compactification $\tilde\kappa$ of $\kappa$.<br> | ||
| We now claim that any nonempty object $K$ of $\CompHaus$ is not $\kappa$-presentable for any small regular cardinal $\kappa$. If so, then choose a point $x \in \tilde \kappa \setminus \kappa$, and consider the constant map $K \to \tilde \kappa$ with value $x$. By the assumption, this would have to factor through $[0, \alpha]$ for some ordinal $\alpha < \kappa$. That means that the constant value $x$ is in $[0, \alpha] \subseteq \kappa$, contradicting the choice of $x$.<br> | ||
| Now any colimit in $\CompHaus$ of empty spaces is empty, showing that $\CompHaus$ is not accessible.'); | ||
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.
We can remove this because of http://localhost:5173/category-implication/pretopos_balanced
On the second thought, maybe we should keep it because you are using this in the proof of coregularity below.
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.
I don't see how we can remove this. The pretopos_balanced inference is used to infer the category is mono-regular; but if I try commenting this out, the system can't infer it's well-powered.
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.
it seems you already removed this now. But as mentioned, maybe we should not do it.