mathlib

mathlib copied to clipboard

We define structures ring_seminorm and ring_norm. These definitions are useful when one needs to consider multiple (semi)norms on a given ring.

---

Are you aware of the seminorm structure we already have? I'm a little worried this is duplicating it, just with a different sort of bundling

Are you aware of the seminorm structure we already have? I'm a little worried this is duplicating it, just with a different sort of bundling

The structure seminorm is for defining module seminorms over a normed ring, that is not what I want here - I want a structure that tells me that a given function is a (ring) seminorm on a given ring.

I think if we really want both is_seminorm and seminorm, then we should rename the concept in this file to is_mul_seminorm or similar.

Is it the case that anything satisfying is_mul_seminorm can be turned into seminorm, or does neither imply the other.

I think if we really want both is_seminorm and seminorm, then we should rename the concept in this file to is_mul_seminorm or similar.

I would not mind renaming is_seminorm to is_ring_seminorm.

Is it the case that anything satisfying is_mul_seminorm can be turned into seminorm, or does neither imply the other.

If you have an is_ring_seminorm on k that satisfies the triangle inequality (which I probably should include in the definition), and you use this seminorm to put a semi_normed_ring kstructure on k, then this is trivially a seminorm when regarding k as a module over itself (I think this may be what you mean).

However, I explicitly want to avoid having a preferred seminorm on k; I want to be able to consider several ring seminorms on k (and a second is_ring_seminorm on k would not be a seminorm with respect to a preferred semi_normed_ring k structure).

If you have an is_seminorm_ring on k that satisfies the triangle inequality (which I probably should include in the definition)

This was really what I was getting at; it seems odd for a seminorm not to satisfy the triangle inequality.

I still wonder if a better approach would be to do

structure ring_seminorm extends seminorm 𝕜 E

Ah, I understand your comment now; I hadn't realized that seminorm 𝕜 E relied on an underlying global norm on 𝕜

(misclick, sorry)

This was really what I was getting at; it seems odd for a seminorm not to satisfy the triangle inequality.

Yes, this was an oversight on my part (since I was using is_ring_seminorm together with is_nonarchimedean in my applications). I've now included the triangle inequality as part of the definition of is_ring_seminorm.

Yeah this PR is something a bit different to seminorm, which is for modules. My impression of what's going on here is that both analysts and algebraists want to talk about norms and seminorms, but the analysts are always working over the reals and complexes with their fixed usual norm, and want to talk about seminorms on vector spaces over these fields, whereas the algebraists don't have this "fixed base" and want to talk about seminorms on fields like the rationals, finite extensions of the rationals, finite extensions of the p-adic numbers, integers of these things, and so on. I guess calling the main definition is_ring_seminorm is one way of flagging this difference.

Ah, I understand your comment now; I hadn't realized that seminorm 𝕜 E relied on an underlying global norm on 𝕜

Thinking again, I don't think this matters; you can always just set 𝕜 = punit and then it becomes irrelevant. So maybe extending seminorm is still the right way to go.

Thinking again, I don't think this matters; you can always just set 𝕜 = punit and then it becomes irrelevant. So maybe extending seminorm is still the right way to go.

I hadn't thought of this. I will try it out. Update: This approach doesn't work because a general ring is not a module over punit. I will replace is_ring_seminorm by a structure ring_seminorm extending add_monoid_seminorm from #14336.

I don't really feel comfortable reviewing this, the code looks good, but I cannot judge whether this makes sense mathematically.

:v: mariainesdff can now approve this pull request. To approve and merge a pull request, simply reply with bors r+. More detailed instructions are available here.

bors r+

Canceled.

If you agree with the folder scheme I described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Reorganising.20norms, could you move the new material to analysis.normed.field.seminorm or analysis.normed.ring.seminorm? I suspect this second option only makes sense if normed_ring doesn't live with normed_field in analysis.normed.field.basic.

If you agree with the folder scheme I described at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Reorganising.20norms, could you move the new material to analysis.normed.field.seminorm or analysis.normed.ring.seminorm?

I've moved it to analysis.normed.ring.seminorm (to me that seems the better option). Assuming CI works, would this be ready to merge? Otherwise it will have to wait until September 5th.

~~@YaelDillies, you said that #16237 already added add_group_seminorm.trivial_norm but I can't find it. Does it have a different name?~~ I guess it's the 1 norm.

~~I think add_group_seminorm.trivial_norm f is just f ≠ 0?~~

Can I go ahead and merge it now?

Well I would prefer for you to introduce the hom classes straight away. If you don't know how to, I can do it.

Well I would prefer for you to introduce the hom classes straight away. If you don't know how to, I can do it.

I am happy to do that in a new PR after this one is merged. The thing is that I don't need the hom classes,, but I have needed the ring_norm and ring_seminorm definitions for months now - I would rather not wait for something that could be PRd in parallel.

Here they are.

I think it's fair merging now

bors r+

Pull request successfully merged into master.

Build succeeded:

• Build mathlib
• Lint mathlib
• Lint style
• Run tests