show that Met and Met_oo do have cartesian filtered colimits

Author: ScriptRaccoon

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

@@ -47,6 +47,12 @@ VALUES
 	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.' 
 ),
+(
+	'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$.'
+),
 (
 	'Met',
 	'strict initial object',

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

@@ -23,6 +23,12 @@ VALUES
 	TRUE,
 	'Example 4.5 in <a href="https://arxiv.org/abs/1504.02660" target="_blank">this preprint</a>'
 ),
+(
+	'Met_oo',
+	'cartesian filtered colimits',
+	TRUE,
+	'We can use the same proof as for the <a href="/category/Met">category of metric spaces</a> since the equation $\inf_i \max(r, s_i) = \max(r, \inf_i s_i)$ also holds for for $r, s_i \in \mathbb{R} \cup \{\infty\}$.'
+),
 (
 	'Met_oo',
 	'infinitary extensive',