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..a21af240 --- /dev/null +++ b/database/data/categories/Unif.yaml @@ -0,0 +1,111 @@ +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, 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 + +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 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 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. + + - 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 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$. + + - property: extensive + proof: >- + 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 + 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 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 + 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 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 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. + + - 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 + 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.' 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}