determine special morphisms for pseudo-metric spaces

Author: ScriptRaccoon

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

@@ -71,6 +71,18 @@ VALUES
 	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',
 	'countable powers',

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

@@ -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',

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',