Add the categories of normed and semi-normed vector spaces

databases/catdat/data/001_categories/003_analysis.sql

@@ -14,11 +14,32 @@ VALUES
 	'category of Banach spaces with linear contractions',
 	'$\mathbf{Ban}$',
 	'Banach spaces over $\mathbb{C}$',
-	'linear contractions, i.e. linear maps of norm $\leq 1$',
-	'The choice of morphisms is similar to that of $\mathbf{Met}$ which yields better categorical properties.',
+	'linear contractions, i.e. linear maps $f$ with $|f(x)| \leq |x|$',
+	'The choice of morphisms is similar to that of $\mathbf{Met}$ which yields better categorical properties than continuous linear maps.',
 	'https://ncatlab.org/nlab/show/Banach+space',
 	NULL
 ),
+(
+	'SemiNormVect',
+	'category of semi-normed vector spaces with linear contractions',
+	'$\mathbf{SemiNormVect}$',
+	'semi-normed vector spaces over $\mathbb{C}$',
+	'linear contractions, i.e. linear maps $f$ with $|f(x)| \leq |x|$',
+	'In contrast to a norm, a semi-norm does not necessarily satisfy $|x|=0 \implies x=0$. In particular, every vector space $V$ yields a trivial semi-normed vector space $(V,0)$; and this construction yields a functor which is right adjoint to the forgetful functor $\mathbf{SemiNormVect} \to \mathbf{Vect}$.
+	<br>The choice of morphisms is similar to that of $\mathbf{PMet}$ which yields better categorical properties than continuous linear maps.',
+	NULL,
+	NULL
+),
+(
+	'NormVect',
+	'category of normed vector spaces with linear contractions',
+	'$\mathbf{NormVect}$',
+	'normed vector spaces over $\mathbb{C}$',
+	'linear contractions, i.e. linear maps $f$ with $|f(x)| \leq |x|$',
+	'The choice of morphisms is similar to that of $\mathbf{Met}$ which yields better categorical properties than continuous linear maps.',
+	NULL,
+	NULL
+),
 (
 	'Meas',
 	'category of measurable spaces',

databases/catdat/data/001_categories/100_related-categories.sql

@@ -14,6 +14,7 @@ VALUES
 ('Alg(R)', 'R-Mod'),
 ('Alg(R)', 'Ring'),
 ('Ban','Met'),
+('Ban','NormVect'),
 ('B', 'FI'),
 ('B', 'FS'),
 ('BG_c', 'BG_f'),
@@ -67,7 +68,7 @@ VALUES
 ('Meas', 'Top'),
 ('Met', 'Met_c'),
 ('Met', 'Met_oo'),
-('Met', 'Ban'),
+('Met', 'NormVect'),
 ('Met', 'PMet'),
 ('Met_c', 'Met'),
 ('Met_c', 'Met_oo'),
@@ -82,8 +83,13 @@ VALUES
 ('N', 'Z_div'),
 ('N_oo', 'N'),
 ('N_oo', 'On'),
+('NormVect', 'Ban'),
+('NormVect', 'SemiNormVect'),
+('NormVect', 'Vect'),
+('NormVect', 'Met'),
 ('On', 'N'),
 ('PMet', 'Met'),
+('PMet', 'SemiNormVect'),
 ('Pos', 'FinOrd'),
 ('Pos', 'Prost'),
 ('Prost', 'Pos'),
@@ -101,6 +107,9 @@ VALUES
 ('Rng', 'Ring'),
 ('Sch', 'LRS'),
 ('Sch', 'Z'),
+('SemiNormVect', 'NormVect'),
+('SemiNormVect', 'Vect'),
+('SemiNormVect', 'PMet'),
 ('Set_c', 'Set'),
 ('Set_c', 'FinSet'),
 ('Set_f', 'Set'),
@@ -131,6 +140,7 @@ VALUES
 ('Top*', 'Set*'),
 ('Vect', 'R-Mod'),
 ('Vect', 'R-Mod_div'),
+('Vect', 'NormVect'),
 ('Z', 'Sch'),
 ('Z', 'Set'),
 ('Z_div', 'N'),

databases/catdat/data/001_categories/200_category-tags.sql

@@ -59,6 +59,7 @@ VALUES
 ('N', 'thin'),
 ('N_oo', 'number theory'),
 ('N_oo', 'thin'),
+('NormVect', 'analysis'),
 ('On', 'set theory'),
 ('On', 'thin'),
 ('PMet', 'analysis'),
@@ -72,6 +73,7 @@ VALUES
 ('Ring', 'algebra'),
 ('Rng', 'algebra'),
 ('Sch', 'algebraic geometry'),
+('SemiNormVect', 'analysis'),
 ('Set_c', 'set theory'),
 ('Set_f', 'set theory'),
 ('Set', 'set theory'),

databases/catdat/data/003_category-property-assignments/Ban.sql

@@ -11,12 +11,6 @@ VALUES
 	TRUE,
 	'There is a forgetful functor $\mathbf{Ban} \to \mathbf{Set}$ and $\mathbf{Set}$ is locally small.' 
 ),
-(
-	'Ban',
-	'pointed',
-	TRUE,
-	'The trivial Banach space $\{0\}$ is a zero object.'
-),
 (
 	'Ban',
 	'locally ℵ₁-presentable',
@@ -69,7 +63,7 @@ VALUES
 	'Ban',
 	'unital',
 	FALSE,
-	'See <a href="https://math.stackexchange.com/questions/5033161" target="_blank">MSE/5033161</a>.'
+	'The canonical morphism $(V,|{-}|) \oplus (W,|{-}|) \to (V,|{-}|) \times (W,|{-}|)$ is given by the monomorphism $(V \times W, |{-}|_1) \hookrightarrow (V \times W, |{-}|_{\sup})$, which is proper since $|{-}|_{\sup} < |{-}|_1$ in general, hence is no strong epimorphism.'
 ),
 (
 	'Ban',

databases/catdat/data/003_category-property-assignments/SemiNormVect.sql

@@ -0,0 +1,73 @@
+INSERT INTO category_property_assignments (
+	category_id,
+	property_id,
+	is_satisfied,
+	reason
+)
+VALUES
+(
+    'SemiNormVect',
+    'locally small',
+    TRUE,
+    'There is a forgetful functor to $\mathbf{Vect}$, which is locally small.'
+),
+(
+    'SemiNormVect',
+    'equalizers',
+    TRUE,
+    'It suffices to take the equalizer in $\mathbf{Vect}$ and restrict the norm. The universal property is easy to verify.'
+),
+(
+    'SemiNormVect',
+    'products',
+    TRUE,
+    'The product of a family of semi-normed vector spaces $(V_i, |{-}|)_{i \in I}$ is the subspace of the product $\prod_{i \in I} V_i$ that consists of those tuples $v=(v_i)_{i \in I}$ such that $\sup_{i \in I} |v_i| < \infty$, equipped with the semi-norm $|v| := \sup_{i \in I} |v_i|$. The universal property is easy to verify.'
+),
+(
+    'SemiNormVect',
+    'coproducts',
+    TRUE,
+    'The coproduct of a family of semi-normed vector spaces $(V_i, |{-}|)_{i \in I}$ is the direct sum (i.e. coproduct) $\bigoplus_{i \in I} V_i$  equipped with the semi-norm $|v| := \sum_{i \in I} |v_i|$. The universal property is easy to verify: if $h : \bigoplus_{i \in I} V_i \to T$ is a linear map such that each $h|_{V_i}$ is a contraction, then $\textstyle |h(v)| = |\sum_i h(v_i)| \leq \sum_i |h(v_i)| \leq \sum_i |v_i| = |v|$.'
+),
+(
+    'SemiNormVect',
+    'coequalizers',
+    TRUE,
+    'By the usual argument it suffices to construct quotients by subspaces. If $(V,|{-}|)$ is a semi-normed vector space and $U \subseteq V$ is a subspace, endow the quotient vector space $V/U$ with the semi-norm $|\pi(v)| := \inf_{u \in U} |v + u|$. This is indeed a semi-norm and satisfies the universal property.'
+),
+(
+	'SemiNormVect',
+	'CIP',
+	TRUE,
+	'This is immediate from the concrete description of coproducts and products.'
+),
+(
+   'SemiNormVect',
+   'generator',
+   TRUE,
+   'Assume that $f,g : (V,|{-}|) \rightrightarrows (W,|{-}|)$ are morphisms that equalize all morphisms from $(\mathbb{C},|{-}|)$ (with the usual norm). This means that $f(v)=g(v)$ when $|v| \leq 1$, and we need to prove $f(v)=g(v)$ for every $v$. If $|v| = 0$, this is clear. Otherwise, consider $w := 1/|v| \cdot v$. Then $|w| \leq 1$, hence $f(w)=g(w)$, and this implies $f(v)=g(v)$.'
+),
+(
+   'SemiNormVect',
+   'cogenerator',
+   TRUE,
+   'The object $(\mathbb{C},0)$ is a cogenerator since $\mathbb{C}$ is a cogenerator in $\mathbf{Vect}$.'
+),
+(
+    'SemiNormVect',
+    'CSP',
+    FALSE,
+    'This is immediate from the description of coproducts, products, and epimorphisms.'
+),
+(
+	'SemiNormVect',
+	'balanced',
+	FALSE,
+	'The linear map $\mathbb{C} \to \mathbb{C}$, $x \mapsto x/2$ is a counterexample. It is bijective, hence a mono- and epimorphism, but not isometric and therefore no isomorphism.'
+),
+(
+    'SemiNormVect',
+    'unital',
+    FALSE,
+    'The canonical morphism $(V,|{-}|) \oplus (W,|{-}|) \to (V,|{-}|) \times (W,|{-}|)$ is given by the monomorphism $(V \times W, |{-}|_1) \hookrightarrow (V \times W, |{-}|_{\sup})$, which is proper since $|{-}|_{\sup} < |{-}|_1$ in general, hence is no strong epimorphism.'
+);

databases/catdat/data/005_special-objects/002_initial_objects.sql

@@ -43,6 +43,7 @@ VALUES
 ('Ring', 'ring of integers'),
 ('Rng', 'trivial ring'),
 ('Sch', 'empty scheme'),
+('SemiNormVect', 'trivial vector space with the unique semi-norm'),
 ('Set_c', 'empty set'),
 ('Set_f', 'empty set'),
 ('Set', 'empty set'),

databases/catdat/data/005_special-objects/003_terminal_objects.sql

@@ -40,6 +40,7 @@ VALUES
 ('Ring', 'zero ring'),
 ('Rng', 'zero ring'),
 ('Sch', '$\mathrm{Spec}(\mathbb{Z})$'),
+('SemiNormVect', 'trivial vector space with the unique semi-norm'),
 ('Set_c', 'singleton set'),
 ('Set', 'singleton set'),
 ('Set*', 'singleton pointed set'),

databases/catdat/data/005_special-objects/004_coproducts.sql

@@ -36,6 +36,7 @@ VALUES
 ('Ring', 'see <a href="https://math.stackexchange.com/questions/625874" target="_blank">MSE/625874</a>'),
 ('Rng', 'see <a href="https://math.stackexchange.com/questions/4975797" target="_blank">MSE/4975797</a>'),
 ('Sch', 'disjoint union with the product sheaf'),
+('SemiNormVect', 'The coproduct of a family of semi-normed spaces $(V_i,|{-}|)$ is the direct sum $\bigoplus_i V_i$ equipped with the semi-norm $|v| := \sum_i |v_i|$.'),
 ('Set', 'disjoint union'),
 ('Set*', 'wedge sum, aka one-point union'),
 ('SetxSet', 'component-wise disjoint union'),

databases/catdat/data/005_special-objects/005_products.sql

@@ -11,7 +11,7 @@ VALUES
 ('1', '$0 \times 0$'),
 ('Ab', 'direct products with pointwise operations'),
 ('Alg(R)', 'direct products with pointwise operations'),
-('Ban', 'direct products with the $\sup$-norm'),
+('Ban', 'The product of a family of Banach spaces $(B_i)$ is the subspace $\bigl\{x \in \prod_i B_i : \sup_i |x_i| < \infty\bigr\}$ equipped with the sup-norm $|x| := \sup_i |x_i|$.'),
 ('CAlg(R)', 'direct products with pointwise operations'),
 ('Cat', 'direct products with pointwise operations'),
 ('CMon', 'direct products with pointwise operations'),
@@ -32,6 +32,7 @@ VALUES
 ('Rel', 'disjoint unions (!)'),
 ('Ring', 'direct products with pointwise operations'),
 ('Rng', 'direct products with pointwise operations'),
+('SemiNormVect', 'The product of a family of semi-normed spaces $(V_i,|{-}|)$ is the subspace $\{v \in \prod_i V_i : \sup_i |v_i| < \infty\}$ equipped with the semi-norm $|v| := \sup_i |v_i|$.'),
 ('Set', 'direct products with pointwise operations'),
 ('Set*', 'direct products with pointwise operations'),
 ('Setne', 'direct products'),

databases/catdat/data/006_special-morphisms/002_isomorphisms.sql

@@ -245,6 +245,11 @@ VALUES
 	'bijective rng homomorphisms',
 	'This characterization holds in every algebraic category.'
 ),
+(
+	'SemiNormVect',
+	'bijective linear isometries',
+	'This is easy.'
+),
 (
 	'Sch',
 	'pairs $(f,f^{\sharp})$ consisting of a homeomorphism $f$ and an isomorphism of sheaves $f^{\sharp}$',

databases/catdat/data/006_special-morphisms/003_monomorphisms.sql

@@ -240,6 +240,11 @@ VALUES
 	'injective rng homomorphisms',
 	'This holds in every finitary algebraic category: the forgetful functor to $\mathbf{Set}$ is faithful, hence reflects monomorphisms, and it is continuous (even representable), hence preserves monomorphisms.'
 ),
+(
+	'SemiNormVect',
+	'injective linear contractions',
+	'For the non-trivial direction, let $f : (V,|{-}|) \to (W,|{-}|)$ be a monomorphism. Assume that $f(v)=0$. If $|v|=0$, then $v$ corresponds to a morphism $\rho_v : (\mathbb{C},0) \to (V,|{-}|)$, $1 \mapsto v$. Since $f \circ \rho_v = 0$, we deduce $\rho_v = 0$, and hence $v = 0$. Now assume that $|v| \neq 0$. We may then replace $v$ with $1/|v| \cdot v$ and assume that $|v| \leq 1$. Then $v$ corresponds to a morphism $\lambda_v : (\mathbb{C},|{-}|) \to (V,|{-}|)$, $1 \mapsto v$. Since $f \circ \lambda_v = 0$, we deduce $\lambda_v = 0$, and hence $v = 0$.'
+),
 (
 	'Set_c',
 	'injective maps',

databases/catdat/data/006_special-morphisms/004_epimorphisms.sql

@@ -226,6 +226,11 @@ VALUES
 	'A relation $R : A \to B$ is an epimorphism iff the map $R^* : P(B) \to P(A)$ defined by $S \mapsto \{a \in A : \exists \, b \in S: (a,b) \in R \}$ is injective.',
 	'See <a href="https://math.stackexchange.com/questions/350716/" target="_blank">MSE/350716</a>.'
 ),
+(
+	'SemiNormVect',
+	'surjective linear contractions',
+	'For the non-trivial direction, use that the forgetful functor $\mathbf{SemiNormVect} \to \mathbf{Vect}$ has a right adjoint, hence preserves all colimits, and therefore preserves epimorphisms.'
+),
 (
 	'Set_c',
 	'surjective maps',