From 21d5757451b74f7538df57298a246d6bd0c363bc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 19:29:59 +0200 Subject: [PATCH 01/11] add the category of uniform spaces; decide some first properties --- .cspell.json | 3 +- database/data/categories/Met_c.yaml | 1 + database/data/categories/Top.yaml | 1 + database/data/categories/Unif.yaml | 69 +++++++++++++++++++++++++++++ database/data/macros.yaml | 1 + 5 files changed, 74 insertions(+), 1 deletion(-) create mode 100644 database/data/categories/Unif.yaml diff --git a/.cspell.json b/.cspell.json index 94a0b930..45c57af4 100644 --- a/.cspell.json +++ b/.cspell.json @@ -19,7 +19,8 @@ "FiltVect", "networkidle", "devlog", - "cech" + "cech", + "Unif" ], "words": [ "abelian", diff --git a/database/data/categories/Met_c.yaml b/database/data/categories/Met_c.yaml index 4b457140..eddcfa80 100644 --- a/database/data/categories/Met_c.yaml +++ b/database/data/categories/Met_c.yaml @@ -14,6 +14,7 @@ related: - Met - Met_oo - Top + - Unif satisfied_properties: - property: locally small diff --git a/database/data/categories/Top.yaml b/database/data/categories/Top.yaml index 864ce08b..6407c46f 100644 --- a/database/data/categories/Top.yaml +++ b/database/data/categories/Top.yaml @@ -15,6 +15,7 @@ related: - Met_c - Top_* - Man + - Unif satisfied_properties: - property: locally small diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml new file mode 100644 index 00000000..deb2ccbb --- /dev/null +++ b/database/data/categories/Unif.yaml @@ -0,0 +1,69 @@ +id: Unif +name: category of uniform spaces +notation: $\Unif$ +objects: uniform spaces +morphisms: uniformly continuous maps +description: >- + A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations (called entourages) encoding the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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). +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. + # TODO: explain this better + + - property: cocomplete + proof: Take the colimit of the underlying sets and endow it with the finest uniform structure making all inclusions uniformly continuous. + # TODO: explain this better + + - 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$. + +unsatisfied_properties: + - property: skeletal + proof: This is trivial. + + - property: countably distributive + proof: The introduction to Cartesian-Closed Coreflective Subcategories of Uniform Spaces by Rice-Tashjian says that the canonical map $\coprod_{n \in \IN} [0,1] \to [0,1] \times \IN$ is not an isomorphism; this implies that $[0,1] \times -$ does not preserve countable coproducts. + # TODO: spell this out + + - property: pointed + proof: This is obvious. + + - 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. + +special_objects: + initial object: + description: empty set with the unique uniform structure + terminal object: + description: singleton set with the unique uniform structure + +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 in 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 $2$ with the indiscrete uniform structure (having only one entourage, $2 \times 2$). diff --git a/database/data/macros.yaml b/database/data/macros.yaml index bd497850..fd54b927 100644 --- a/database/data/macros.yaml +++ b/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} From c3e5ecdab1190c1e13d9d159b7e691c525fdb275 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 20:23:05 +0200 Subject: [PATCH 02/11] describe (co)products of uniform spaces; explain the proof that Unif is not countably distributive --- database/data/categories/Unif.yaml | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index deb2ccbb..f4151d70 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -41,21 +41,27 @@ unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: countably distributive - proof: The introduction to Cartesian-Closed Coreflective Subcategories of Uniform Spaces by Rice-Tashjian says that the canonical map $\coprod_{n \in \IN} [0,1] \to [0,1] \times \IN$ is not an isomorphism; this implies that $[0,1] \times -$ does not preserve countable coproducts. - # TODO: spell this out - - property: pointed proof: This is obvious. - 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. + - property: countably distributive + 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). It is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} 1$. We claim that the functor $[0,1] \times - : \Unif \to \Unif$ does not preserve this coproduct, which means that the canonical map + $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \IN,$$ + which is certainly bijective and uniformly continuous, is not 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 in $\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 in 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$. + 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: From 8b539abcfd5ab12075622b7494b66b46da665d37 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 20:32:42 +0200 Subject: [PATCH 03/11] Unif has no NNO --- database/data/categories/Unif.yaml | 18 +++++++++++------- 1 file changed, 11 insertions(+), 7 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index f4151d70..d82211be 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -37,21 +37,25 @@ satisfied_properties: - property: generator proof: The one-point uniform space is a generator since it represents the forgetful functor $\Unif \to \Set$. + # - property: distributive + # proof: TBA + unsatisfied_properties: - property: skeletal proof: This is trivial. - - property: pointed - proof: This is obvious. - - 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. - - property: countably distributive + - 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). It is isomorphic to the coproduct of one-point spaces $\coprod_{n \in \IN} 1$. We claim that the functor $[0,1] \times - : \Unif \to \Unif$ does not preserve this coproduct, which means that the canonical map - $$\textstyle\coprod_{n \in \IN} [0,1] \to [0,1] \times \IN,$$ - which is certainly bijective and uniformly continuous, is not 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 in $\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 in 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$. + 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 this result 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 in $\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 in 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$. special_objects: initial object: From 964f72132ae57ebb2b9392de7a4e58edd0a196b9 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 23:01:05 +0200 Subject: [PATCH 04/11] Unif is distributive and has disjoint coproducts --- database/data/categories/Unif.yaml | 19 +++++++++++++++++-- 1 file changed, 17 insertions(+), 2 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index d82211be..755a59eb 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -37,8 +37,23 @@ satisfied_properties: - property: generator proof: The one-point uniform space is a generator since it represents the forgetful functor $\Unif \to \Set$. - # - property: distributive - # proof: TBA + - property: distributive + proof: >- + We will adopt the usual abuse of notation and write a uniform space as $X$, while also denoting its underlying set by $X$. It is clear that $X \times \varnothing \cong \varnothing$ as uniform spaces, so it suffices to prove that $X \times -$ preserves binary coproducts. Let $Y,Z$ be two uniform spaces. The canonical uniformly continuous map + $$\alpha : (X \times Y) \sqcup (X \times Z) \to X \times (Y \sqcup Z)$$ + is bijective since $\Set$ is distributive and the forgetful functor $\Unif \to \Set$ preserves coproducts and products. It remains to show that $\alpha$ maps entourages to entourages. A basic entourage of the domain of $\alpha$ has the form + $$\begin{align*} + O & = (p_1 \times p_1)^*(U) \cap (p_2 \times p_2)^*(V) \\ + & \quad \sqcup (p_1 \times p_1)^*(U') \cap (p_2 \times p_2)^*(W) + \end{align*}$$ + for entourages $U,U'$ on $X$, an entourage $V$ on $Y$, and an entourage $W$ on $Z$. Then the image $(\alpha \times \alpha)_*(O)$ contains the basic entourage + $$(p_1 \times p_1)^*(U \cap U') \cap (p_2 \times p_2)^*(V \sqcup W)$$ + on $X \times (Y \sqcup Z)$ and is therefore an entourage as well. + + # TODO: decide if Unif is actually extensive + + - property: disjoint finite coproducts + proof: This follows easily from the corresponding property of $\Set$ and the fact that $\Unif$ has finite coproducts and pullbacks which are preserved by the forgetful functor (which is faithful and thus reflects monomorphisms), as well as the obvious fact that the uniform structure on the empty set is uniquely determined. unsatisfied_properties: - property: skeletal From 214abb3e797e6109dfe8f5b7c7cdcbddbac71e38 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 23:11:09 +0200 Subject: [PATCH 05/11] describe the cogenerator in Unif --- database/data/categories/Unif.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 755a59eb..97511a3d 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -37,6 +37,9 @@ satisfied_properties: - 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 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 $\Set$. + - property: distributive proof: >- We will adopt the usual abuse of notation and write a uniform space as $X$, while also denoting its underlying set by $X$. It is clear that $X \times \varnothing \cong \varnothing$ as uniform spaces, so it suffices to prove that $X \times -$ preserves binary coproducts. Let $Y,Z$ be two uniform spaces. The canonical uniformly continuous map From 8a757b31e40cf3f963464eb38a311ca544204d38 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 27 Jul 2026 23:27:51 +0200 Subject: [PATCH 06/11] describe regular monos in Unif --- database/data/categories/Unif.yaml | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 97511a3d..0b05193b 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -40,6 +40,9 @@ satisfied_properties: - property: cogenerator proof: The indiscrete 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 $\Set$. + - 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: distributive proof: >- We will adopt the usual abuse of notation and write a uniform space as $X$, while also denoting its underlying set by $X$. It is clear that $X \times \varnothing \cong \varnothing$ as uniform spaces, so it suffices to prove that $X \times -$ preserves binary coproducts. Let $Y,Z$ be two uniform spaces. The canonical uniformly continuous map @@ -94,4 +97,7 @@ special_morphisms: 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 $2$ with the indiscrete uniform structure (having only one entourage, $2 \times 2$). + 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 on $X$ is a preimage of an entourage on $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.' From 2a0b7cb40472eaa7cbbda5e328317ccbcc7c3ffc Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 28 Jul 2026 00:28:10 +0200 Subject: [PATCH 07/11] explain limits and colimits a bit more --- database/data/categories/Unif.yaml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 0b05193b..be23aa7b 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -4,7 +4,7 @@ notation: $\Unif$ objects: uniform spaces morphisms: uniformly continuous maps description: >- - A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations (called entourages) encoding the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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). + A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations (called entourages) encoding the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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 @@ -18,12 +18,11 @@ satisfied_properties: 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. - # TODO: explain this better + proof: 'Take the limit of the underlying sets and endow it with the coarsest uniform structure making all projections uniformly continuous; cf. Bourbaki, General Topology (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 on $X$.' - property: cocomplete - proof: Take the colimit of the underlying sets and endow it with the finest uniform structure making all inclusions uniformly continuous. - # TODO: explain this better + 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, Introduction to Uniform Spaces, 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. @@ -38,7 +37,7 @@ satisfied_properties: proof: The one-point uniform space is a generator since it represents the forgetful functor $\Unif \to \Set$. - property: cogenerator - proof: The indiscrete 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 $\Set$. + 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 $\Set$. - 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$. From 79be33b75f376bcc0709371a53acae994f15e80d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 28 Jul 2026 00:35:56 +0200 Subject: [PATCH 08/11] Unif has no stable epis --- database/data/categories/Unif.yaml | 3 +++ 1 file changed, 3 insertions(+) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index be23aa7b..23ccab8b 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -77,6 +77,9 @@ unsatisfied_properties: Choose any sequence of positive numbers $\varepsilon_n > 0$ converging to $0$. Then $\coprod_{n \in \IN} U_{\varepsilon_n}$ is an entourage in $\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 in 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 $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here 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. + special_objects: initial object: description: empty set with the unique uniform structure From b704d521e1d9ebc2b001c6f2903dfc10ada63b1d Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Tue, 28 Jul 2026 00:46:43 +0200 Subject: [PATCH 09/11] add sketch that Unif has no extremal generating set --- database/data/categories/Unif.yaml | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index 23ccab8b..f1ca10f8 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -80,6 +80,10 @@ unsatisfied_properties: - property: cofiltered-limit-stable epimorphisms proof: We already know that $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here 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 $\Top$, 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 From 9e55d78313df12c9d068dbfacc2456f6b039d6a2 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 30 Jul 2026 16:08:07 +0200 Subject: [PATCH 10/11] Unif is extensive --- database/data/categories/Unif.yaml | 45 ++++++++++++++++-------------- 1 file changed, 24 insertions(+), 21 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index f1ca10f8..f1a9ad29 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -4,7 +4,7 @@ notation: $\Unif$ objects: uniform spaces morphisms: uniformly continuous maps description: >- - A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations (called entourages) encoding the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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$. + A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations, called entourages, that satisfy certain properties and that encode the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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 @@ -18,7 +18,7 @@ satisfied_properties: 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, General Topology (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 on $X$.' + proof: 'Take the limit of the underlying sets and endow it with the coarsest uniform structure making all projections uniformly continuous; cf. Bourbaki, General Topology (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, Introduction to Uniform Spaces, Ch. 2.' @@ -42,23 +42,25 @@ satisfied_properties: - 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: distributive + - property: extensive proof: >- - We will adopt the usual abuse of notation and write a uniform space as $X$, while also denoting its underlying set by $X$. It is clear that $X \times \varnothing \cong \varnothing$ as uniform spaces, so it suffices to prove that $X \times -$ preserves binary coproducts. Let $Y,Z$ be two uniform spaces. The canonical uniformly continuous map - $$\alpha : (X \times Y) \sqcup (X \times Z) \to X \times (Y \sqcup Z)$$ - is bijective since $\Set$ is distributive and the forgetful functor $\Unif \to \Set$ preserves coproducts and products. It remains to show that $\alpha$ maps entourages to entourages. A basic entourage of the domain of $\alpha$ has the form - $$\begin{align*} - O & = (p_1 \times p_1)^*(U) \cap (p_2 \times p_2)^*(V) \\ - & \quad \sqcup (p_1 \times p_1)^*(U') \cap (p_2 \times p_2)^*(W) - \end{align*}$$ - for entourages $U,U'$ on $X$, an entourage $V$ on $Y$, and an entourage $W$ on $Z$. Then the image $(\alpha \times \alpha)_*(O)$ contains the basic entourage - $$(p_1 \times p_1)^*(U \cap U') \cap (p_2 \times p_2)^*(V \sqcup W)$$ - on $X \times (Y \sqcup Z)$ and is therefore an entourage as well. - - # TODO: decide if Unif is actually extensive - - - property: disjoint finite coproducts - proof: This follows easily from the corresponding property of $\Set$ and the fact that $\Unif$ has finite coproducts and pullbacks which are preserved by the forgetful functor (which is faithful and thus reflects monomorphisms), as well as the obvious fact that the uniform structure on the empty set is uniquely determined. + This can be deduced from the extensivity of $\Set$ 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 @@ -66,6 +68,7 @@ unsatisfied_properties: - 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: >- @@ -75,7 +78,7 @@ unsatisfied_properties: $$\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 in $\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 in 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$. + 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 $\Set$ does not have this property. Now apply the contrapositive of the dual of Lemma 2 here 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. @@ -96,7 +99,7 @@ special_objects: 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 in the codomain + 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 @@ -105,5 +108,5 @@ special_morphisms: 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 on $X$ is a preimage of an entourage on $Y$' + 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.' From 2aa2a4abf9ae78f00c1aa98c1ebe8300f1e791bb Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 30 Jul 2026 23:20:13 +0200 Subject: [PATCH 11/11] explain coequalizers in Unif concretely --- database/data/categories/Unif.yaml | 11 +++++------ 1 file changed, 5 insertions(+), 6 deletions(-) diff --git a/database/data/categories/Unif.yaml b/database/data/categories/Unif.yaml index f1a9ad29..a21af240 100644 --- a/database/data/categories/Unif.yaml +++ b/database/data/categories/Unif.yaml @@ -4,7 +4,7 @@ notation: $\Unif$ objects: uniform spaces morphisms: uniformly continuous maps description: >- - A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations, called entourages, that satisfy certain properties and that encode the property of two points being sufficiently close to each other. A uniformly continuous map (or simply: uniform map) $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$. + A uniform space $(X,\Phi)$ consists of a set $X$ and a uniform structure $\Phi$ on $X$, which is a set of binary relations, called entourages, that satisfy certain properties and that encode the property of two points being sufficiently close to each other. A uniformly continuous map or simply uniform map $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 @@ -18,11 +18,10 @@ satisfied_properties: 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, General Topology (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$.' + proof: 'Take the limit of the underlying sets and endow it with the coarsest uniform structure making all projections uniform; cf. Bourbaki, General Topology (Part 1), Chapter II, § 3, no. 3 on initial uniformities. In more concrete terms, products are described below on this page, and the equalizer of two uniform maps $f,g : (X,\Phi) \rightrightarrows (Y,\Psi)$ is the subset $E := \{x \in X : f(x) = g(x)\}$ equipped with the uniform structure $\{U \cap (E \times E) : U \in \Phi\}$.' - 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, Introduction to Uniform Spaces, Ch. 2.' - # TODO: explain coequalizers / quotients better. find better reference. + proof: 'Take the colimit of the underlying sets and endow it with the finest uniform structure making all inclusions uniform. More concretely, coproducts are described below on this page, and the coequalizer of two uniform maps $f,g : (X,\Phi) \rightrightarrows (Y,\Psi)$ is the $\Set$-based coequalizer $Q = Y / (f(x) \sim g(x))$ equipped with the following uniform structure, which makes the projection $p : Y \to Q$ uniform. Let $\Theta$ be the set of all subsets $U \subseteq Q \times Q$ such that $(p \times p)^*(U) \in \Psi$. It satisfies all the axioms of a uniform structure except one, namely the composition axiom. To fix this (and this construction works in complete generality), let $\Sigma \subseteq \Theta$ be the set of all $U \in \Theta$ for which there exists a sequence $U_1,U_2,\dotsc$ in $\Theta$ such that $U_1 \subseteq U$ and $U_{k+1} \circ U_{k+1} \subseteq U_k$ for all $k$. It is then straightforward to check that $\Sigma$ is a uniform structure on $Q$. Moreover, by construction, the map $p : (Y,\Psi) \to (Q,\Sigma)$ is uniform, and one verifies that it satisfies the required universal property.' - property: well-powered proof: This is clear from the classification of monomorphisms as injective continuous maps. @@ -37,7 +36,7 @@ satisfied_properties: 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 $\Set$. + 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 uniform and since $\{0,1\}$ is a cogenerator in $\Set$. - 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$. @@ -67,7 +66,7 @@ unsatisfied_properties: 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. + 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 uniform 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