Zulip Chat Archive

Stream: maths

Topic: Definition of `normed_algebra`

Yury G. Kudryashov (Oct 03 2021 at 12:36):

What do you think about changing the "extra" axiom of normed_algebra k A from norm_algebra_map_eq to norm_smul_le (which is equivalent to norm_smul_eq since we require k to be a normed filed)? My motivation is that we'll be able to reuse normed_space proofs in normed_algebra instances. As far as I understand, the current axiom is equivalent to norm_smul_eq + norm_one.

AFAIR, @Kevin Buzzard said some time ago that the definition with norm_algebra_map is bad in some cases, and @Heather Macbeth had to consider some "trivial" cases separately but I don't remember the details.

Eric Wieser (Oct 03 2021 at 15:01):

Surely docs#normed_algebra.to_normed_space means the proofs can already be reused?

Kevin Buzzard (Oct 03 2021 at 15:46):

Unfortunately I can't remember my thoughts at the time. I remember one issue, which was that I wanted 0 to be a normed k-algebra but the map from k into this algebra isn't an isometry

Yury G. Kudryashov (Oct 03 2021 at 16:08):

@Eric Wieser We can't reuse the proof of “A is a normed space over k” in the proof of “A is a normed algebra over k”.

Yury G. Kudryashov (Oct 03 2021 at 16:09):

I remember one issue @Heather Macbeth encountered: continuous linear endomorphisms of the zero vector space do not form a normed algebra over the base field.

Kevin Buzzard (Oct 03 2021 at 17:36):

They do as far as I'm concerned. Are you just saying they don't in Lean?

Yury G. Kudryashov (Oct 03 2021 at 17:38):

Yes, because the norm of one is zero.

Yury G. Kudryashov (Oct 03 2021 at 17:39):

I mean, yes, I was talking about "do not form a normed algebra ... in the sense of docs#normed_algebra".

Kevin Buzzard (Oct 03 2021 at 18:07):

So this means for example that affinoid algebras will not be normed algebras even though they're algebras with a norm, because the zero algebra is definitely an affinoid algebra (its valuation spectrum is the empty set).

Kevin Buzzard (Oct 03 2021 at 18:11):

According to Bosch-Guentzer-Remmert, a normed ring has |1|<=1 and |xy|<=|x||y|, and this forces either |1|=1 or R=0

Kevin Buzzard (Oct 03 2021 at 18:28):

In short, I would be maximally in favour of removing the incorrect axiom and replacing it with the correct one.

Adam Topaz (Oct 03 2021 at 18:38):

If we change the definition of a normed algebra by relaxing the isometry condition to, say, | algebra_map x | \le | x |, then k with the trivial norm would be a normed algebra over k with a nontrivial norm. Do we want thhis?

Riccardo Brasca (Oct 03 2021 at 18:53):

The trivial norm is an interesting one, isn't it? I think that people doing Berkovich geometry really like it

Adam Topaz (Oct 03 2021 at 19:49):

I completely agree that it's an interesting norm, but I'm not completely convinced we want to generalize the normed_algebra class in this way.

Kevin Buzzard (Oct 03 2021 at 20:04):

I think that if a field has a nontrivial norm then there are elements of norm both less than and greater than one so I'm not convinced @Adam Topaz

Adam Topaz (Oct 03 2021 at 20:07):

Oh you're right Kevin, I'm thinking in terms of valuations

Adam Topaz (Oct 03 2021 at 20:07):

(the trivial valuation is coarser than any other valuation)

Adam Topaz (Oct 03 2021 at 20:21):

Ok, maybe we should actually change = in normed_algebra to $\le$ :)

Yury G. Kudryashov (Oct 03 2021 at 20:33):

Why not just use norm_smul_le?

Adam Topaz (Oct 03 2021 at 20:35):

Sure. That works too

Yury G. Kudryashov (Oct 04 2021 at 02:26):

It seems that we do not require norm_one_le_one in docs#normed_ring. Should I add this axiom?

Yury G. Kudryashov (Oct 04 2021 at 02:26):

This will make things like docs#list.norm_prod_le work without [norm_one_class] assumption.

Yury G. Kudryashov (Oct 04 2021 at 02:45):

BTW, do we really need a [normed_field] for a [normed_algebra]?

Yury G. Kudryashov (Oct 04 2021 at 02:46):

I mean, what's wrong with normed algebras over normed rings?

Yury G. Kudryashov (Oct 04 2021 at 02:46):

(disclaimer: quite possibly I miss something trivial)

Adam Topaz (Oct 04 2021 at 02:52):

I think normed rings should be allowed as a base for normed algebras (well, the algebra class requires commutativity, so normed_comm_ring, is that a thing?)

Yury G. Kudryashov (Oct 04 2021 at 02:57):

Yes, we have this.

Yury G. Kudryashov (Oct 04 2021 at 03:44):

Also, I'm going to replace docs#norm_one_class with a lemma assuming [normed_ring R] [nontrivial R].

Yury G. Kudryashov (Oct 04 2021 at 04:17):

Started branch#redefine-normed-algebra.

Yury G. Kudryashov (Oct 04 2021 at 04:17):

(with only a partial refactor, i.e. I still require k to be a normed field)

Yury G. Kudryashov (Oct 04 2021 at 04:20):

(and I'm removing docs#semi_normed_space in the same branch; we already had this situation with semimodule and module)

Scott Morrison (Oct 04 2021 at 04:37):

semi_normed_space and semimodule have completely different meanings of semi! One is about the metric being only a pseudometric, the other is about not having negatives.

Yury G. Kudryashov (Oct 04 2021 at 04:38):

But both situations (semimodule vs module and semi_normed_space vs normed_space) are very similar from Lean point of view.

Scott Morrison (Oct 04 2021 at 04:38):

Indeed, I see. :-)

Yury G. Kudryashov (Oct 04 2021 at 04:38):

I mean, normed_space has the same axioms but it takes stronger TC arguments.

Riccardo Brasca (Oct 04 2021 at 05:48):

I am maybe confused, by the situation for seminormed space seems a little different than with semimodule: a semimodule over a ring is automatically a module, but I don't see an analogue for seminormed space.

Sebastien Gouezel (Oct 04 2021 at 05:53):

Yury G. Kudryashov said:

It seems that we do not require norm_one_le_one in docs#normed_ring. Should I add this axiom?

Definitely not: there are important examples of normed rings where the identity has norm larger than one (for instance n x n matrices with the Hilbert-Schmidt norm). That's the reason of the norm_one_class. We should probably add this in the docstring for normed rings.

Johan Commelin (Oct 04 2021 at 06:01):

Sebastien Gouezel said:

We should probably add this in the docstring for normed rings.

:this:

Yury G. Kudryashov (Oct 04 2021 at 06:32):

@Sebastien Gouezel Thank you, I'll revert this part of the patch.

Yury G. Kudryashov (Oct 04 2021 at 06:32):

@Riccardo Brasca A seminormed space that is a normed group is automatically a normed space.

Riccardo Brasca (Oct 04 2021 at 06:39):

Sure. But then we will have seminormed_group and normed_group but only normed_space?
To be clear: I don't have a strong opinion here, but we definitely want to be able to work with seminormed vector spaces.