diff --git a/databases/catdat/data/001_categories/003_analysis.sql b/databases/catdat/data/001_categories/003_analysis.sql index 425dfb3e..dfdacb78 100644 --- a/databases/catdat/data/001_categories/003_analysis.sql +++ b/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}$. +
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', diff --git a/databases/catdat/data/001_categories/100_related-categories.sql b/databases/catdat/data/001_categories/100_related-categories.sql index 9b6a96ca..581794db 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/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'), diff --git a/databases/catdat/data/001_categories/200_category-tags.sql b/databases/catdat/data/001_categories/200_category-tags.sql index 60b66093..6f75b106 100644 --- a/databases/catdat/data/001_categories/200_category-tags.sql +++ b/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'), diff --git a/databases/catdat/data/003_category-property-assignments/Ban.sql b/databases/catdat/data/003_category-property-assignments/Ban.sql index 38864102..ca66a64b 100644 --- a/databases/catdat/data/003_category-property-assignments/Ban.sql +++ b/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 MSE/5033161.' + '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', diff --git a/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql b/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql new file mode 100644 index 00000000..f88909b1 --- /dev/null +++ b/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.' +); \ No newline at end of file diff --git a/databases/catdat/data/005_special-objects/002_initial_objects.sql b/databases/catdat/data/005_special-objects/002_initial_objects.sql index 809a8680..ca8bbe9d 100644 --- a/databases/catdat/data/005_special-objects/002_initial_objects.sql +++ b/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'), diff --git a/databases/catdat/data/005_special-objects/003_terminal_objects.sql b/databases/catdat/data/005_special-objects/003_terminal_objects.sql index ea7e846b..172ce485 100644 --- a/databases/catdat/data/005_special-objects/003_terminal_objects.sql +++ b/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'), diff --git a/databases/catdat/data/005_special-objects/004_coproducts.sql b/databases/catdat/data/005_special-objects/004_coproducts.sql index 4bc13d0f..6fb9ae57 100644 --- a/databases/catdat/data/005_special-objects/004_coproducts.sql +++ b/databases/catdat/data/005_special-objects/004_coproducts.sql @@ -36,6 +36,7 @@ VALUES ('Ring', 'see MSE/625874'), ('Rng', 'see MSE/4975797'), ('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'), diff --git a/databases/catdat/data/005_special-objects/005_products.sql b/databases/catdat/data/005_special-objects/005_products.sql index ab6ae148..60ddd1f8 100644 --- a/databases/catdat/data/005_special-objects/005_products.sql +++ b/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'), diff --git a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql index 5cac6ec0..b4533015 100644 --- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql +++ b/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}$', diff --git a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql index fcf8ecfd..7f55873b 100644 --- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql +++ b/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', diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql index 0e00d7b5..41235247 100644 --- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql +++ b/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 MSE/350716.' ), +( + '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',