assign first properties to semi-normed vector spaces

Author: ScriptRaccoon

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

@@ -25,7 +25,7 @@ VALUES
 	'$\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$. The choice of morphisms is similar to that of $\mathbf{PMet}$ which yields better categorical properties than continuous linear maps.',
+	'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)$. The choice of morphisms is similar to that of $\mathbf{PMet}$ which yields better categorical properties than continuous linear maps.',
 	NULL,
 	NULL
 ),

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