The category of metric spaces has no regular subobject classifier

database/data/categories/Met.yaml

@@ -33,7 +33,7 @@ satisfied_properties:
     check_redundancy: false
 
   - property: terminal object
-    proof: The one-point metric space is terminal.
+    proof: The one-point metric space $\{\ast\}$ is terminal.
     check_redundancy: false
 
   - property: coequalizers
@@ -165,6 +165,13 @@ unsatisfied_properties:
     references:
       - pmet_not_regular
 
+  - property: regular subobject classifier
+    proof: >-
+      Assume that $\top : 1 \to \Omega$ is a regular subobject classifier. We can identify $\top$ with a point $\top \in \Omega$, and for every regular monomorphism $Y \hookrightarrow X$ there is a unique non-expansive map $f : X \to \Omega$ such that $f^*(\{\top\}) = Y$ as metric spaces, and hence as topological spaces.
+
+      The underlying set of $\Omega$ is identified with $\Hom(1,\Omega) \cong \Sub_{\reg}(1)$. There are two regular subobjects of $1 = \{\ast\}$, namely $\{\ast\} \subseteq \{\ast\}$ and $\varnothing \subseteq \{\ast\}$ (the latter being the equalizer of, say, two maps $\{\ast\} \rightrightarrows \{0,1\}$). Thus, $\Omega$ has exactly two points and is therefore discrete. In particular, $\top : 1 \to \Omega$ is a clopen inclusion. The universal property then implies that every regular monomorphism is a clopen inclusion. But this is not the case: for example, the inclusion $[0,\infty) \hookrightarrow \IR$ is the equalizer of $\id : \IR \to \IR$ and the absolute value function $|{-}| : \IR \to \IR$, where $\IR$ is equipped with the standard metric.
+    label: Met_no_regular_subobject_classifier
+
 special_objects:
   initial object:
     description: empty metric space

database/data/categories/Met_oo.yaml

@@ -75,6 +75,11 @@ unsatisfied_properties:
     references:
       - pmet_not_regular
 
+  - property: regular subobject classifier
+    proof: The same proof as for <a href="/category/Met">$\Met$</a> works.
+    references:
+      - Met_no_regular_subobject_classifier
+
 special_objects:
   initial object:
     description: empty metric space

database/data/categories/PMet.yaml

@@ -37,7 +37,7 @@ satisfied_properties:
     check_redundancy: false
 
   - property: terminal object
-    proof: The one-point (pseudo-)metric space is terminal.
+    proof: The one-point (pseudo-)metric space $\{\ast\}$ is terminal.
     check_redundancy: false
 
   - property: coequalizers
@@ -55,6 +55,12 @@ satisfied_properties:
     references:
       - met_aleph1_cofiltered_limits
 
+  - property: regular subobject classifier
+    proof: >-
+      Consider the pseudo-metric space $\Omega = (\{0,1\},0)$, equipped with the zero pseudo-metric. We know that the regular monomorphisms are precisely the injective isometric maps (see below), and hence are, up to isomorphism, inclusions of isometric subspaces. In particular, the map $\top : \{\ast\} \to \Omega$, $\ast \mapsto 1$, is a regular monomorphism. If $Y \subseteq X$ is an isometric subspace, its characteristic function $\chi_Y : X \to \Omega$ is non-expansive for trivial reasons and satisfies $X \times_{\Omega} \{\ast\} = Y$. Indeed, the underlying set of the pullback $X \times_{\Omega} \{\ast\}$ identifies with the preimage $(\chi_Y)^*(\{1\}) = Y$, and the metric on the pullback is
+      $d((x,\ast),(x',\ast)) = \sup(d(x,x'),d(\ast,\ast)) = d(x,x')$,
+      i.e. the metric induced from $X$.
+
   - property: extremal generator
     proof: >-
       The proof will be similar to the one for <a href="/category/Met">$\Met$</a>. Namely, let $G$ be the set $\IR_{\ge 0} \sqcup \{ 0' \}$, equipped with the metric where $d(x,y) = 0$ if $x=y$ and otherwise $d(x,y) = x+y$ for $x, y \in \IR_{\ge 0}$, and $d(x, 0') = d(0', x) = x$ for $x \in \IR_{\ge 0}$. We will show $G$ is an extremal generator for $\PMet$.
@@ -98,9 +104,6 @@ unsatisfied_properties:
   - property: balanced
     proof: 'Let $d : \IR \times \IR \to \IR_{\geq 0}$ be the usual Euclidean metric on $\IR$ and $0 : \IR \times \IR \to \IR_{\geq 0}$ be the zero pseudo-metric. Then the identity map $(\IR,d) \to (\IR,0)$ provides a counterexample.'
 
-  - property: Malcev
-    proof: Take any counterexample in <a href="/category/Set">$\Set$</a> and equip it with the zero pseudo-metric.
-
   - property: cartesian closed
     proof: This is proven in <a href="https://math.stackexchange.com/questions/5131457" target="_blank">MSE/5131457</a>.
 
@@ -140,6 +143,9 @@ special_morphisms:
   epimorphisms:
     description: surjective non-expansive maps
     proof: 'Let $f : X \to Y$ be a non-expansive map that is not surjective. Choose $y_0 \in Y \setminus f(X)$. We extend the pseudo-metric from $Y$ to $Z \coloneqq Y \sqcup \{y''_0\}$ via $d(y,y''_0) \coloneqq d(y,y_0)$, i.e., we make $y_0,y''_0$ indistinguishable. Let $g : Y \to Z$ be the inclusion and $h : Y \to Z$ be the map that composes $g$ with the swap between $y_0$ and $y''_0$. Both are isometric and satisfy $g \circ f = h \circ f$. Therefore, $f$ is not an epimorphism.'
+  regular monomorphisms:
+    description: injective isometric maps
+    proof: 'Equalizers are injective isometric maps by construction. Conversely, if $X \hookrightarrow Y$ is an injective isometric map, we may assume without loss of generality that it is the inclusion of an isometric subspace. Then it is the equalizer of the two non-expansive maps $\chi_X, 1 : Y \rightrightarrows \Omega$, where $\Omega = (\{0,1\},0)$ is equipped with the zero pseudo-metric.'
   regular epimorphisms:
     description: 'surjective non-expansive maps $f : X \to Y$ with the property that for all $x,x'' \in X$, $d(p(x),p(x''))$ is the infimum of the sums $\sum_{i=0}^{n-1} d(y_i,x_{i+1})$, where $x=x_0$, $x_i \sim y_i$ for $0 \leq i \leq n$, and $y_n = x''$.'
     proof: This follows from the construction of the quotient pseudo-metric on $X/{\sim}$ in <a href="https://mathoverflow.net/questions/123739" target="_blank">MO/123739</a>.