Add various properties of Ban

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 <a href="/category-implication/biproducts_cartesian_filtered_colimits">here</a>), 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 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.
+      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
     proof: This is trivial.
@@ -48,8 +55,18 @@ 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: See <a href="https://math.stackexchange.com/questions/5033161" target="_blank">MSE/5033161</a>.
+    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.
 
   - property: co-Malcev
     proof: See the comments to <a href="https://mathoverflow.net/a/509555/2841" target="_blank">MO/509552</a>.
@@ -66,9 +83,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:
@@ -83,3 +100,16 @@ special_morphisms:
   regular monomorphisms:
     description: closed embeddings
     proof: The non-trivial direction follows from the <a href="https://math.stackexchange.com/questions/319867" target="_blank">well-known fact</a> 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) 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.
+
+      (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|$.

databases/catdat/data/category-properties/counital.yaml

@@ -1,6 +1,6 @@
 id: counital
 relation: is
-description: 'A category is <i>counital</i> 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 <i>counital</i> 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 <a href="https://ncatlab.org/nlab/show/strong+monomorphism" target="_blank">strong monomorphism</a>.'
 dual_property: unital
 invariant_under_equivalences: true
 

databases/catdat/data/category-properties/unital.yaml

@@ -1,6 +1,6 @@
 id: unital
 relation: is
-description: 'A category is <i>unital</i> 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 <i>unital</i> 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 <a href="https://ncatlab.org/nlab/show/strong+epimorphism" target="_blank">strong epimorphism</a>.'
 nlab_link: https://ncatlab.org/nlab/show/unital+category
 dual_property: counital
 invariant_under_equivalences: true