Add the category of uniform spaces

.cspell.json

@@ -19,7 +19,8 @@
 		"FiltVect",
 		"networkidle",
 		"devlog",
-		"cech"
+		"cech",
+		"Unif"
 	],
 	"words": [
 		"abelian",

database/data/categories/Meas.yaml

@@ -11,6 +11,7 @@ tags:
 
 related:
   - Top
+  - Unif
 
 comments:
   - The thread <a href="https://math.stackexchange.com/questions/5024471/">MSE/5024471</a> asks for the finitely presentable objects of this category.

database/data/categories/Met_c.yaml

@@ -14,6 +14,7 @@ related:
   - Met
   - Met_oo
   - Top
+  - Unif
 
 satisfied_properties:
   - property: locally small

database/data/categories/Top.yaml

@@ -15,6 +15,8 @@ related:
   - Met_c
   - Top_*
   - Man
+  - Unif
+  - Meas
 
 satisfied_properties:
   - property: locally small
@@ -33,30 +35,30 @@ satisfied_properties:
   - property: well-copowered
     proof: This is clear from the classification of epimorphisms as surjective continuous maps.
 
+  - property: filtered-colimit-stable monomorphisms
+    proof: This follows from Lemma 2 <a href="/content/subcategories">here</a> applied to the forgetful functor to $\Set$.
+
   - property: semi-strongly connected
     proof: Every non-empty space is weakly terminal (by using constant maps).
 
   - property: generator
     proof: The one-point space is a generator since it represents the forgetful functor $\Top \to \Set$.
 
-  - property: infinitary extensive
-    proof: 'This can be deduced from the infinitary extensivity of <a href="/category/Set">$\Set$</a> as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets whose open subsets are unions of open subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique topology, it follows immediately that coproducts are disjoint in $\Top$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of topological spaces and let $f : T \to \coprod_{i \in I} X_i$ be a continuous map. Consider the pullbacks $T_i := f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the topology induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical continuous map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is an open map. By the concrete description of open subsets in the disjoint union, it suffices to prove that each $T_i \to T$ is an open map. But this is the inclusion of a subspace, which is open since $X_i$ is open in $\coprod_{i \in I} X_i$.'
+  - property: extremal cogenerator
+    proof: >-
+      Using the dual of Lemma 9 <a href="/content/subcategories">here</a> with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of <a href="/category/Set">$\Set$</a>, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective.
+
+      Now, by <a href="/content/generator_construction">this result</a>, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$.
 
   - property: regular subobject classifier
     proof: The indiscrete two-point space $\{0,1\}$ is a regular subobject classifier since continuous maps $X \to \{0,1\}$ correspond to subsets of $X$.
 
+  - property: infinitary extensive
+    proof: 'This can be deduced from the infinitary extensivity of <a href="/category/Set">$\Set$</a> as follows. We already know that coproducts and pullbacks exist, and these are preserved by the forgetful functor to $\Set$. More concretely, coproducts are disjoint unions of the underlying sets whose open subsets are unions of open subsets of the summands. Since coproducts are disjoint in $\Set$ and the empty set has a unique topology, it follows immediately that coproducts are disjoint in $\Top$ as well. It remains to show that coproducts are stable under pullbacks. Let $(X_i)_{i \in I}$ be a family of topological spaces and let $f : T \to \coprod_{i \in I} X_i$ be a continuous map. Consider the pullbacks $T_i := f^*(X_i)$. These are just the preimages of $X_i$ under $f$, with the topology induced from $T$. Since coproducts in $\Set$ are stable under pullbacks, the canonical continuous map $\coprod_{i \in I} T_i \to T$ is bijective. It remains to show that it is an open map. By the concrete description of open subsets in the disjoint union, it suffices to prove that each $T_i \to T$ is an open map. But this is the inclusion of a subspace, which is open since $X_i$ is open in $\coprod_{i \in I} X_i$.'
+
   - property: coregular
     proof: The category has all limits and colimits, and the regular monomorphisms are the subspace inclusions. Thus, it suffices to prove that subspace inclusions are stable under pushouts. For a proof see e.g. Lemma 3.6 at the <a href="https://ncatlab.org/nlab/show/subspace+topology#pushout" target="_blank">nLab</a>. Another proof can be found in <a href="https://math.stackexchange.com/a/2044509">MSE/2016945</a>.
 
-  - property: filtered-colimit-stable monomorphisms
-    proof: This follows from Lemma 2 <a href="/content/subcategories">here</a> applied to the forgetful functor to $\Set$.
-
-  - property: extremal cogenerator
-    proof: >-
-      Using the dual of Lemma 9 <a href="/content/subcategories">here</a> with $U : \Top \to \Set$ the forgetful functor whose right adjoint is the indiscrete topology functor, and the fact that the two-element set is a cogenerator of <a href="/category/Set">$\Set$</a>, we see that the indiscrete two-point space is a cogenerator of $\Top$. We claim that adding the Sierpinski space $S$ makes an extremal cogenerating set. To see this, let $f : X \to Y$ be a continuous function. First, $f$ inducing a bijection of maps to the indiscrete two-point space implies that $f$ is bijective on the underlying sets. Then, $f$ inducing a bijection of maps to the Sierpinski space implies that $f^* : \Open(Y) \to \Open(X)$ is also a bijection. We can then conclude that $f$ is open and therefore a homeomorphism: if $U \subseteq X$ is open, then there is an open subset $V \subseteq Y$ such that $f^*(V) = U$. Therefore, $f_*(U) = f_*(f^*(V)) = V$ is open, where in the last equality we use the fact that $f$ is surjective.
-
-      Now, by <a href="/content/generator_construction">this result</a>, we conclude that the product of the indiscrete two-point space and the Sierpinski space is an extremal cogenerator of $\Top$.
-
 unsatisfied_properties:
   - property: skeletal
     proof: This is trivial.
@@ -65,6 +67,9 @@ unsatisfied_properties:
     proof: If $X$ is a set, consider the discrete space $X_d$ on $X$ and the indiscrete space $X_i$ on $X$. The identity map $X \to X$ lifts to a continuous map $X_d \to X_i$, which is bijective and therefore both a mono- and an epimorphism, but it is not an isomorphism unless $X$ has at most one element.
     check_redundancy: false
 
+  - property: cofiltered-limit-stable epimorphisms
+    proof: We already know that <a href="/category/Set">$\Set$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the functor $\Set \to \Top$ which equips a set with the indiscrete topology.
+
   - property: cartesian filtered colimits
     proof: 'The functor $\IQ \times - : \Top \to \Top$ does not preserve sequential colimits, see <a href="https://math.stackexchange.com/questions/1255678" target="_blank">MSE/1255678</a>.'
 
@@ -77,9 +82,6 @@ unsatisfied_properties:
   - property: co-Malcev
     proof: 'See <a href="https://mathoverflow.net/questions/509548" target="_blank">MO/509548</a>. We can also phrase the proof as follows: Consider the forgetful functor $U : \Top \to \Set$ and the relation $R \subseteq U^2$ defined by $R(X) \coloneqq \{(x,y) \in U(X)^2 : x \in \overline{\{y\}} \}$. Both are representable: $U$ by the singleton and $R$ by the Sierpinski space. It is clear that $R$ is reflexive, but not symmetric.'
 
-  - property: cofiltered-limit-stable epimorphisms
-    proof: We already know that <a href="/category/Set">$\Set$</a> does not have this property. Now apply the contrapositive of the dual of Lemma 2 <a href="/content/subcategories">here</a> to the functor $\Set \to \Top$ which equips a set with the indiscrete topology.
-
   - property: effective cocongruences
     proof: 'Consider the indiscrete topological space $I$ on two points. This represents the functor which takes a topological space $X$ to the pairs of indistinguishable points of $X$. Therefore, we get a cocongruence $1 \rightrightarrows I$, where the maps are the two possible functions. However, this cannot be effective: if we have $h : Z\to 1$ which equalizes the two maps, then $Z$ must be empty. But that means the cokernel pair of $h$ is the discrete space on two points.'