NormedModule ?

Stream: Is there code for X?

[Sophie Morel]

It's all in the title. Does there exist a class corresponding to normed modules over a normed ring ? (Not necessarily commutative.) I wanted to work with normed vector spaces over a normed division algebra (like the quaternions), but NormedSpace requires the coefficients to be a field.
Also, in p-adic theory people work with normed modules over Banach algebras, so this is a useful notion.

[Eric Wieser]

Yes, it's docs#BoundedSMul

[Eric Wieser]

Maybe three months ago I made a series of refactors to generalize results about NormedSpace to be about BoundedSMul instead

[Sophie Morel]

Awesome, thanks ! Do you have the fact that the inequality is an equality if the coefficients are a division ring ?

[Sophie Morel]

(I mean the inequalities in dist_smul_pair' and dist_pair_smul').

[Eric Wieser]

Yes, maybe docs#dist_smul ?

[Eric Wieser]

Certainly docs#norm_smul ?

[Sophie Morel]

I see, thank you again!

[Eric Wieser]

I can't remember if I thought NormedModule was a bad idea, or if i just didn't want to take on that large a refactor!

[Yaël Dillies]

Btw I have BoundedSMul instances for Prod and Pi if you need them.

[Sophie Morel]

I certainly will @Yaël Dillies if I ever get far enough with my quatertionic projectiv spaces (at least I'll need the Prod). Are they in mathlib already ?

[Yaël Dillies]

No, they're currently parked in LeanCamCombi LeanAPAP. Let me PR that real quick.

[Sophie Morel]

Thanks !

[Yaël Dillies]

#7311

[Yaël Dillies]

Just in time for my battery to die.

[Sophie Morel]

No worries, I have to teach tomorrow afternoon so I won't come back to this before tomorrow evening at the earliest.

[Kevin Buzzard]

Yeah these normed modules over normed rings such as affinoid algebras are everywhere in p-adic analysis.

[Yaël Dillies]

Merging now

[Yaël Dillies]

Merged

[Anatole Dedecker]

What do you think of the following:

• add a NormEqDistZero class with the axiom ‖x‖ = dist x 0
• add an instance from SeminormedAddGroup to NormEqDistZero
• redefine NormedSpace (or NormedModule, or NormedSMul) as the current BoundedSMul, except assuming NormEqDistZero on both spaces and thus replacing the weird-looking dist x 0 by more natural ‖x‖.

That way we can get rid of BoundedSMul (maybe adding a few Norm and NormEqDistZero instances to cover e.g docs#NNReal.boundedSMul) and we no longer have multiple ways to express the same thing (I think the BoundedSMul typeclass was a bit confusing in itself). The main disadvantage is that we have to write [Module R E] [NormedSpace R E] instead of just [NormedSpace R E], but I'd argue that we should be un-doing some of the algebra+norm bundles anyways.

[Sophie Morel]

It sounds good to me, it would make the classes easier to find and possibly to use. But I have no real idea of how painful that would be, or of the trouble it could cause elsewhere.

[David Loeffler]

If NormedModule R E is going to be the current BoundedSMul with dist x 0 replaced by ‖x‖, then I think there's a risk of confusion since BoundedSMul R E ends up requiring E to have both a norm and a metric, but not that dist x y = ‖x - y‖ for all x, y, so the metric is not determined by the norm. Generally it seems bizarre to call something NormedModule and yet have its definition in terms of metrics rather than norms.

I'd advocate that NormedModule R E (or whatever the successor to BoundedSMul is called) should assume SeminormedRing R and SeminormedAddGroup E, and be wholly written in terms of norms.

[David Loeffler]

I guess this wouldn't cover the existing docs#NNReal.boundedSMul; but how crucial is this anyway? I tried commenting it out and recompiling and nothing's broken so far.

[Anatole Dedecker]

Well the whole point of BoundedSMul was to have a common API for true normed modules and also some weaker use cases, typically NNReal. My claim was that we wouldn't lose anything by actually incorporating this into NormedModule, even if it means that the typeclass is weaker than its name suggest (similarly to how we use Module for semi-modules). I think the main downside of my approach is that writing [NormedModule R E] would no longer throw an error in absence of [SeminormedAddGroup E].

[Eric Wieser]

The original motivation wasn't NNReal, but normed Quaternion modules; but indeed it would be a shame to drop any existing instances

[Anatole Dedecker]

Eric Wieser said:

The original motivation wasn't NNReal, but normed Quaternion modules; but indeed it would be a shame to drop any existing instances

Oh okay. But anyways this one would be covered by NormedModule assuming SeminormedAddGroup.

[Eric Wieser]

Actually, I now remember the motivation was more general than that; I wanted norm_smul_le to work when • = *

[Eric Wieser]

So that we didn't repeat all the module results from scratch for rings