Add the category of pseudo-metric spaces

database/data/001_categories/002_analysis.sql

@@ -39,6 +39,16 @@ VALUES
 	'https://ncatlab.org/nlab/show/Met',
 	NULL
 ),
+(
+	'PMet',
+	'category of pseudo-metric spaces with non-expansive maps',
+	'$\mathbf{PMet}$',
+	'pseudo-metric spaces',
+	'non-expansive maps $f$, meaning $d(f(x),f(y)) \leq d(x,y)$ for all $x,y$',
+	'In contrast to metric spaces, we do not demand $d(x,y)=0 \implies x=y$ here.',
+	NULL,
+	NULL
+),
 (
 	'Met_oo',
 	'category of metric spaces with ∞ allowed',

database/data/001_categories/100_related-categories.sql

@@ -66,6 +66,7 @@ VALUES
 ('Met', 'Met_c'),
 ('Met', 'Met_oo'),
 ('Met', 'Ban'),
+('Met', 'PMet'),
 ('Met_c', 'Met'),
 ('Met_c', 'Met_oo'),
 ('Met_c', 'Top'),
@@ -80,6 +81,7 @@ VALUES
 ('N_oo', 'N'),
 ('N_oo', 'On'),
 ('On', 'N'),
+('PMet', 'Met'),
 ('Pos', 'FinOrd'),
 ('Pos', 'Prost'),
 ('Prost', 'Pos'),

database/data/002_tags/002_category-tags.sql

@@ -61,6 +61,7 @@ VALUES
 ('N_oo', 'thin'),
 ('On', 'set theory'),
 ('On', 'thin'),
+('PMet', 'analysis'),
 ('Pos', 'order theory'),
 ('Prost', 'order theory'),
 ('R-Mod', 'algebra'),

database/data/004_property-assignments/Met.sql

@@ -39,19 +39,19 @@ VALUES
 	'Met',
 	'coequalizers',
 	TRUE,
-	'See <a href="https://mathoverflow.net/questions/123739" target="_blank">MO/123739</a>.'
+	'This is because the <a href="/category/PMet">category of pseudo-metric spaces</a> has coequalizers and $\mathbf{Met} \hookrightarrow \mathbf{PMet}$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the coequalizer in the category of pseudo-metric spaces and then identify points with distance zero.' 
 ),
 (
 	'Met',
 	'directed colimits',
 	TRUE,
-	'Given a directed diagram $(X_i)$ of metric spaces, take the directed colimit $X$ of the underlying sets with the following metric: If $x,y \in X$, let $d(x,y)$ be infimum of all $d(x_i,y_i)$, where $x_i,y_i \in X_i$ are some preimages of $x,y$ in some $X_i$. This is only a pseudo-metric, so finally take the associated metric space (Kolmogorov quotient). The definition ensures that each $X_i \to X$ is non-expansive, and the universal property is easy to check.' 
+	'This is because the <a href="/category/PMet">category of pseudo-metric spaces</a> has directed colimits and $\mathbf{Met} \hookrightarrow \mathbf{PMet}$ has a left adjoint, mapping a pseudo-metric space $X$ to $X /{\sim}$ where $x \sim y \iff d(x,y)=0$. Concretely, we take the directed colimit in the category of pseudo-metric spaces and then identify points with distance zero.' 
 ),
 (
 	'Met',
 	'cartesian filtered colimits',
 	TRUE,
-	'The canonical map $\mathrm{colim}_i  (X \times Y_i) \to X \times \mathrm{colim}_i Y_i$ is an isomorphism for directed diagrams $(Y_i)$: It is surjective by the concrete description of directed colimits. It is isometric because of the elementary observation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ for $r, s_i \in \mathbb{R}$, where $i \leq j \implies s_i \geq s_j$.'
+	'The canonical map $\mathrm{colim}_i (X \times Y_i) \to X \times \mathrm{colim}_i Y_i$ is an isomorphism for directed diagrams $(Y_i)$: It is surjective by the concrete description of directed colimits. It is isometric because of the elementary observation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ for $r, s_i \in \mathbb{R}$, where $i \leq j \implies s_i \geq s_j$.'
 ),
 (
 	'Met',
@@ -105,7 +105,7 @@ VALUES
 	'Met',
 	'balanced',
 	FALSE,
-	'The inclusion $\mathbb{Q} \hookrightarrow \mathbb{R}$ is a counterexample; it is an epimorphism since $\mathbb{Q}$ is dense in $\mathbb{R}$.'
+	'The inclusion $\mathbb{Q} \hookrightarrow \mathbb{R}$ is a counterexample; it is an epimorphism since $\mathbb{Q}$ is dense in $\mathbb{R}$. Alternatively, consider the identity map $(X,2d) \to (X,d)$ for any non-trivial metric space $(X,d)$.'
 ),
 (
 	'Met',

database/data/004_property-assignments/Met_oo.sql

@@ -51,7 +51,7 @@ VALUES
 	'Met_oo',
 	'balanced',
 	FALSE,
-	'The inclusion $\mathbb{Q} \hookrightarrow \mathbb{R}$ provides a counterexample.'
+	'The inclusion $\mathbb{Q} \hookrightarrow \mathbb{R}$ provides a counterexample. Alternatively, consider the identity map $(X,2d) \to (X,d)$ for any non-trivial metric space $(X,d)$.'
 ),
 (
 	'Met_oo',

database/data/004_property-assignments/PMet.sql

@@ -0,0 +1,141 @@
+INSERT INTO category_property_assignments (
+	category_id,
+	property_id,
+	is_satisfied,
+	reason
+)
+VALUES
+(
+	'PMet',
+	'locally small',
+	TRUE,
+	'There is a forgetful functor $\mathbf{PMet} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.'
+),
+(
+	'PMet',
+	'equalizers',
+	TRUE,
+	'Just restrict the pseudo-metric to the equalizer built from the sets.'
+),
+(
+	'PMet',
+	'binary products',
+	TRUE,
+	'The product of two pseudo-metric spaces $(X,d)$, $(Y,d)$ is $(X \times Y,d)$ with $d((x_1,y_1),(x_2,x_2)) := \sup(d(x_1,x_2),d(y_1,y_2))$.' 
+),
+(
+	'PMet',
+	'terminal object',
+	TRUE,
+	'The one-point (pseudo-)metric space is terminal.'
+),
+(
+	'PMet',
+	'coequalizers',
+	TRUE,
+	'See <a href="https://mathoverflow.net/questions/123739" target="_blank">MO/123739</a>.'
+),
+(
+	'PMet',
+	'directed colimits',
+	TRUE,
+	'Given a directed diagram $(X_i)$ of pseudo-metric spaces, take the directed colimit $X$ of the underlying sets with the following pseudo-metric: If $x,y \in X$, let $d(x,y)$ be infimum of all $d(x_i,y_i)$, where $x_i,y_i \in X_i$ are some preimages of $x,y$ in some $X_i$. The definition ensures that each $X_i \to X$ is non-expansive, and the universal property is easy to check.' 
+),
+(
+	'PMet',
+	'exact filtered colimits',
+	TRUE,
+	'Let $\mathcal{I}$ be a finite category and $\mathcal{J}$ be a small filtered category, w.l.o.g. a directed poset. Let $X : \mathcal{I} \times \mathcal{J} \to \mathbf{PMet}$ be a diagram. We need to show that the canonical map $\mathrm{colim}_{j \in \mathcal{J}} \lim_{i \in \mathcal{I}} X(i,j) \to \lim_{i \in \mathcal{I}} \mathrm{colim}_{j \in \mathcal{J}}  X(i,j)$ is an isomorphism. It is bijective since the forgetful functor to $\mathbf{Set}$ preserves finite limits and filtered colimits and since $\mathbf{Set}$ has exact filtered colimits. That the map is isometric can easily be reduced to the following lemma: If $d_{i,j} \in \mathbb{R}_{\geq 0}$ are numbers for $i \in \mathcal{I}$, $j \in \mathcal{J}$ with $j \leq k \implies d_{i,k} \leq d_{i,j}$, then $\inf_j \sup_i d_{i,j} = \sup_i \inf_j d_{i,j}$. This can be proven directly. Alternatively, use that the thin category $(\mathbb{R}_{\geq 0} \cup \{\infty\},\leq)$ is isomorphic to $([0,1],\leq)$, and we already know that <a href="/category/real_interval">it has exact filtered colimits</a>.'
+),
+(
+	'PMet',
+	'strict initial object',
+	TRUE,
+	'The empty (pseudo-)metric space is initial and clearly strict.'
+),
+(
+	'PMet',
+	'generator',
+	TRUE,
+	'The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\mathbf{PMet} \to \mathbf{Set}$.'
+),
+(
+	'PMet',
+	'cogenerator',
+	TRUE,
+	'The set $\{0,1\}$ equipped with the pseudo-metric $d(0,1)=0$ is a cogenerator since every map into is automatically non-expansive and since $\{0,1\}$ is a cogenerator in $\mathbf{Set}$.' 
+),
+(
+	'PMet',
+	'semi-strongly connected',
+	TRUE,
+	'Every non-empty pseudo-metric space is weakly terminal (by using constant maps).'
+),
+(
+	'PMet',
+	'well-powered',
+	TRUE,
+	'This follows since monomorphisms are injective (see below).'
+),
+(
+	'PMet',
+	'well-copowered',
+	TRUE,
+	'This follows since epimorphisms are surjective (see below).'
+),
+(
+	'PMet',
+	'balanced',
+	FALSE,
+	'Let $d : \mathbb{R} \times \mathbb{R} \to \mathbb{R}_{\geq 0}$ be the usual Euclidean metric on $\mathbb{R}$ and $0 : \mathbb{R} \times \mathbb{R} \to \mathbb{R}_{\geq 0}$ be the zero pseudo-metric. Then the identity map $(\mathbb{R},d) \to (\mathbb{R},0)$ provides a counterexample.'
+),
+(
+	'PMet',
+	'cartesian closed',
+	FALSE,
+	'This is proven in <a href="https://math.stackexchange.com/questions/5131457" target="_blank">MSE/5131457</a>.'
+),
+(
+	'PMet',
+	'countable powers',
+	FALSE,
+	'Assume that the power $P = \mathbb{R}^{\mathbb{N}}$ exists, where $\mathbb{R}$ has the usual (pseudo-)metric. Since the forgetful functor $\mathbf{PMet} \to \mathbf{Set}$ is representable, it preserves limits, powers in particular. Thus, we may assume that $P$ is the set of sequences of numbers and that the projections $p_n : P \to \mathbb{R}$ are given by $p_n(x) = x_n$. Now consider the sequences $x = (n)_n$ and $y = (0)_n$. Since each $p_n$ is non-expansive, we get $d(x,y) \geq d(p_n(x),p_n(y)) = d(n,0) = n$. But then $d(x,y) = \infty$, a contradiction.'
+),
+(
+	'PMet',
+	'binary copowers',
+	FALSE,
+	'The coproduct of two non-empty pseudo-metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a> (the proof also works for pseudo-metric spaces). For example, the copower $\mathbb{R} \sqcup \mathbb{R}$ does not exist. We only get coproducts when allowing $\infty$ as a distance.'
+),
+(
+	'PMet',
+	'strict terminal object',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'PMet',
+	'essentially small',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'PMet',
+	'skeletal',
+	FALSE,
+	'This is trivial.'
+),
+(
+	'PMet',
+	'Malcev',
+	FALSE,
+	'Take any counterexample in $\mathbf{Set}$ and equip it with the zero pseudo-metric.'
+),
+(
+	'PMet',
+	'natural numbers object',
+	FALSE,
+	'If $(N,z,s)$ is a natural numbers object in $\mathbf{PMet}$, then
+	<p>$1 \xrightarrow{z} N \xleftarrow{s} N$</p>
+	is a coproduct cocone by <a href="https://ncatlab.org/nlab/show/Sketches+of+an+Elephant" target="_blank">Johnstone</a>, Part A, Lemma 2.5.5. Since there is a map $1 \to N$, we have $N \neq \varnothing$. However, the coproduct of two non-empty pseudo-metric spaces does not exist, see <a href="https://math.stackexchange.com/questions/1778408" target="_blank">MSE/1778408</a>.'
+);

database/data/006_special-objects/002_initial_objects.sql

@@ -33,6 +33,7 @@ VALUES
 ('N', '$0$'),
 ('N_oo', '$0$'),
 ('On', '$0$'),
+('PMet', 'empty pseudo-metric space'),
 ('Pos', 'empty poset'),
 ('Prost', 'empty proset'),
 ('R-Mod', 'trivial module'),

database/data/006_special-objects/003_terminal_objects.sql

@@ -30,6 +30,7 @@ VALUES
 ('Met_oo', 'singleton space'),
 ('Mon', 'trivial monoid'),
 ('N_oo', '$\infty$'),
+('PMet', 'singleton space'),
 ('Pos', 'singleton poset'),
 ('Prost', 'singleton proset'),
 ('R-Mod', 'zero module'),

database/data/006_special-objects/005_products.sql

@@ -61,6 +61,7 @@ VALUES
 ('FreeAb', '[finite case] direct sums'),
 ('Met_c', '[countable case] In the finite case, take direct products with the metric $d(x,y) = \sup_i d_i(x_i,y_i)$, but other metrics such as $d(x,y) = \sum_i d_i(x_i,y_i)$ also work. In the countable case, one can assume $d_i \leq 1$ and then define $d(x,y) = \sum_i d_i(x,y) / 2^i$.'),
 ('Met', '[finite case] direct products with the metric $d(x,y) = \sup_i d_i(x_i,y_i)$'),
+('PMet', '[finite case] direct products with the pseudo-metric $d(x,y) = \sup_i d_i(x_i,y_i)$'),
 ('Sch', '[finite case] The idea is to use $\mathrm{Spec}(A) \times \mathrm{Spec}(B) = \mathrm{Spec}(A \otimes B)$ and then to glue affine pieces together. See EGA I, Chap. I, Thm. 3.2.1.'),
 ('Man', '[finite case] direct products $X \times Y$ with the product topology and the charts $\mathbb{R}^{n + m} = \mathbb{R}^n \times \mathbb{R}^m \cong U \times V \hookrightarrow X \times Y$ for charts $\mathbb{R}^n \cong U \hookrightarrow X$ and $\mathbb{R}^m \cong V \hookrightarrow Y$'),
 ('walking_span', '[binary case] $1 \times 2 = 0$, $x \times x = x$, $0 \times x = 0$');

database/data/007_special-morphisms/002_isomorphisms.sql

@@ -200,6 +200,11 @@ VALUES
 	'only the identities',
 	'This is true for every poset (regarded as a category).'
 ),
+(
+	'PMet',
+	'bijective isometries',
+	'This is easy.'
+),
 (
 	'Pos',
 	'bijective functions that are order-preserving and order-reflecting',

database/data/007_special-morphisms/003_monomorphisms.sql

@@ -88,7 +88,7 @@ VALUES
 (
 	'Delta',
 	'injective order-preserving maps',
-	'The non-trivial direction follows since the forgetful functor $\Delta \to \mathbf{Set}$ is representable (by $[0]$), hence preserves monomorphisms.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'FI',
@@ -108,12 +108,12 @@ VALUES
 (
 	'FinOrd',
 	'injective order-preserving maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'FinSet',
 	'injective maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Fld',
@@ -138,7 +138,7 @@ VALUES
 (
 	'Haus',
 	'injective continuous maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'M-Set',
@@ -148,27 +148,27 @@ VALUES
 (
 	'Man',
 	'injective smooth maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Meas',
 	'injective measurable maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Met',
 	'injective non-expansive maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Met_c',
 	'injective continuous maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Met_oo',
 	'injective non-expansive maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'CAlg(R)',
@@ -195,6 +195,11 @@ VALUES
 	'every morphism',
 	'It is a thin category.'
 ),
+(
+	'PMet',
+	'injective non-expansive maps',
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
+),
 (
 	'Pos',
 	'injective order-preserving functions',
@@ -248,7 +253,7 @@ VALUES
 (
 	'Setne',
 	'injective maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'SetxSet',
@@ -278,12 +283,12 @@ VALUES
 (
 	'Top',
 	'injective continuous maps',
-	'The same proof as for $\mathbf{Set}$ can be used.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
 ),
 (
 	'Top*',
 	'injective pointed continuous maps',
-	'For the non-trivial direction: The forgetful functor $\mathbf{Top}_* \to \mathbf{Set}$ is representable (take the discrete two-point space) and hence preserves monomorphisms.'
+	'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the discrete two-point space), hence preserves monomorphisms.'
 ),
 (
 	'Vect',

database/data/007_special-morphisms/004_epimorphisms.sql

@@ -180,6 +180,11 @@ VALUES
 	'every morphism',
 	'It is a thin category.'
 ),
+(
+	'PMet',
+	'surjective non-expansive maps',
+	'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 := Y \sqcup \{y''_0\}$ via $d(y,y''_0) := 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.'
+),
 (
 	'On',
 	'every morphism',