diff --git a/database/data/001_categories/002_analysis.sql b/database/data/001_categories/002_analysis.sql index d598c8d3..425dfb3e 100644 --- a/database/data/001_categories/002_analysis.sql +++ b/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', diff --git a/database/data/001_categories/100_related-categories.sql b/database/data/001_categories/100_related-categories.sql index 09a3d7c8..553e8ffd 100644 --- a/database/data/001_categories/100_related-categories.sql +++ b/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'), diff --git a/database/data/002_tags/002_category-tags.sql b/database/data/002_tags/002_category-tags.sql index e71ce633..9f784853 100644 --- a/database/data/002_tags/002_category-tags.sql +++ b/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'), diff --git a/database/data/004_property-assignments/Met.sql b/database/data/004_property-assignments/Met.sql index 9536df23..fcf2ab76 100644 --- a/database/data/004_property-assignments/Met.sql +++ b/database/data/004_property-assignments/Met.sql @@ -39,19 +39,19 @@ VALUES 'Met', 'coequalizers', TRUE, - 'See MO/123739.' + 'This is because the category of pseudo-metric spaces 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 category of pseudo-metric spaces 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', diff --git a/database/data/004_property-assignments/Met_oo.sql b/database/data/004_property-assignments/Met_oo.sql index bb97a1ed..79cd4b3d 100644 --- a/database/data/004_property-assignments/Met_oo.sql +++ b/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', diff --git a/database/data/004_property-assignments/PMet.sql b/database/data/004_property-assignments/PMet.sql new file mode 100644 index 00000000..3756102e --- /dev/null +++ b/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 MO/123739.' +), +( + '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 it has exact filtered colimits.' +), +( + '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 MSE/5131457.' +), +( + '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 MSE/1778408 (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 +

$1 \xrightarrow{z} N \xleftarrow{s} N$

+ is a coproduct cocone by Johnstone, 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 MSE/1778408.' +); diff --git a/database/data/006_special-objects/002_initial_objects.sql b/database/data/006_special-objects/002_initial_objects.sql index 9a4713f5..eb8408ed 100644 --- a/database/data/006_special-objects/002_initial_objects.sql +++ b/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'), diff --git a/database/data/006_special-objects/003_terminal_objects.sql b/database/data/006_special-objects/003_terminal_objects.sql index c51d167a..360ce6cd 100644 --- a/database/data/006_special-objects/003_terminal_objects.sql +++ b/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'), diff --git a/database/data/006_special-objects/005_products.sql b/database/data/006_special-objects/005_products.sql index 5829f599..9a985208 100644 --- a/database/data/006_special-objects/005_products.sql +++ b/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$'); diff --git a/database/data/007_special-morphisms/002_isomorphisms.sql b/database/data/007_special-morphisms/002_isomorphisms.sql index 2824f322..2a0831d6 100644 --- a/database/data/007_special-morphisms/002_isomorphisms.sql +++ b/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', diff --git a/database/data/007_special-morphisms/003_monomorphisms.sql b/database/data/007_special-morphisms/003_monomorphisms.sql index 6e6a0586..b018c8ea 100644 --- a/database/data/007_special-morphisms/003_monomorphisms.sql +++ b/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', diff --git a/database/data/007_special-morphisms/004_epimorphisms.sql b/database/data/007_special-morphisms/004_epimorphisms.sql index fe1b3d5b..54e162c7 100644 --- a/database/data/007_special-morphisms/004_epimorphisms.sql +++ b/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',