Zulip Chat Archive

Stream: maths

Topic: Norm of 1

Heather Macbeth (Jul 18 2020 at 18:40):

@Yury G. Kudryashov , we discussed adding an axiom to normed_ring, that the norm of 1 be 1. At the time we agreed to leave it, but I would like to propose making the change now, because I have a use in mind.

The use: I would like to show that in a complete normed ring, ∥(x + t)⁻¹∥ is O(1) as t → 0. The argument is to bound ∥(x + t)⁻¹∥ by
$\lVert x^{-1}\sum_{i=0}^\infty(tx^{-1})^i\rVert\leq \lVert x^{-1}\rVert \left(\lVert 1\rVert + \sum_{i=1}^\infty\lVert tx^{-1}\rVert ^i\right)$ .

If $\lVert 1\rVert=1$ this can be written crisply as $\lVert x^{-1}\rVert \left(1 - \lVert tx^{-1}\rVert \right)^{-1}$ . It's obviously still possible without the axiom, just a little messier, so this only justifies adding the axiom if it is a good axiom for other reasons.

Yury G. Kudryashov (Jul 18 2020 at 18:42):

I don't know if there is some exotic normed_ring with $\|1\|\ne 1$ we should care about.

Yury G. Kudryashov (Jul 18 2020 at 18:42):

Let's wait for 24h. If no one objects, then go ahead.

Heather Macbeth (Jul 18 2020 at 18:42):

Sounds good. Let us also invoke exotic analysts such as @Kevin Buzzard .

Yury G. Kudryashov (Jul 18 2020 at 18:43):

I remember that some lemmas about is_o/is_O assume normed_field instead of normed_ring only to have norm_one.

Heather Macbeth (Jul 18 2020 at 18:46):

I think the more controversial axiom (which we already have) is to assume that a normed ring/algebra even has a 1 at all, since some important normed algebras (eg, the ring of continuous functions on $\mathbb{R}$ which tend to 0 at $\pm\infty$ ) are not unital.

Kevin Buzzard (Jul 18 2020 at 18:50):

In pure algebra it's really important to let 0 be a ring

Reid Barton (Jul 18 2020 at 18:50):

aka the ring of bounded continuous functions on the empty space

Kevin Buzzard (Jul 18 2020 at 18:51):

In non-archimedean analysis it's really important to let 0 be a normed ring

Yury G. Kudryashov (Jul 18 2020 at 18:51):

Should we have an additional typeclass norm_one?

Yury G. Kudryashov (Jul 18 2020 at 18:52):

Some day we'll need (a) (normed) non-unital rings; (b) (normed) semifields.

Kevin Buzzard (Jul 18 2020 at 18:54):

However in non-archimedean analysis and algebraic geometry the fundamental geometric objects (schemes, rigid spaces, Berkovich spaces, adic spaces, algebraic stacks etc) are built by gluing model spaces which are spectra of such rings (affine schemes, affinoid spaces etc)

Kevin Buzzard (Jul 18 2020 at 18:54):

In all of these theories, the use of sheaves is absolutely central

Kevin Buzzard (Jul 18 2020 at 18:55):

Grothendieck once said that it didn't matter if you had bad objects as long as you had a good category

Kevin Buzzard (Jul 18 2020 at 18:56):

A scheme is a disgusting thing to a geometer. The underlying topological space is completely pathological, for example

Heather Macbeth (Jul 18 2020 at 18:56):

And indeed, @Kevin Buzzard already made the case for modifying the axioms in normed_algebra to include the zero ring, for related reasons.

Kevin Buzzard (Jul 18 2020 at 18:56):

There are many non-closed points

Heather Macbeth (Jul 18 2020 at 18:57):

I am fairly sympathetic to this, so maybe the conclusion should be that, at least, we should not make it harder to possibly fix that in future by requiring that $\lVert 1\rVert = 1$ in rings as well.

Kevin Buzzard (Jul 18 2020 at 18:57):

But the category of schemes is really nice. There are many kinds of limits and colimits. Furthermore in algebraic geometry we really use these limits

Kevin Buzzard (Jul 18 2020 at 19:00):

I think that there is some strange disconnect here. For a manifold the local model is not a ring, it is R^n and maybe this is a point where the theory bifurcates. Sheaves seem to be far less crucial to the differential geometers. So maybe it's more convenient for them to have all algebras non-zero for some reason

Kevin Buzzard (Jul 18 2020 at 19:02):

I want normed spaces because I want to make geometric objects from them. A differential geometer wants them for completely different reasons

Heather Macbeth (Jul 18 2020 at 19:02):

I want these for differential geometry only indirectly -- my use case will be the normed ring of bounded linear operators on a Banach space.

Kevin Buzzard (Jul 18 2020 at 19:44):

But the 0 Banach space is a Banach space right? Is it somehow less important than the zero ring?

Heather Macbeth (Jul 18 2020 at 20:43):

Interestingly, in the previous conversation about axioms for normed rings (here's the link again), Kevin's proposed axiom about the norm of 1 was that $\lVert 1\rVert \leq 1$ . That would be perfectly fine for my current purpose.

Heather Macbeth (Jul 18 2020 at 20:48):

And note that since $\lVert 1\rVert = \lVert 1^2\rVert \leq \lVert 1\rVert^2$ , this axiom forces that $\lVert 1\rVert \in \{0,1\}$ , with the former occurring only in the zero ring.

Jalex Stark (Jul 18 2020 at 20:50):

then you can write a lemma in the namespace assuming nontrivial R and proving that the norm is one, and you'll have the same API as if you had made the more restrictive definition

Heather Macbeth (Jul 18 2020 at 20:51):

Yes, if anyone needs that $\lVert 1\rVert = 1$ -- like I said, $\lVert 1\rVert \leq 1$ is fine for my current purpose.

Jalex Stark (Jul 18 2020 at 20:52):

i think there's nothing controversial about this new axiom, then

Heather Macbeth (Jul 18 2020 at 23:03):

Let's make sure others think so -- @Yury G. Kudryashov , @Kevin Buzzard (and others), how would you feel about the axiom $\lVert 1\rVert \leq 1$ ? :up:

Heather Macbeth (Jul 18 2020 at 23:14):

@Kevin Buzzard , if you like, I would be willing to implement your other proposed normed algebra axiom at the same time (replacing the axiom ∀ (c : 𝕜), ∥(algebra_map c)∥ = ∥c∥ with the axiom ∀ (c : 𝕜) (x : E), ∥(algebra_map c) * x∥ = ∥c∥ * ∥x∥), so that 0 can join the ranks of the normed algebras. But this would be a more controversial change, so should be discussed more thoroughly.

Sebastien Gouezel (Jul 19 2020 at 07:39):

I have a counterexample to the axiom. The trace-class norm of a finite rank operator is the minimum of $\sum \|a_i\| \|b_i^*\|$ over all representations of the operator as $\sum a_i \otimes b_i^*$ where $a_i$ is an element of the space and $b_i^*$ an element of the dual. It is a natural norm satisfying $\|A B\|\leq \|A\| \|B\|$ , but in dimension $n$ the norm of the identity is $n$ . The same would go for the Hilbert-Schmidt norm.

Kevin Buzzard (Jul 19 2020 at 09:36):

This is maybe not a norm but a seminorm

Sebastien Gouezel (Jul 19 2020 at 09:42):

No it's really a norm (it's larger than the usual operator norm).

David Wärn (Jul 19 2020 at 11:25):

This sounds like a "not-necessarily-unital normed algebra" rather than a "normed ring"

Scott Morrison (Jul 19 2020 at 11:29):

These examples only have an identity when they are finite dimensional, in which case you can normalise the norm by the dimension.

David Wärn (Jul 19 2020 at 11:45):

I think normalisation would break submultiplicativity
Doesn't the trace-class norm show that there are two different good notions?

There are normed unital rings, where we require a multiplicative identity / empty product, and hence also require submultiplicativity for the empty product, i.e. $\lVert 1 \rVert \le 1$
There are normed non-unital rings, where do not require a multiplicative identity, and hence could not require $\lVert 1 \rVert \le 1$ even if we wanted to

Sebastien Gouezel (Jul 19 2020 at 11:56):

Scott Morrison said:

These examples only have an identity when they are finite dimensional, in which case you can normalise the norm by the dimension.

If you normalize by the dimension, you lose the multiplicativity (for instance $A = e_1 \otimes e_1^*$ is a projector, it has norm $1$ , and it wouldn't satify $\|A^2\| \leq \|A\|^2$ for the normalized norm).

Sebastien Gouezel (Jul 19 2020 at 12:00):

Of course, I agree that this example is a little bit artificial, as in general this ring doesn't have a unit. But when it turns out to have one (which only happens in finite dimension), it doesn't satisfy $\|1\| \leq 1$ . Maybe add a further typeclass requiring this inequality, but avoid it when it's not really necessary?

Heather Macbeth (Jul 19 2020 at 13:23):

OK, I guess that clinches it :). I will leave the library as it is, but in the future someone could refactor to implement Kevin's axioms for normed algebras (which Sébastien's example doesn't break, at least not any more than the current axioms).

Last updated: Dec 20 2023 at 11:08 UTC