From 135dbbdb4524a27744c8454d0f3c7f52cbeda8ff Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 28 Jun 2026 05:02:14 +0200 Subject: [PATCH 1/7] Ban is not counital --- databases/catdat/data/categories/Ban.yaml | 3 +++ databases/catdat/data/category-properties/counital.yaml | 2 +- databases/catdat/data/category-properties/unital.yaml | 2 +- 3 files changed, 5 insertions(+), 2 deletions(-) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 92fef27f6..7823ced7c 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -51,6 +51,9 @@ unsatisfied_properties: - property: unital proof: See MSE/5033161. + - property: counital + proof: The canonical morphism $X \sqcup Y \to X \times Y$ is surjective, and therefore an epimorphism. Hence, if it were also a strong monomorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree. + - property: co-Malcev proof: See the comments to MO/509552. diff --git a/databases/catdat/data/category-properties/counital.yaml b/databases/catdat/data/category-properties/counital.yaml index b71b7cdbc..57e443b74 100644 --- a/databases/catdat/data/category-properties/counital.yaml +++ b/databases/catdat/data/category-properties/counital.yaml @@ -1,6 +1,6 @@ id: counital relation: is -description: 'A category is counital if its dual is unital, i.e., it has a zero object, finite colimits, and for all objects $X,Y$ the two morphisms $(\id_X;0) : X \sqcup Y \twoheadrightarrow X$ and $(0;\id_Y) : X \sqcup Y \twoheadrightarrow Y$ are jointly strongly monomorphic. When products exist, the canonical morphism $X \sqcup Y \to X \times Y$ therefore must be a strong monomorphism.' +description: 'A category is counital if its dual is unital, i.e., it has a zero object, finite colimits, and for all objects $X,Y$ the two morphisms $(\id_X;0) : X \sqcup Y \twoheadrightarrow X$ and $(0;\id_Y) : X \sqcup Y \twoheadrightarrow Y$ are jointly strongly monomorphic. When binary products exist, the canonical morphism $X \sqcup Y \to X \times Y$ therefore must be a strong monomorphism.' dual_property: unital invariant_under_equivalences: true diff --git a/databases/catdat/data/category-properties/unital.yaml b/databases/catdat/data/category-properties/unital.yaml index acd194b3d..43d75ea5c 100644 --- a/databases/catdat/data/category-properties/unital.yaml +++ b/databases/catdat/data/category-properties/unital.yaml @@ -1,6 +1,6 @@ id: unital relation: is -description: 'A category is unital if it has a zero object, finite limits, and for all objects $X,Y$ the two morphisms $(\id_X,0) : X \hookrightarrow X \times Y$ and $(0,\id_Y) : Y \hookrightarrow X \times Y$ are jointly strongly epimorphic. This means: there is no proper subobject of $X \times Y$ that contains $X$ and $Y$. When coproducts exist, the canonical morphism $X \sqcup Y \to X \times Y$ therefore must be a strong epimorphism.' +description: 'A category is unital if it has a zero object, finite limits, and for all objects $X,Y$ the two morphisms $(\id_X,0) : X \hookrightarrow X \times Y$ and $(0,\id_Y) : Y \hookrightarrow X \times Y$ are jointly strongly epimorphic. This means: there is no proper subobject of $X \times Y$ that contains $X$ and $Y$. When binary coproducts exist, the canonical morphism $X \sqcup Y \to X \times Y$ therefore must be a strong epimorphism.' nlab_link: https://ncatlab.org/nlab/show/unital+category dual_property: counital invariant_under_equivalences: true From d1ae8b58f50198c8cd9f924af1408802d5549300 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 28 Jun 2026 05:08:58 +0200 Subject: [PATCH 2/7] Ban is not unital: replace reference with direct proof --- databases/catdat/data/categories/Ban.yaml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 7823ced7c..11684d12a 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -49,7 +49,7 @@ unsatisfied_properties: proof: If $\Omega$ is a regular subobject classifier, then by the classification of regular monomorphisms, $\Hom(X,\Omega)$ is isomorphic to the set of closed subspaces of $X$ for any Banach space $X$. For $X = \IC$ this implies that there are exactly two vectors in $\Omega$ with norm $\leq 1$, which is absurd. (For $\Omega = 0$ there is just one, and for $\Omega \neq 0$ there are infinitely many.) - property: unital - proof: See MSE/5033161. + proof: The canonical morphism $X \sqcup Y \to X \times Y$ is injective, and therefore a monomorphism. Hence, if it were also a strong epimorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree. - property: counital proof: The canonical morphism $X \sqcup Y \to X \times Y$ is surjective, and therefore an epimorphism. Hence, if it were also a strong monomorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree. From 0ababb1185d384a24184534883587375460f4bca Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 28 Jun 2026 19:02:56 +0200 Subject: [PATCH 3/7] classify regular epis in Ban --- databases/catdat/data/categories/Ban.yaml | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 11684d12a..b23ada90b 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -86,3 +86,14 @@ special_morphisms: regular monomorphisms: description: closed embeddings proof: The non-trivial direction follows from the well-known fact that for every closed subspace of a Banach space its quotient space is again a Banach space. + regular epimorphisms: + description: >- + For a linear contraction $f : V \to W$ the following are equivalent: (1) $f$ is a regular epimorphism. (2) $f$ is surjective and the norm on $W$ is given by $|w| = \inf \{|v| : f(v) = w\}$. (3) $f$ is surjective and $f$ maps the open unit ball of $V$ onto the open unit ball of $W$. + proof: >- + (1) implies (2): This follows immediately from the concrete construction of coequalizers, and the quotient Banach space $V/U$ in particular. + + (2) implies (1): Let $U \coloneqq \ker(f)$. Then $U$ is a closed subspace of $V$, and $f$ induces a bijective linear contraction $\tilde{f} : V/U \to W$. It is isometric by assumption on $f$ and the definition of the norm on $V/U$. Thus, $\tilde{f}$ is an isomorphism. Since $V/U$ is the cokernel of $U \hookrightarrow V$, it follows that $f$ is a regular epimorphism. + + (2) implies (3): Let $w \in W$ be an element with $|w| < 1$. Since $|w|$ is the infimum of all $|v|$ with $f(v)=w$, there is some $v$ with $f(v)=w$ and $|v| < 1$. + + (3) implies (2): Let $w \in W$. Since $f$ is a linear contraction, the inequality $|w| \leq \inf \{|v| : f(v) = w\}$ holds. Let $\varepsilon > 0$. Consider $w' \coloneqq w / (|w| + \varepsilon)$. Then $|w'| < 1$. Thus, by assumption, there is some $v' \in V$ with $|v'| < 1$ and $f(v') =w'$. Let $v \coloneqq (|w| + \varepsilon) v'$. Then $f(v) = w$ and $|v| < |w| + \varepsilon$. Thus, the infimum in question is $\leq |w| + \varepsilon$, for every $\varepsilon > 0$, and hence $\leq |w|$. From 8bf1c14da93f42b29a3048b66f7b1663bbaf69b1 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Sun, 28 Jun 2026 19:12:57 +0200 Subject: [PATCH 4/7] Ban is regular --- databases/catdat/data/categories/Ban.yaml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index b23ada90b..7159cb081 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -35,6 +35,13 @@ satisfied_properties: - property: cocartesian cofiltered limits proof: 'If $X$ is a Banach space and $(Y_i)$ is a cofiltered diagram of Banach spaces, the canonical map $X \oplus \lim_i Y_i \to \lim_i (X \oplus Y_i)$ is an isomorphism: Since the forgetful functor $\Ban \to \Vect$ preserves finite coproducts and all limits, and $\Vect$ has the claimed property (see here), the canonical map is bijective. It remains to show that it is isometric. For $(x,y) \in X \oplus \lim_i Y_i$ the norm in the domain is $|x| + \sup_i |y_i|$, and the norm in the codomain is $\sup_i (|x| + |y_i|)$, and these clearly agree.' + - property: regular + proof: >- + It suffices to prove that regular epimorphisms are stable under pullbacks. We will use their classification below. + So let $f : V \to W$ be a regular epimorphism of Banach spaces and let $g : T \to W$ be any morphism. We need to show that the projection $V \times_W T \to T$ is a regular epimorphism. + Clearly, it is surjective since $f$ is surjective. Now let $t \in T$ be an element of norm $<1$. Since $g$ is a linear contraction, $g(t)$ has norm $<1$. Since $f$ is a regular epimorphism, there is some $v \in V$ with norm $<1$ and $f(v) = g(t)$. + Then $(v,t) \in V \times_W T$ has norm $\max(|v|,|t|) < 1$ and provides a preimage of $t$. + unsatisfied_properties: - property: skeletal proof: This is trivial. From ce17c759737a2650941c9b00133ce2f45dd04eb3 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 29 Jun 2026 06:45:04 +0200 Subject: [PATCH 5/7] adjust description of regular epis in Ban --- databases/catdat/data/categories/Ban.yaml | 10 ++++++---- 1 file changed, 6 insertions(+), 4 deletions(-) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 7159cb081..ae45e49d9 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -37,10 +37,10 @@ satisfied_properties: - property: regular proof: >- - It suffices to prove that regular epimorphisms are stable under pullbacks. We will use their classification below. + It suffices to prove that regular epimorphisms are stable under pullbacks. We will use their classification via open unit balls below. So let $f : V \to W$ be a regular epimorphism of Banach spaces and let $g : T \to W$ be any morphism. We need to show that the projection $V \times_W T \to T$ is a regular epimorphism. - Clearly, it is surjective since $f$ is surjective. Now let $t \in T$ be an element of norm $<1$. Since $g$ is a linear contraction, $g(t)$ has norm $<1$. Since $f$ is a regular epimorphism, there is some $v \in V$ with norm $<1$ and $f(v) = g(t)$. - Then $(v,t) \in V \times_W T$ has norm $\max(|v|,|t|) < 1$ and provides a preimage of $t$. + Let $t \in T$ be an element of norm $<1$. Since $g$ is a linear contraction, $g(t)$ has norm $<1$. Since $f$ is a regular epimorphism, there is some $v \in V$ with norm $<1$ and $f(v) = g(t)$. + Then $(v,t) \in V \times_W T$ is a preimage of $t$ with norm $\max(|v|,|t|) < 1$. unsatisfied_properties: - property: skeletal @@ -95,8 +95,10 @@ special_morphisms: proof: The non-trivial direction follows from the well-known fact that for every closed subspace of a Banach space its quotient space is again a Banach space. regular epimorphisms: description: >- - For a linear contraction $f : V \to W$ the following are equivalent: (1) $f$ is a regular epimorphism. (2) $f$ is surjective and the norm on $W$ is given by $|w| = \inf \{|v| : f(v) = w\}$. (3) $f$ is surjective and $f$ maps the open unit ball of $V$ onto the open unit ball of $W$. + For a linear contraction $f : V \to W$ the following are equivalent: (1) $f$ is a regular epimorphism. (2) The norm on $W$ is given by $|w| = \inf \{|v| : f(v) = w\}$. (3) $f$ maps the open unit ball of $V$ onto the open unit ball of $W$. proof: >- + First of all, notice that all three conditions imply that $f$ is surjective. + (1) implies (2): This follows immediately from the concrete construction of coequalizers, and the quotient Banach space $V/U$ in particular. (2) implies (1): Let $U \coloneqq \ker(f)$. Then $U$ is a closed subspace of $V$, and $f$ induces a bijective linear contraction $\tilde{f} : V/U \to W$. It is isometric by assumption on $f$ and the definition of the norm on $V/U$. Thus, $\tilde{f}$ is an isomorphism. Since $V/U$ is the cokernel of $U \hookrightarrow V$, it follows that $f$ is a regular epimorphism. From c64378a4986da195f0061d43bac269da696143fd Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 29 Jun 2026 06:49:59 +0200 Subject: [PATCH 6/7] fix description of products of Banach spaces --- databases/catdat/data/categories/Ban.yaml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index ae45e49d9..a91c94345 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -76,9 +76,9 @@ special_objects: terminal object: description: trivial Banach space coproducts: - description: 'The coproduct of a family of Banach spaces $(B_i)$ is the subspace $\bigl\{x \in \prod_i B_i : \sum_i |x_i| < \infty\bigr\}$ equipped with the $1$-norm $|x| \coloneqq \sum_i |x_i|$.' + description: 'The coproduct of a family of Banach spaces $(B_i,|{-}|)_{i \in I}$ is the subspace $\bigl\{x \in \prod_{i \in I} B_i : \sum_{i \in I} |x_i| < \infty\bigr\}$ of their vector space product equipped with the $1$-norm $|x|_1 \coloneqq \sum_{i \in I} |x_i|$.' products: - description: direct products with the $\sup$-norm + description: 'The product of a family of Banach spaces $(B_i,|{-}|)_{i \in I}$ is the subspace $\bigl\{x \in \prod_{i \in I} B_i : \sup_{i \in I} |x_i| < \infty\bigr\}$ of their vector space product equipped with the $\sup$-norm $|x|_\infty \coloneqq \sup_{i \in I} |x_i|$.' special_morphisms: isomorphisms: From 441b5222ecfc39dc681997f683e3d79ce79eda11 Mon Sep 17 00:00:00 2001 From: Script Raccoon Date: Mon, 29 Jun 2026 07:27:03 +0200 Subject: [PATCH 7/7] Ban has no regular quotient object classifier --- databases/catdat/data/categories/Ban.yaml | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index a91c94345..aecaf9ca7 100644 --- a/databases/catdat/data/categories/Ban.yaml +++ b/databases/catdat/data/categories/Ban.yaml @@ -55,6 +55,13 @@ unsatisfied_properties: - property: regular subobject classifier proof: If $\Omega$ is a regular subobject classifier, then by the classification of regular monomorphisms, $\Hom(X,\Omega)$ is isomorphic to the set of closed subspaces of $X$ for any Banach space $X$. For $X = \IC$ this implies that there are exactly two vectors in $\Omega$ with norm $\leq 1$, which is absurd. (For $\Omega = 0$ there is just one, and for $\Omega \neq 0$ there are infinitely many.) + - property: regular quotient object classifier + proof: >- + Assume that $\Psi$ is a regular quotient object classifier in $\Ban$. For a Banach space $V$ let $S(V)$ be the set of closed subspaces of $V$. Then for any Banach space $V$ the map + $$\Hom(\Psi,V) \to S(V), \quad f \mapsto \overline{\im(f)}$$ + is bijective. In particular, there is a morphism $f : \Psi \to V$ with dense image, i.e. an epimorphism. But this contradicts the already established fact that $\Ban$ is well-copowered (since it is locally presentable). + Alternatively, we may use that for every cardinal $\kappa$ the Banach space $\ell^2(\kappa^+)$ has no dense subset of size $\kappa$. + - property: unital proof: The canonical morphism $X \sqcup Y \to X \times Y$ is injective, and therefore a monomorphism. Hence, if it were also a strong epimorphism, it would be an isomorphism. However, for example, when $X = Y = \IC$, the norms do not agree.