Skip to content

Commit 532801a

Browse files
ScriptRaccoonScriptRaccoon
committed
add category of pseudo-metric spaces
1 parent 54f2306 commit 532801a

File tree

7 files changed

+161
-0
lines changed

7 files changed

+161
-0
lines changed

‎database/data/001_categories/002_analysis.sql‎

Lines changed: 10 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -39,6 +39,16 @@ VALUES
3939
'https://ncatlab.org/nlab/show/Met',
4040
NULL
4141
),
42+
(
43+
'PMet',
44+
'category of pseudo-metric spaces with non-expansive maps',
45+
'$\mathbf{PMet}$',
46+
'pseudo-metric spaces',
47+
'non-expansive maps $f$, meaning $d(f(x),f(y)) \leq d(x,y)$ for all $x,y$',
48+
'In contrast to metric spaces, we do not demand $d(x,y)=0 \implies x=y$ here.',
49+
NULL,
50+
NULL
51+
),
4252
(
4353
'Met_oo',
4454
'category of metric spaces with ∞ allowed',

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

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -66,6 +66,7 @@ VALUES
6666
('Met', 'Met_c'),
6767
('Met', 'Met_oo'),
6868
('Met', 'Ban'),
69+
('Met', 'PMet'),
6970
('Met_c', 'Met'),
7071
('Met_c', 'Met_oo'),
7172
('Met_c', 'Top'),
@@ -80,6 +81,7 @@ VALUES
8081
('N_oo', 'N'),
8182
('N_oo', 'On'),
8283
('On', 'N'),
84+
('PMet', 'Met'),
8385
('Pos', 'FinOrd'),
8486
('Pos', 'Prost'),
8587
('Prost', 'Pos'),

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

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -61,6 +61,7 @@ VALUES
6161
('N_oo', 'thin'),
6262
('On', 'set theory'),
6363
('On', 'thin'),
64+
('PMet', 'analysis'),
6465
('Pos', 'order theory'),
6566
('Prost', 'order theory'),
6667
('R-Mod', 'algebra'),

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

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
INSERT INTO category_property_assignments (
2+
category_id,
3+
property_id,
4+
is_satisfied,
5+
reason
6+
)
7+
VALUES
8+
(
9+
'PMet',
10+
'locally small',
11+
TRUE,
12+
'There is a forgetful functor $\mathbf{PMet} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.'
13+
),
14+
(
15+
'PMet',
16+
'equalizers',
17+
TRUE,
18+
'Just restrict the pseudo-metric to the equalizer built from the sets.'
19+
),
20+
(
21+
'PMet',
22+
'binary products',
23+
TRUE,
24+
'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))$.'
25+
),
26+
(
27+
'PMet',
28+
'terminal object',
29+
TRUE,
30+
'The one-point (pseudo-)metric space is terminal.'
31+
),
32+
(
33+
'PMet',
34+
'coequalizers',
35+
TRUE,
36+
'See <a href="https://mathoverflow.net/questions/123739" target="_blank">MO/123739</a>.'
37+
),
38+
(
39+
'PMet',
40+
'directed colimits',
41+
TRUE,
42+
'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.'
43+
),
44+
(
45+
'PMet',
46+
'cartesian filtered colimits',
47+
TRUE,
48+
'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 bijective by the concrete description of directed colimits and since $\mathbf{Set}$ has cartesian filtered 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$.'
49+
),
50+
(
51+
'PMet',
52+
'strict initial object',
53+
TRUE,
54+
'The empty (pseudo-)metric space is initial and clearly strict.'
55+
),
56+
(
57+
'PMet',
58+
'generator',
59+
TRUE,
60+
'The one-point (pseudo-)metric space is a generator since it represents the forgetful functor $\mathbf{Met} \to \mathbf{Set}$.'
61+
),
62+
(
63+
'PMet',
64+
'cogenerator',
65+
TRUE,
66+
'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}$.'
67+
),
68+
(
69+
'PMet',
70+
'semi-strongly connected',
71+
TRUE,
72+
'Every non-empty pseudo-metric space is weakly terminal (by using constant maps).'
73+
),
74+
(
75+
'PMet',
76+
'well-powered',
77+
TRUE,
78+
'This follows since monomorphisms are injective (see below).'
79+
),
80+
(
81+
'PMet',
82+
'well-copowered',
83+
TRUE,
84+
'This follows since epimorphisms are surjective (see below).'
85+
),
86+
(
87+
'PMet',
88+
'balanced',
89+
FALSE,
90+
'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.'
91+
),
92+
(
93+
'PMet',
94+
'cartesian closed',
95+
FALSE,
96+
'This is proven in <a href="https://math.stackexchange.com/questions/5131457" target="_blank">MSE/5131457</a>.'
97+
),
98+
(
99+
'PMet',
100+
'countable powers',
101+
FALSE,
102+
'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.'
103+
),
104+
(
105+
'PMet',
106+
'binary copowers',
107+
FALSE,
108+
'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.'
109+
),
110+
(
111+
'PMet',
112+
'strict terminal object',
113+
FALSE,
114+
'This is trivial.'
115+
),
116+
(
117+
'PMet',
118+
'essentially small',
119+
FALSE,
120+
'This is trivial.'
121+
),
122+
(
123+
'PMet',
124+
'skeletal',
125+
FALSE,
126+
'This is trivial.'
127+
),
128+
(
129+
'PMet',
130+
'Malcev',
131+
FALSE,
132+
'Take any counterexample in $\mathbf{Set}$ and equip it with the zero pseudo-metric.'
133+
);

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -200,6 +200,11 @@ VALUES
200200
'only the identities',
201201
'This is true for every poset (regarded as a category).'
202202
),
203+
(
204+
'PMet',
205+
'bijective isometries',
206+
'This is easy.'
207+
),
203208
(
204209
'Pos',
205210
'bijective functions that are order-preserving and order-reflecting',

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -195,6 +195,11 @@ VALUES
195195
'every morphism',
196196
'It is a thin category.'
197197
),
198+
(
199+
'PMet',
200+
'injective non-expansive maps',
201+
'For the non-trivial direction, the forgetful functor to $\mathbf{Set}$ is representable (by the terminal object), hence preserves monomorphisms.'
202+
),
198203
(
199204
'Pos',
200205
'injective order-preserving functions',

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

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -180,6 +180,11 @@ VALUES
180180
'every morphism',
181181
'It is a thin category.'
182182
),
183+
(
184+
'PMet',
185+
'surjective non-expansive maps',
186+
'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.'
187+
),
183188
(
184189
'On',
185190
'every morphism',

0 commit comments

Comments
 (0)