Proving that Ban is a Pre-Abelian Category via Cauchy Completion Functor

We are working over $\mathbb{C}$$\mathbb{C}$.

Let $\mathsf{Ban}$$\mathsf{Ban}$ be the category of Banach spaces. Let $X$$X$ be a Banach space, a sub vector space $V\subseteq X$$V\subseteq X$ is a subobject if $V$$V$ is closed. Otherwise $V$$V$ is not a Banach space. It is easy to see that $\mathsf{Ban}$$\mathsf{Ban}$ is an additive category. Similarly, denote $\mathsf{Norm}$$\mathsf{Norm}$ as the category of normed vector spaces, which is a pre-abelian category.

We would like to prove that $\mathsf{Ban}$$\mathsf{Ban}$ is a pre-abelian category.

It is easy to see that the kernel exists in $\mathsf{Ban}$$\mathsf{Ban}$. For cokernel, we have the following adjoint pair between $\mathsf{Norm}$$\mathsf{Norm}$ and $\mathsf{Ban}$$\mathsf{Ban}$:

$U⊣F$$U \dashv F$

Here $U$$U$ is the Cauchy completion functor, and $F$$F$ is the forgetful/embedding functor. Then both $U,F$$U, F$ are additive functors.

Proposition. Let $X$$X$ be a Banach space and $K$$K$ is a closed subspace of $X$$X$. Then the cokernel of $K\hookrightarrow X$$K\hookrightarrow X$ exists.

Proof. Consider the following short exact sequence in $\mathsf{Norm}$$\mathsf{Norm}$:

$$0⟶K⟶X\stackrel{\pi }{\to }X/K⟶0$$

The Cauchy completion functor preserves cokernels:

$$U(\mathrm{coker}(K\hookrightarrow X))\cong \mathrm{coker}(U(K)\hookrightarrow U(X))\cong \mathrm{coker}(K\hookrightarrow X)$$

Hence $U(X/K)\cong X/K$$U(X/K)\cong X/K$. $◻$$\square$