Add various properties of Ban

[ScriptRaccoon]

This PR

• adds the easy proof that Ban is not counital (thus, resolves Is this a correct proof that Ban is counital? #257)
• adds the classification of regular epimorphisms in Ban
• adds the proof that Ban is regular
• adds the proof that Ban has no regular quotient object classifier

Thanks to @dschepler !

[dschepler]

Looks good to me.

On a related note, I'm pretty convinced that the regular epimorphisms in Ban are exactly the linear contractions which are surjective on open unit balls - or equivalently, surjective maps $f : X \to Y$ such that the norm on $Y$ is equal to $\inf { |x| \mid f(x) = y }$. Which should make it pretty easy to show that regular epimorphisms are stable under pullback, and therefore Ban is regular.

[ScriptRaccoon]

Thanks! I have added the proofs. So we have filled 3 gaps instead of just one here, great :)

[ScriptRaccoon]

Is there a reason why we didn't decide if Ban has effective congruences so far? (and thus, is Barr-exact)

This looks correct and doable. I will try to write it down.

[dschepler]

Is there a reason why we didn't decide if Ban has effective congruences so far? (and thus, is Barr-exact)

This looks correct and doable. I will try to write it down.

I guess at the vector space level, it's clear a congruence has to be congruence modulo some subspace. The question is: does the norm have to match the max norm? Just from the conditions $|(x,y)| \ge \max(|x|,|y|)$, $|(x,x)| = |x|$, $|(x,y)| = |(y,x)|$, and $|(x,z)| \le \max(|(x,y)|, |(y,z)|)$. (If so, then clearly the 0 slice is a closed subspace, so the congruence is exactly the kernel pair of the quotient map.)

[dschepler]

Maybe we can also settle "regular quotient object classifier"? It looks like that means that $\Psi$ would have to be big enough to be able to have a dense image in any closed subspace, which you should be able to rule out with a cardinality argument, using the fact that any Banach space is sequential.

[dschepler]

Just noticed: for the description of products, do you need to restrict to the subspace with finite sup-norm, similar to the restriction needed for the description of coproducts?