From 684e108a6935fec9fee121f3e1fb040f9b75132e Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Apr 2026 13:10:57 +0200 Subject: [PATCH 1/4] add NormVect and SemiNormVect --- .../data/001_categories/003_analysis.sql | 22 ++++++++++++++++++- .../001_categories/100_related-categories.sql | 12 +++++++++- .../data/001_categories/200_category-tags.sql | 2 ++ src/lib/server/macros.ts | 2 ++ 4 files changed, 36 insertions(+), 2 deletions(-) diff --git a/databases/catdat/data/001_categories/003_analysis.sql b/databases/catdat/data/001_categories/003_analysis.sql index 1084c019..b7008feb 100644 --- a/databases/catdat/data/001_categories/003_analysis.sql +++ b/databases/catdat/data/001_categories/003_analysis.sql @@ -15,10 +15,30 @@ VALUES '$\Ban$', 'Banach spaces over $\IC$', 'linear contractions, i.e. linear maps of norm $\leq 1$', - 'The choice of morphisms is similar to that of $\Met$ which yields better categorical properties.', + 'The choice of morphisms is similar to that of $\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', + '$\SemiNormVect$', + 'semi-normed vector spaces over $\IC$', + '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 $\PMet$ which yields better categorical properties than continuous linear maps.', + NULL, + NULL +), +( + 'NormVect', + 'category of normed vector spaces with linear contractions', + '$\NormVect$', + 'normed vector spaces over $\IC$', + 'linear contractions, i.e. linear maps $f$ with $|f(x)| \leq |x|$', + 'The choice of morphisms is similar to that of $\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 5fc756f0..d288e9e9 100644 --- a/databases/catdat/data/001_categories/100_related-categories.sql +++ b/databases/catdat/data/001_categories/100_related-categories.sql @@ -17,6 +17,7 @@ VALUES ('Alg(R)', 'R-Mod'), ('Alg(R)', 'Ring'), ('Ban','Met'), +('Ban','NormVect'), ('B', 'FI'), ('B', 'FS'), ('BG_c', 'BG_f'), @@ -75,7 +76,7 @@ VALUES ('Meas', 'Top'), ('Met', 'Met_c'), ('Met', 'Met_oo'), -('Met', 'Ban'), +('Met', 'NormVect'), ('Met', 'PMet'), ('Met_c', 'Met'), ('Met_c', 'Met_oo'), @@ -90,8 +91,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'), @@ -109,6 +115,9 @@ VALUES ('Rng', 'Ring'), ('Sch', 'LRS'), ('Sch', 'Z'), +('SemiNormVect', 'NormVect'), +('SemiNormVect', 'Vect'), +('SemiNormVect', 'PMet'), ('Set_c', 'Set'), ('Set_c', 'FinSet'), ('Set_f', 'Set'), @@ -145,6 +154,7 @@ VALUES ('TorsAb', 'FinAb'), ('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 f9d97dab..0d71c6b4 100644 --- a/databases/catdat/data/001_categories/200_category-tags.sql +++ b/databases/catdat/data/001_categories/200_category-tags.sql @@ -61,6 +61,7 @@ VALUES ('N', 'thin'), ('N_oo', 'number theory'), ('N_oo', 'thin'), +('NormVect', 'analysis'), ('On', 'set theory'), ('On', 'thin'), ('PMet', 'analysis'), @@ -74,6 +75,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/src/lib/server/macros.ts b/src/lib/server/macros.ts index ad50c81b..2c80b772 100644 --- a/src/lib/server/macros.ts +++ b/src/lib/server/macros.ts @@ -96,4 +96,6 @@ export const MACROS = { '\\RS': '\\mathbf{RS}', '\\CoAlg': '\\mathbf{CoAlg}', '\\Cone': '\\mathbf{Cone}', + '\\NormVect': '\\mathbf{NormVect}', + '\\SemiNormVect': '\\mathbf{SemiNormVect}', } From f6d20ec1b70021ab0fd3ad928d13526bb9a256d1 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Apr 2026 14:15:19 +0200 Subject: [PATCH 2/4] assign first properties to semi-normed vector spaces --- .../data/001_categories/003_analysis.sql | 2 +- .../003_category-property-assignments/Ban.sql | 8 +-- .../SemiNormVect.sql | 67 +++++++++++++++++++ .../002_initial_objects.sql | 1 + .../003_terminal_objects.sql | 1 + .../005_special-objects/004_coproducts.sql | 1 + .../data/005_special-objects/005_products.sql | 3 +- .../002_isomorphisms.sql | 5 ++ .../003_monomorphisms.sql | 5 ++ 9 files changed, 84 insertions(+), 9 deletions(-) create mode 100644 databases/catdat/data/003_category-property-assignments/SemiNormVect.sql diff --git a/databases/catdat/data/001_categories/003_analysis.sql b/databases/catdat/data/001_categories/003_analysis.sql index b7008feb..730e0897 100644 --- a/databases/catdat/data/001_categories/003_analysis.sql +++ b/databases/catdat/data/001_categories/003_analysis.sql @@ -25,7 +25,7 @@ VALUES '$\SemiNormVect$', 'semi-normed vector spaces over $\IC$', '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 $\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 $\PMet$ which yields better categorical properties than continuous linear maps.', NULL, NULL ), diff --git a/databases/catdat/data/003_category-property-assignments/Ban.sql b/databases/catdat/data/003_category-property-assignments/Ban.sql index 311fd649..e58f5986 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 $\Ban \to \Set$ and $\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..aabcf300 --- /dev/null +++ b/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 $\Vect$, which is locally small.' +), +( + 'SemiNormVect', + 'equalizers', + TRUE, + 'It suffices to take the equalizer in $\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 $(\IC,|{-}|)$ (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 $(\IC,0)$ is a cogenerator since $\IC$ is a cogenerator in $\Vect$.' +), +( + 'SemiNormVect', + 'balanced', + FALSE, + 'The linear map $\IC \to \IC$, $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 29b8868f..113f1cc8 100644 --- a/databases/catdat/data/005_special-objects/002_initial_objects.sql +++ b/databases/catdat/data/005_special-objects/002_initial_objects.sql @@ -44,6 +44,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 4f884101..ea1c370b 100644 --- a/databases/catdat/data/005_special-objects/003_terminal_objects.sql +++ b/databases/catdat/data/005_special-objects/003_terminal_objects.sql @@ -41,6 +41,7 @@ VALUES ('Ring', 'zero ring'), ('Rng', 'zero ring'), ('Sch', '$\Spec(\IZ)$'), +('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 dd74e850..a33b0b24 100644 --- a/databases/catdat/data/005_special-objects/004_coproducts.sql +++ b/databases/catdat/data/005_special-objects/004_coproducts.sql @@ -37,6 +37,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 92fcb6c4..42139a66 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'), @@ -33,6 +33,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 e7e9e090..37c535ef 100644 --- a/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/002_isomorphisms.sql @@ -250,6 +250,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 f143a1b2..7c909523 100644 --- a/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/003_monomorphisms.sql @@ -245,6 +245,11 @@ VALUES 'injective rng homomorphisms', 'This holds in every finitary algebraic category: the forgetful functor to $\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 : (\IC,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 : (\IC,|{-}|) \to (V,|{-}|)$, $1 \mapsto v$. Since $f \circ \lambda_v = 0$, we deduce $\lambda_v = 0$, and hence $v = 0$.' +), ( 'Set_c', 'injective maps', From 0d0ecf510f02e5f42687129139cbb62b6d00e4a4 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Apr 2026 20:39:38 +0200 Subject: [PATCH 3/4] describe epis for SemiNormVect --- databases/catdat/data/001_categories/003_analysis.sql | 3 ++- .../catdat/data/006_special-morphisms/004_epimorphisms.sql | 5 +++++ 2 files changed, 7 insertions(+), 1 deletion(-) diff --git a/databases/catdat/data/001_categories/003_analysis.sql b/databases/catdat/data/001_categories/003_analysis.sql index 730e0897..b72e3abc 100644 --- a/databases/catdat/data/001_categories/003_analysis.sql +++ b/databases/catdat/data/001_categories/003_analysis.sql @@ -25,7 +25,8 @@ VALUES '$\SemiNormVect$', 'semi-normed vector spaces over $\IC$', '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)$. The choice of morphisms is similar to that of $\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)$; and this construction yields a functor which is right adjoint to the forgetful functor $\SemiNormVect \to \Vect$. +
The choice of morphisms is similar to that of $\PMet$ which yields better categorical properties than continuous linear maps.', NULL, NULL ), diff --git a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql index 8e92bc6c..feb22f11 100644 --- a/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql +++ b/databases/catdat/data/006_special-morphisms/004_epimorphisms.sql @@ -231,6 +231,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 $\SemiNormVect \to \Vect$ has a right adjoint, hence preserves all colimits, and therefore preserves epimorphisms.' +), ( 'Set_c', 'surjective maps', From 1a19046ec0ab7d17088a57ee3239fc90599951c7 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Thu, 23 Apr 2026 20:43:08 +0200 Subject: [PATCH 4/4] decide CSP --- .../data/003_category-property-assignments/SemiNormVect.sql | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql b/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql index aabcf300..dc36c147 100644 --- a/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql +++ b/databases/catdat/data/003_category-property-assignments/SemiNormVect.sql @@ -53,6 +53,12 @@ VALUES TRUE, 'The object $(\IC,0)$ is a cogenerator since $\IC$ is a cogenerator in $\Vect$.' ), +( + 'SemiNormVect', + 'CSP', + FALSE, + 'This is immediate from the description of coproducts, products, and epimorphisms.' +), ( 'SemiNormVect', 'balanced',