diff --git a/.vscode/settings.json b/.vscode/settings.json index 89fdf748..8d0a2d8b 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -39,6 +39,7 @@ "cancellative", "Catabase", "catdat", + "Čech", "clopen", "Clowder", "coaccessible", @@ -74,6 +75,7 @@ "colimits", "comonad", "comonadic", + "compactification", "conormal", "copower", "copowers", @@ -229,9 +231,12 @@ "surjectivity", "Tarski", "tensoring", + "Tietze", "Turso", + "Tychonoff", "unital", "unitalization", + "Urysohn", "vercel", "Vite", "Wedderburn", diff --git a/databases/catdat/data/001_categories/004_topology.sql b/databases/catdat/data/001_categories/004_topology.sql index d29e82b1..080e1103 100644 --- a/databases/catdat/data/001_categories/004_topology.sql +++ b/databases/catdat/data/001_categories/004_topology.sql @@ -35,6 +35,15 @@ VALUES 'This is the full subcategory of $\Top$ consisting of those spaces that are Hausdorff.', 'https://ncatlab.org/nlab/show/Hausdorff+space' ), +( + 'CompHaus', + 'category of compact Hausdorff spaces', + '$\CompHaus$', + 'compact Hausdorff spaces', + 'continuous functions', + 'This is the full subcategory of $\Top$ consisting of those spaces that are compact and Hausdorff.', + 'https://ncatlab.org/nlab/show/compact+Hausdorff+space' +), ( 'sSet', 'category of simplicial sets', @@ -61,4 +70,4 @@ VALUES 'order-preserving maps', 'The simplex category is a skeleton of $\FinOrd \setminus \{\varnothing\}$. It plays an important role in topology and is used to define the category of simplicial sets.', 'https://ncatlab.org/nlab/show/simplex+category' -); \ No newline at end of file +); diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql index cad1441c..f2721ca6 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/databases/catdat/data/001_categories/100_related-categories.sql @@ -34,6 +34,8 @@ VALUES ('CMon','Ab'), ('CMon','CRing'), ('CMon','Mon'), +('CompHaus','Haus'), +('CompHaus','Top'), ('CRing', 'CAlg(R)'), ('CRing', 'Ring'), ('CRing', 'Rng'), @@ -70,6 +72,7 @@ VALUES ('FinGrp', 'FinAb'), ('Haus', 'Top'), ('Haus', 'Met_c'), +('Haus', 'CompHaus'), ('J2', 'M-Set'), ('LRS', 'Sch'), ('M-Set', 'R-Mod'), @@ -189,4 +192,4 @@ VALUES ('walking_span', 'walking_pair'), ('walking_splitting', 'walking_idempotent'), ('walking_splitting', 'walking_isomorphism'), -('walking_splitting', 'walking_coreflexive_pair'); \ No newline at end of file +('walking_splitting', 'walking_coreflexive_pair'); diff --git a/databases/catdat/data/001_categories/200_category-tags.sql b/databases/catdat/data/001_categories/200_category-tags.sql index 95dfde10..89eec732 100644 --- a/databases/catdat/data/001_categories/200_category-tags.sql +++ b/databases/catdat/data/001_categories/200_category-tags.sql @@ -29,6 +29,7 @@ VALUES ('Cat', 'algebra'), ('Cat', 'category theory'), ('CMon', 'algebra'), +('CompHaus', 'topology'), ('CRing', 'algebra'), ('Delta', 'order theory'), ('Delta', 'topology'), @@ -123,4 +124,4 @@ VALUES ('Z', 'algebraic geometry'), ('Z', 'category theory'), ('Z_div', 'number theory'), -('Z_div', 'thin'); \ No newline at end of file +('Z_div', 'thin'); diff --git a/databases/catdat/data/003_category-property-assignments/CompHaus.sql b/databases/catdat/data/003_category-property-assignments/CompHaus.sql new file mode 100644 index 00000000..077a5476 --- /dev/null +++ b/databases/catdat/data/003_category-property-assignments/CompHaus.sql @@ -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 nLab 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 nLab. Therefore, by this result, $\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 nLab. Therefore, by this result, $\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.
+ 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.' +), +( + '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 this result, 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 here.' +), +( + '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 $\Haus$.' +), +( + '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 $\Haus$. 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$.
+ 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.' +); + +-- 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'); diff --git a/databases/catdat/data/003_category-property-assignments/Haus.sql b/databases/catdat/data/003_category-property-assignments/Haus.sql index b25c4ff7..b28e4008 100644 --- a/databases/catdat/data/003_category-property-assignments/Haus.sql +++ b/databases/catdat/data/003_category-property-assignments/Haus.sql @@ -81,7 +81,9 @@ VALUES 'Haus', 'filtered-colimit-stable monomorphisms', FALSE, - 'The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of $[-1/n,+1/n] \hookrightarrow \IR$ with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \leq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, 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 \IR$ in the colimit, which is no monomorphism.' + 'The proof is similar to $\Met$. For $n \geq 1$ let $X_n$ be the pushout of + $$(-\infty, -1/n] \cup [1/n, \infty) \hookrightarrow \IR$$ + with itself. That is, $X_n$ is the union of two lines $\IR \times \{1\}$ and $\IR \times \{2\}$ where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$. Then $X_n$ is Hausdorff, and there is a canonical surjective continuous map $X_n \to X_{n+1}$. The colimit in $\Top$ is the union of two lines where we identify $(x,1) \equiv (x,2)$ when $|x| \geq 1/n$ for some $n$, i.e. when $x \neq 0$. This is the line with the double origin, which is not Hausdorff. Its Hausdorff reflection is the line $\IR$ where all points of both lines are identified, and it provides the colimit in $\Haus$. Now, 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 \IR$ in the colimit, which is not a monomorphism.' ), ( 'Haus', diff --git a/databases/catdat/data/004_category-implications/002_limits-colimits-behavior-implications.sql b/databases/catdat/data/004_category-implications/002_limits-colimits-behavior-implications.sql index d8237c35..66d0b200 100644 --- a/databases/catdat/data/004_category-implications/002_limits-colimits-behavior-implications.sql +++ b/databases/catdat/data/004_category-implications/002_limits-colimits-behavior-implications.sql @@ -260,6 +260,13 @@ VALUES 'This holds by definition of a regular category.', FALSE ), +( + 'regular_well-powered_well-copowered', + '["regular", "epi-regular", "well-powered"]', + '["well-copowered"]', + 'The regularity condition gives a bijection between the collection of quotients of $X$ and the collection of effective congruences on $X$, where the latter is a subcollection of the collection of subobjects of $X\times X$.', + FALSE +), ( 'power_construction', '["copowers", "cartesian closed"]', @@ -294,4 +301,4 @@ VALUES '["CIP"]', 'Let $(X_i)_{i \in I}$ be a family of objects. For every finite subset $E \subseteq I$ the canonical morphism $\coprod_{i \in E} X_i = \prod_{i \in E} X_i \to \prod_{i \in I} X_i$ is a (split) monomorphism. Hence, their colimit is also a monomorphism, which is the canonical morphism $\coprod_{i \in I} X_i \to \prod_{i \in I} X_i$.', FALSE -); \ No newline at end of file +); diff --git a/databases/catdat/data/005_special-objects/002_initial_objects.sql b/databases/catdat/data/005_special-objects/002_initial_objects.sql index 763f583d..9a63500e 100644 --- a/databases/catdat/data/005_special-objects/002_initial_objects.sql +++ b/databases/catdat/data/005_special-objects/002_initial_objects.sql @@ -13,6 +13,7 @@ VALUES ('CAlg(R)', '$R$'), ('Cat', 'empty category'), ('CMon', 'trivial monoid'), +('CompHaus', 'empty space'), ('CRing', 'ring of integers'), ('FI', 'empty set'), ('FinAb', 'trivial group'), diff --git a/databases/catdat/data/005_special-objects/003_terminal_objects.sql b/databases/catdat/data/005_special-objects/003_terminal_objects.sql index 9f95331b..738817dd 100644 --- a/databases/catdat/data/005_special-objects/003_terminal_objects.sql +++ b/databases/catdat/data/005_special-objects/003_terminal_objects.sql @@ -13,6 +13,7 @@ VALUES ('CAlg(R)', 'trivial algebra'), ('Cat', 'trivial category'), ('CMon', 'trivial monoid'), +('CompHaus', 'singleton space'), ('CRing', 'zero ring'), ('FinAb', 'trivial group'), ('FinGrp', 'trivial group'), diff --git a/databases/catdat/data/005_special-objects/004_coproducts.sql b/databases/catdat/data/005_special-objects/004_coproducts.sql index fae68b39..b1d33e9b 100644 --- a/databases/catdat/data/005_special-objects/004_coproducts.sql +++ b/databases/catdat/data/005_special-objects/004_coproducts.sql @@ -15,6 +15,7 @@ VALUES ('CAlg(R)', 'tensor products over $R$'), ('Cat', 'disjoint unions'), ('CMon', 'direct sums'), +('CompHaus', 'Stone-Čech compactification of the disjoint union with the disjoint union topology (in the finite case, the disjoint union is already compact Hausdorff so Stone-Čech compactification is not necessary)'), ('CRing', 'tensor products over $\IZ$'), ('FreeAb', 'direct sums'), ('Grp', 'free products'), diff --git a/databases/catdat/data/005_special-objects/005_products.sql b/databases/catdat/data/005_special-objects/005_products.sql index 091fd6f9..676d1510 100644 --- a/databases/catdat/data/005_special-objects/005_products.sql +++ b/databases/catdat/data/005_special-objects/005_products.sql @@ -15,6 +15,7 @@ VALUES ('CAlg(R)', 'direct products with pointwise operations'), ('Cat', 'direct products with pointwise operations'), ('CMon', 'direct products with pointwise operations'), +('CompHaus', 'direct product with the product topology (which is compact by the Tychonoff product theorem)'), ('CRing', 'direct products with pointwise operations'), ('Grp', 'direct products with pointwise operations'), ('Haus', 'direct product with the product topology'), diff --git a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql index e61b24d0..f640247a 100644 --- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql @@ -85,6 +85,11 @@ VALUES 'bijective homomorphisms', 'This characterization holds in every algebraic category.' ), +( + 'CompHaus', + 'homeomorphisms', + 'This is easy.' +), ( 'CRing', 'bijective ring homomorphisms', diff --git a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql index e0944657..5887549f 100644 --- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql @@ -80,6 +80,11 @@ VALUES 'injective homomorphisms', 'This holds in every finitary algebraic category: the forgetful functor to $\Set$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.' ), +( + 'CompHaus', + 'injective continuous maps (which are automatically closed embeddings)', + 'For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms. To prove the parenthetical remark, given an injective continuous function $f : X \to Y$ between compact Hausdorff spaces, the image of $f$ is a closed subset. Also, the induced map from $X$ to $\im(f)$ with the subspace topology is a bijective continuous map between compact Hausdorff spaces, so it is a homeomorphism.' +), ( 'CRing', 'injective ring homomorphisms', diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql index 342e6cba..e72e8f0c 100644 --- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql @@ -81,6 +81,11 @@ VALUES 'a homomorphism of algebras which is an epimorphism of commutative rings', 'The forgetful functor $\CAlg(R) \to \Ring$ is faithful and hence reflects epimorphisms, but it also preserves epimorphisms since it preserves pushouts (since $\CAlg(R) \cong R / \Ring$). For epimorphisms of commutative rings see their detail page.' ), +( + 'CompHaus', + 'surjective continuous maps (which are automatically quotient maps)', + 'For the non-trivial direction, and for a proof of the parenthetical remark, see the proof above that $\CompHaus$ is epi-regular.' +), ( 'CRing', 'A ring map $f : R \to S$ is an epimorphism iff $S$ equals the dominion of $f(R) \subseteq S$, meaning that for every $s \in S$ there is some matrix factorization $(s) = Y X Z$ with $X \in M_{n \times n}(R)$, $Y \in M_{1 \times n}(S)$, and $Z \in M_{n \times 1}(S)$.', @@ -378,4 +383,4 @@ SELECT category_id, description, reason, 'epimorphisms' FROM epimorphisms; -DROP TABLE epimorphisms; \ No newline at end of file +DROP TABLE epimorphisms; diff --git a/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql b/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql index 78b65fe5..fd82a30c 100644 --- a/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/005_regular-monomorphisms.sql @@ -65,6 +65,11 @@ VALUES 'closed embeddings', 'The non-trivial direction follows from the well-known fact that for every closed subspace of a Banach space its quotient space is again a Banach space.' ), +( + 'CompHaus', + 'same as monomorphisms', + 'This is because the category is mono-regular.' +), ( 'Delta', 'same as monomorphisms', @@ -317,4 +322,4 @@ SELECT category_id, description, reason, 'regular monomorphisms' FROM regular_monomorphisms; -DROP TABLE regular_monomorphisms; \ No newline at end of file +DROP TABLE regular_monomorphisms; diff --git a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql index 89cbf7c7..f7c8860c 100644 --- a/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/006_regular-epimorphisms.sql @@ -74,7 +74,12 @@ VALUES 'CMon', 'surjective homomorphisms', 'This holds in every finitary algebraic category.' -), +), +( + 'CompHaus', + 'same as epimorphisms', + 'This is because the category is epi-regular.' +), ( 'CRing', 'surjective homomorphisms', @@ -327,4 +332,4 @@ SELECT category_id, description, reason, 'regular epimorphisms' FROM regular_epimorphisms; -DROP TABLE regular_epimorphisms; \ No newline at end of file +DROP TABLE regular_epimorphisms; diff --git a/databases/catdat/data/009_lemmas/001_lemmas.sql b/databases/catdat/data/009_lemmas/001_lemmas.sql index a49577c8..b294fc09 100644 --- a/databases/catdat/data/009_lemmas/001_lemmas.sql +++ b/databases/catdat/data/009_lemmas/001_lemmas.sql @@ -177,5 +177,14 @@ INSERT INTO lemmas ( By classical induction on $n \in \IN$ it follows that $$\Phi(a, n \otimes 1) = n \otimes a,$$ which exactly means $\Phi \circ \alpha = \id_{\IN \otimes A}$.' +), +( + 'cofiltered-limit-of-non-empty-compact', + 'Cofiltered limits of non-empty compact Hausdorff spaces are non-empty', + 'Let $\I$ be a cofiltered category, and let $X : \I \to \CompHaus$ be a cofiltered diagram in which $X_i$ is non-empty for each $i \in \I$. Then its limit $\lim_{i \in \I} X_i$ is also non-empty.', + 'Consider the product space $\prod_{i \in \I} X_i$. Now for each morphism $f : i \to j$ in $\I$, define the subset + $$\textstyle E_f := \bigl\{ x \in \prod_{i \in \I} X_i \mid X_f(x_i) = x_j \bigr\}.$$ + Then each $E_f$ is a closed subset.
+ Next, we prove that the collection $\{ E_f : f \in \Mor(\I) \}$ has the finite intersection property, i.e. that $\bigcap_{f \in F} E_f$ is non-empty for every finite set $F \subseteq \Mor(\I)$. For $f \in F$ we write $f : i_f \to j_f$. Then the diagram with objects $J := \{ i_f : f \in F \} \cup \{ j_f : f \in F\}$ and morphisms $\{ f : f \in F \}$ has a cone with vertex $k \in \I$ and morphisms $g_i : k \to i$ for each $i \in J$. Now choose $y \in X_k$, and define $x \in \prod_{i \in \I} X_i$ such that $x_i = X_{g_i}(y)$ if $i \in J$, with arbitrary choices of $x_i \in X_i$ for all other $i$. We then see that $x \in \bigcap_{f \in F} E_f$, which finishes the proof of the claim.
+ Since $\prod_{i \in \I} X_i$ is compact, that implies that the intersection of all $E_f$ is non-empty. But that intersection is precisely $\lim_{i \in \I} X_i$.' ); - diff --git a/src/lib/server/macros.ts b/src/lib/server/macros.ts index e01b47a7..b8c71c35 100644 --- a/src/lib/server/macros.ts +++ b/src/lib/server/macros.ts @@ -77,6 +77,7 @@ export const MACROS = { '\\PMet': '\\mathbf{PMet}', '\\Top': '\\mathbf{Top}', '\\Haus': '\\mathbf{Haus}', + '\\CompHaus': '\\mathbf{CompHaus}', '\\sSet': '\\mathbf{sSet}', '\\Man': '\\mathbf{Man}', '\\LRS': '\\mathbf{LRS}', diff --git a/static/pdf/comphaus_copresentable.pdf b/static/pdf/comphaus_copresentable.pdf new file mode 100644 index 00000000..73fe5d14 Binary files /dev/null and b/static/pdf/comphaus_copresentable.pdf differ diff --git a/static/pdf/comphaus_copresentable.tex b/static/pdf/comphaus_copresentable.tex new file mode 100644 index 00000000..c09212a4 --- /dev/null +++ b/static/pdf/comphaus_copresentable.tex @@ -0,0 +1,66 @@ +\documentclass[a4paper,12pt,reqno]{amsart} +\usepackage[utf8]{inputenc} +\usepackage[top=25truemm,bottom=25truemm,left=20truemm,right=20truemm]{geometry} + +\usepackage{amsmath, amssymb, amsfonts, amscd, amsthm, mathtools} +\newtheorem{lemma}{Lemma} +\newtheorem{corollary}[lemma]{Corollary} + +\newcommand{\Hom}{\operatorname{Hom}} +\newcommand{\op}{\operatorname{op}} +\newcommand{\CompHaus}{\mathbf{CompHaus}} +\newcommand{\Set}{\mathbf{Set}} +\newcommand{\im}{\operatorname{im}} +\newcommand{\id}{\operatorname{id}} +\newcommand{\I}{\mathcal{I}} +\newcommand{\INnz}{\mathbb{N}_{>0}} + +\title{Local $\aleph_1$-copresentability of the category of compact Hausdorff spaces} +\author{Daniel Schepler} +\date{\today} + +\begin{document} +\maketitle + +We let $\CompHaus$ denote the category of compact Hausdorff spaces. + +\begin{lemma} + The functor $\Hom({-}, [0, 1])) : \CompHaus^{\op} \to \Set$ is monadic. + + \begin{proof} + We use the crude monadicity theorem. First, the functor has a left adjoint $S \mapsto [0, 1]^S$ with the evident isomorphism + $$\Hom_{\CompHaus}(X, [0, 1]^S) \simeq \Hom_{\Set}(S, \Hom_{\CompHaus}(X, [0, 1])). $$ + + To see the functor is conservative, suppose we have a continuous function $f : X \to Y$ such that $f^* : \Hom(Y, [0, 1]) \to \Hom(X, [0, 1])$ is a bijection. Then for any $x_1, x_2 \in X$ with $x_1 \ne x_2$, there exists $\varphi : X \to [0, 1]$ with $\varphi(x_1) = 0$ and $\varphi(x_2) = 1$. Since $f^*$ is surjective, there exists $\psi : Y \to [0, 1]$ with $\varphi = \psi \circ f$; thus, we must have $f(x_1) \ne f(x_2)$. Likewise, we know the image of $f$ is closed. If this image is not all of $Y$, then there exists nonzero $\varphi : Y \to [0, 1]$ which is zero on the image. But then $\varphi \circ f = 0 \circ f$, contradicting the injectivity of $f^*$. Thus, $f$ is a bijective continuous function, and therefore a homeomorphism. + + Finally, suppose we have a coreflexive equalizer pair $E \xhookrightarrow{i} A \overset{f}{\underset{g}{\rightrightarrows}} B$ with $r : B \to A$. We may assume that $i$ is a subspace inclusion map. We may use $r$ to think of $B$ as a bundle of compact spaces over $A$, with two sections $f, g$. We then need to show that + $$\Hom(B, [0,1])) \overset{f^*}{\underset{g^*}{\rightrightarrows}} \Hom(A, [0, 1]) \xrightarrow{i^*} \Hom(E, [0, 1])$$ + is a coequalizer diagram. We first define $s : \Hom(E,[0,1]) \to \Hom(A,[0,1])$ by choosing a Tietze extension of each continuous function $E \to [0,1]$. Now, for each $\varphi \in \Hom(A,[0,1])$, we can define a continuous function on $\im(f) \cup \im(g) \subseteq B$ to be $\varphi \circ r$ on $\im(f)$, and $s(i^*(\varphi))\circ r$ on $\im(g)$. Note that on the overlap $\im(f)\cap \im(g) = f(E) = g(E)$, the first expression gives $f(e) \mapsto \varphi(e)$, and the second expression gives $g(e) \mapsto s(i^*(\varphi))(e) = \varphi(e)$, so we have indeed given a well-defined function on $\im(f)\cup\im(g)$. Choosing a Tietze extension of this function to a function $B\to [0,1]$ for each $\varphi$, we get a map $t : \Hom(A,[0,1]) \to \Hom(B,[0,1])$. By construction, we have $i^* s = \id$, $f^* t = \id$, and $g^* t = s i^*$, so we have shown that the diagram above is a split coequalizer. + \end{proof} +\end{lemma} + +This shows that $\CompHaus^{\op}$ is equivalent to the category of algebras over the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$. We may view such algebras as being models of the algebraic theory of all continuous functions $[0,1]^S \to [0,1]$. In fact, we can show that any such function only depends on countably many coordinates in the domain, so that operations of this theory will be generated by the continuous functions $[0,1]^\omega \to [0,1]$. + +\begin{lemma} + The object $[0,1]$ of $\CompHaus$ is $\aleph_1$-copresentable. + + \begin{proof} + Suppose we have an $\aleph_1$-cofiltered limit $X = \lim_{i\in \I} X_i$ with projections $p_i : X \to X_i$, and a continuous function $\varphi : X \to [0,1]$. Then for any $x\in X$ and $n\in \INnz$, there exists an interval neighborhood $N_x$ of $\varphi(x)$ of diameter at most $1/n$, along with a basic open neighborhood $\bigcap_{a=1}^b p_{i_a}^{-1}(U_a)$ of $x$ whose image is contained in $N_x$. Taking a cone $(j, f_a : j \to i_a)$ of $i_1, \ldots, i_b$, we may form $V := \bigcap_{a=1}^b X_{f_a}^{-1}(U_a)$; the basic open neighborhood is then equal to $p_j^{-1}(V)$. + + By compactness of $X$, we may take finitely many such basic open neighborhoods of the form $p_j^{-1}(V)$ which cover $X$. Again using the assumption that $\I$ is cofiltered, we may assume that $j$ is the same for each neighborhood. In particular, we see that whenever we have $x, y\in X$ with $p_j(x) = p_j(y)$, then $|\varphi(x) - \varphi(y)| < 1/n$. + + Now choose such a $j_n$ for each $n$, and then use the fact that $\I$ is $\aleph_1$-cofiltered to take a cone $(k, f_n : k \to j_n)$. We then see that whenever we have $x, y\in X$ with $p_k(x) = p_k(y)$, then $\varphi(x) = \varphi(y)$. Thus, $\varphi$ induces a well-defined function on the image of $p_k$. This function is continuous, since by construction for any $n\in \INnz$ and $x \in X$, there is a neighborhood $V$ of $p_k(x)$ such that whenever $p_k(y)\in V$ as well, $|p_k(y) - p_k(x)| < 1/n$. This induced function can then can be extended to a continuous function $\psi : X_k \to [0,1]$ such that $\varphi = \psi \circ p_k$. + + Likewise, suppose we have $\varphi, \psi : X_i \to [0,1]$ such that $\varphi \circ p_i = \psi \circ p_i$. For each $n\in \INnz$, consider the set $D_n := \{ x \in X_i \mid |\varphi(x) - \psi(x)| \ge 1/n \}$. For any $x \in D_n$, we must have $x \notin \im(p_i)$. Now recall that we previously proved a result that a cofiltered limit of non-empty compact Hausdorff spaces is nonempty. Using the contrapositive of this, we can conclude that if $x \notin \im(p_i)$, then there exists $f : j \to i$ such that $x \not\in \im(X_f)$. Now $D_n \setminus \im(X_f)$ is open and such sets cover $D_n$; taking a finite subcover and then using the cofiltering assumption again, we conclude that there is a single $f_n : j_n \to i$ such that $\im(X_{f_n})$ is disjoint from $D_n$. Using the $\aleph_1$-cofiltering assumption to take a cone of the $f_n$, we get that there is $f : k \to i$ such that $\im(X_f)$ is disjoint from all $D_n$. This means that $\phi \circ F_f = \psi \circ F_f$. + \end{proof} +\end{lemma} + +\begin{corollary} + The category $\CompHaus$ is $\aleph_1$-copresentable. + + \begin{proof} + It suffices to show that the monad $S \mapsto \Hom_{\CompHaus}([0, 1]^S, [0, 1])$ is $\aleph_1$-accessible. This monad is the composition of $[0, 1]^{-} : \Set \to \CompHaus^{\op}$ followed by $\Hom_{\CompHaus}({-}, [0,1]) : \CompHaus^{\op} \to \Set$. The first automatically preserves $\aleph_1$-filtered colimits (and in fact all colimits) since it has a right adjoint. The second one preserves $\aleph_1$-filtered colimits by the previous lemma. + \end{proof} +\end{corollary} + +\end{document}