diff --git a/databases/catdat/data/categories/Ban.yaml b/databases/catdat/data/categories/Ban.yaml index 92fef27f..aecaf9ca 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 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 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. - property: co-Malcev proof: See the comments to MO/509552. @@ -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 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) 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|$. diff --git a/databases/catdat/data/category-properties/counital.yaml b/databases/catdat/data/category-properties/counital.yaml index b71b7cdb..57e443b7 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 acd194b3..43d75ea5 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