diff --git a/database/data/categories/Met.yaml b/database/data/categories/Met.yaml index 3415d557..6c2d1226 100644 --- a/database/data/categories/Met.yaml +++ b/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 diff --git a/database/data/categories/Met_oo.yaml b/database/data/categories/Met_oo.yaml index b394ac65..bdf90725 100644 --- a/database/data/categories/Met_oo.yaml +++ b/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 $\Met$ works. + references: + - Met_no_regular_subobject_classifier + special_objects: initial object: description: empty metric space diff --git a/database/data/categories/PMet.yaml b/database/data/categories/PMet.yaml index 4635ae69..0b7acab4 100644 --- a/database/data/categories/PMet.yaml +++ b/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 $\Met$. 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 $\Set$ and equip it with the zero pseudo-metric. - - property: cartesian closed proof: This is proven in MSE/5131457. @@ -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 MO/123739.