Zulip Chat Archive

Stream: maths

Topic: Norm of 1


view this post on Zulip 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
x1i=0(tx1)ix1(1+i=1tx1i)\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 1=1\lVert 1\rVert=1 this can be written crisply as x1(1tx1)1\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.

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 18:42):

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

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 18:42):

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

view this post on Zulip Heather Macbeth (Jul 18 2020 at 18:42):

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

view this post on Zulip 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.

view this post on Zulip 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 R\mathbb{R} which tend to 0 at ±\pm\infty) are not unital.

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 18:50):

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

view this post on Zulip Reid Barton (Jul 18 2020 at 18:50):

aka the ring of bounded continuous functions on the empty space

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 18:51):

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

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 18:51):

Should we have an additional typeclass norm_one?

view this post on Zulip Yury G. Kudryashov (Jul 18 2020 at 18:52):

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

view this post on Zulip 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)

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 18:54):

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jul 18 2020 at 18:56):

There are many non-closed points

view this post on Zulip 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 1=1\lVert 1\rVert = 1 in rings as well.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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 11\lVert 1\rVert \leq 1. That would be perfectly fine for my current purpose.

view this post on Zulip Heather Macbeth (Jul 18 2020 at 20:48):

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

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Jul 18 2020 at 20:51):

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

view this post on Zulip Jalex Stark (Jul 18 2020 at 20:52):

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

view this post on Zulip 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 11\lVert 1\rVert \leq 1? :up:

view this post on Zulip 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.

view this post on Zulip 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 aibi\sum \|a_i\| \|b_i^*\| over all representations of the operator as aibi\sum a_i \otimes b_i^* where aia_i is an element of the space and bib_i^* an element of the dual. It is a natural norm satisfying ABAB\|A B\|\leq \|A\| \|B\|, but in dimension nn the norm of the identity is nn. The same would go for the Hilbert-Schmidt norm.

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 09:36):

This is maybe not a norm but a seminorm

view this post on Zulip Sebastien Gouezel (Jul 19 2020 at 09:42):

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

view this post on Zulip David Wärn (Jul 19 2020 at 11:25):

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

view this post on Zulip 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.

view this post on Zulip 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. 11 \lVert 1 \rVert \le 1
  • There are normed non-unital rings, where do not require a multiplicative identity, and hence could not require 11 \lVert 1 \rVert \le 1 even if we wanted to

view this post on Zulip 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=e1e1A = e_1 \otimes e_1^* is a projector, it has norm 11, and it wouldn't satify A2A2\|A^2\| \leq \|A\|^2 for the normalized norm).

view this post on Zulip 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 11\|1\| \leq 1. Maybe add a further typeclass requiring this inequality, but avoid it when it's not really necessary?

view this post on Zulip 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: May 11 2021 at 16:22 UTC