Add the category of uniform spaces

.cspell.json

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

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,7 @@ related:
   - Met_c
   - Top_*
   - Man
+  - Unif
 
 satisfied_properties:
   - property: locally small

database/data/categories/Unif.yaml

@@ -0,0 +1,112 @@
+id: Unif
+name: category of uniform spaces
+notation: $\Unif$
+objects: uniform spaces
+morphisms: uniformly continuous maps
+description: >-
+  A <i>uniform space</i> $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations, called <i>entourages</i>, that satisfy certain properties and that encode the property of two points being sufficiently close to each other. A <i>uniformly continuous map</i> (or simply: <i>uniform map</i>) $f : (X,\Phi) \to (Y,\Psi)$ is a map $f : X \to Y$ such that for every $V \in \Psi$, we have $(f \times f)^*(V) = \{(x,x') \in X \times X : (f(x),f(x'))\} \in \Phi$. We do not assume uniform spaces to be separated (resp. Hausdorff). In particular, every pseudo-metric on $X$ induces a uniform structure on $X$.
+nlab_link: https://ncatlab.org/nlab/show/uniform+space
+tags:
+  - topology
+
+related:
+  - Top
+  - Met_c
+
+satisfied_properties:
+  - property: locally small
+    proof: There is a forgetful functor $\Unif \to \Set$ and $\Set$ is locally small.
+
+  - property: complete
+    proof: 'Take the limit of the underlying sets and endow it with the coarsest uniform structure making all projections uniformly continuous; cf. Bourbaki, <i>General Topology</i> (Part 1), Chapter II, § 3, no. 3 on initial uniformities. In more concrete terms, products are described below, and the equalizer of two uniformly continuous maps $f,g : X \rightrightarrows Y$ is the subset $E := \{x \in X : f(x) = g(x)\}$ whose entourages are precisely the sets $U \cap (E \times E)$, where $U$ is an entourage of $X$.'
+
+  - property: cocomplete
+    proof: 'Take the colimit of the underlying sets and endow it with the finest uniform structure making all inclusions uniformly continuous. In more concrete terms, coproducts are described below, and the coequalizer of two uniformly continuous maps $f,g : X \rightrightarrows Y$ is the $\Set$-based coequalizer $Q = Y / (f(x) \sim g(x))$ equipped with a certain uniform structure making the map $Y \to Q$ uniformly continuous. Unfortunately, in contrast to topological spaces, one cannot simply write down the entourages of $Q$, cf. James, <i>Introduction to Uniform Spaces</i>, Ch. 2.'
+    # TODO: explain coequalizers / quotients better. find better reference.
+
+  - property: well-powered
+    proof: This is clear from the classification of monomorphisms as injective continuous maps.
+
+  - property: well-copowered
+    proof: This is clear from the classification of epimorphisms as surjective continuous maps.
+
+  - property: semi-strongly connected
+    proof: Every non-empty uniform space is weakly terminal (by using constant maps).
+
+  - property: generator
+    proof: The one-point uniform space is a generator since it represents the forgetful functor $\Unif \to \Set$.
+
+  - property: cogenerator
+    proof: The indiscrete (aka trivial) uniform space $\{0,1\}$ (i.e. $\{0,1\} \times \{0,1\}$ is the only entourage) is a cogenerator because every map into $\{0,1\}$ is automatically uniformly continuous and since $\{0,1\}$ is a cogenerator in <a href="/category/Set">$\Set$</a>.
+
+  - 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: extensive
+    proof: >-
+      This can be deduced from the extensivity of <a href="/category/Set">$\Set$</a> as follows. We already know that coproducts and pullbacks exist and are preserved by the forgetful functor $\Unif \to \Set$. Moreover, the empty set carries a unique uniform structure. Since $\Set$ is extensive, it follows immediately that coproducts are disjoint in $\Unif$. It remains to show that finite coproducts are stable under pullbacks (we shall see later that countable coproducts are not, since the category is not countably distributive).
+
+      First, recall that if $A$ is a subset of a uniform space $X$ (we follow the common, albeit imprecise, abuse of notation of denoting a uniform space by the same symbol as its underlying set), then $A$ inherits a uniform structure by declaring the entourages of $A$ to be the sets of the form $U \cap (A \times A)$, where $U$ is an entourage of $X$. With this structure, $A$ is called a subspace of $X$. If $f : X \to Y$ is a uniform map and $A \subseteq Y$ is a subspace, then the subspace $f^*(A) \subseteq X$ is a pullback of the inclusion $A \hookrightarrow Y$ along $f$.
+
+      Now let $f : T \to X + Y$ be a uniform map. Notice that the inclusion maps $X \to X + Y \leftarrow Y$ are embeddings. Thus, we may regard $X$ and $Y$ as subspaces of $X + Y$. Consider the pullbacks $T_X$ and $T_Y$. These are subspaces of $T$, and there is a canonical uniform map $T_X + T_Y \to T$. Our task is to prove that it is an isomorphism of uniform spaces. It is certainly a bijection, since $\Set$ is extensive. It therefore remains to show that it maps entourages to entourages.
+
+      A basic entourage of $T_X \sqcup T_Y$ has the form
+      $$(U \cap (T_X \times T_X)) \sqcup (V \cap (T_Y \times T_Y))$$
+      for entourages $U$ and $V$ of $T$. Its image relation on $T$ is
+      $$(U \cap (T_X \times T_X)) \cup (V \cap (T_Y \times T_Y)),$$
+      and we need to show that this is an entourage of $T$. Since $f$ is uniform and
+      $$M := (X \times X) \sqcup (Y \times Y)$$
+      is an entourage of $X + Y$, its preimage
+      $$(f \times f)^*(M) = (T_X \times T_X) \cup (T_Y \times T_Y)$$
+      is an entourage of $T$. Since $U \cap V$ is also an entourage of $T$, and
+      $$(U \cap V) \cap \bigl((T_X \times T_X) \cup (T_Y \times T_Y)\bigr) \subseteq (U \cap (T_X \times T_X)) \cup (V \cap (T_Y \times T_Y)),$$
+      the claim follows.
+
+unsatisfied_properties:
+  - property: skeletal
+    proof: This is trivial.
+
+  - property: balanced
+    proof: If $X$ is a set, consider the discrete uniform space $X_d$ on $X$ (all reflexive relations are entourages) and the indiscrete space $X_i$ on $X$ (the relation $X \times X$ is the only entourage). The identity map $X \to X$ lifts to a uniformly 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: natural numbers object
+    proof: >-
+      We equip $[0,1]$ with the usual metric, which induces a uniform structure in the usual way: for $\varepsilon > 0$, we have the basic entourage $U_{\varepsilon} := \{(r,s) \in [0,1]^2 : |r-s| < \varepsilon\}$. We equip the set $\IN$ with the discrete uniform structure (i.e., every reflexive relation is an entourage). This uniform space is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} 1$.
+
+      If there was a natural numbers object, then by <a href="/content/nno_distributive_criterion">this result</a> the canonical map
+      $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \coprod_{n \in \IN} 1 \cong [0,1] \times \IN$$
+      would be a split monomorphism. It is certainly surjective and hence an epimorphism. Thus, it would be an isomorphism.
+
+      Choose any sequence of positive numbers $\varepsilon_n > 0$ converging to $0$. Then $\coprod_{n \in \IN} U_{\varepsilon_n}$ is an entourage of $\coprod_{n \in \IN} [0,1]$. Its image in $[0,1] \times \IN$ consists of all $((r,n),(s,m))$ such that $n=m$ and $|r-s| < \varepsilon_n$. Assume, for a contradiction, that this set is an entourage of the product. Then it contains $(p_1 \times p_1)^*(U_\delta) \cap (p_2 \times p_2)^*(\Delta_{\IN})$ for some $\delta > 0$. In other words, $|r-s| < \delta$ implies $|r-s| < \varepsilon_n$ for all $n \in \IN$ and $r,s \in [0,1]$. Taking $s=0$ and $r=\delta/2$, we see that the sequence $(\varepsilon_n)$ is bounded below by $\delta/2$, contradicting the assumption that it converges to $0$.
+
+  - 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 \Unif$ which equips a set $X$ with the indiscrete uniform structure having the only entourage $X \times X$. This functor is right adjoint to the forgetful functor and therefore preserves cofiltered limits.
+
+  - property: extremal generating set
+    proof: The proof is a minor variation of the proof for <a href="/category/Top">$\Top$</a>, using that compact Hausdorff spaces have a unique uniform structure.
+    # TODO: add details
+
+special_objects:
+  initial object:
+    description: empty set with the unique uniform structure
+  terminal object:
+    description: singleton set with the unique uniform structure
+  coproducts:
+    description: The coproduct of a family of uniform spaces $(X_i,\Phi_i)_{i \in I}$ is $(\coprod_{i \in I} X_i,\Phi)$, where $\Phi$ consists of all subsets that contain $\coprod_{i \in I} U_i$ for some family of entourages $U_i \in \Phi_i$ for $i \in I$.
+  products:
+    description: The product of a family of uniform spaces $(X_i,\Phi_i)_{i \in I}$ is $(\prod_{i \in I} X_i,\Phi)$, where $\Phi$ consists of all subsets that contain $\bigcap_{i \in F} (p_i \times p_i)^*(U_i)$ for some finite subset $F \subseteq I$ and some family of entourages $U_i \in \Phi_i$ for $i \in F$.
+
+special_morphisms:
+  isomorphisms:
+    description: uniform isomorphisms, i.e. bijective uniform maps whose inverse map is also uniform; equivalently, bijective maps such that a relation in the domain is an entourage if and only if its image is an entourage of the codomain
+    proof: This is easy.
+  monomorphisms:
+    description: injective uniform maps
+    proof: For the non-trivial direction, the forgetful functor to $\Set$ is representable (by the terminal object), hence preserves monomorphisms.
+  epimorphisms:
+    description: surjective uniform maps
+    proof: The proof works exactly as for the category of sets, where we endow $\{0,1\}$ with the indiscrete uniform structure (having only one entourage, $\{0,1\} \times \{0,1\}$).
+  regular monomorphisms:
+    description: 'A morphism $f : X \to Y$ is a regular monomorphism iff $f$ is a uniform embedding, meaning that every entourage of $X$ is a preimage of an entourage of $Y$'
+    proof: 'Equalizers are uniform embeddings by their construction. Conversely, if $f : X \to Y$ is an uniform embedding, then $f$ is the equalizer of the two characteristic maps $\chi_Y, \chi_{f(X)} : Y \to \{0,1\}$, where $\{0,1\}$ carries the indiscrete uniform structure.'

database/data/macros.yaml

@@ -97,6 +97,7 @@
 \Met: \mathbf{Met}
 \PMet: \mathbf{PMet}
 \Top: \mathbf{Top}
+\Unif: \mathbf{Unif}
 \Haus: \mathbf{Haus}
 \CompHaus: \mathbf{CompHaus}
 \sSet: \mathbf{sSet}