normed_field

Stream: maths

[Jireh Loreaux]

There's no way to upgrade a normed_ring which is also a field to a normed_field, right? I'm asking because I want to say that the quotient of a complete normed ring by a maximal ideal is a normed division ring, but when I created that I gave it a norm_mul field instead of a norm_mul_le field, so I'm not sure I can prove this without changing the definition of normed_division_ring.

[Adam Topaz]

You can take $\mathbb{C}$ with the norm $\| a\| = max(|a|,|a|_0)$ where $|-|_0$ is the trivial norm (sends every nonzero element to 1) and $|-|$ is the usual absolute value.
Then $\|(1/3) \cdot 2 \| = 1$ and $\| 1/3 \|\cdot \|2 \|= 2$.

[Adam Topaz]

These normed ring/field instances are a mess. There is the issue you pointed out, but also the issue that it extends a ring/field structure. Presumably it should be a mixin similar to topological_ring, etc. And maybe the (sub)multiplicative conditions should be mixins as well?

[Eric Wieser]

I don't think we need separate mixins for the multiplicative stuff, but I do think that the hierarchy of normed classes should require the relevant algebra classes and not extend them.

[Eric Wieser]

That idea has come up multiple times, and in the past has been rejected due to verbosity.

[Jireh Loreaux]

Thanks Adam, I figured there was a simple counterexample. Eric, by verbosity do you mean in the source or term size? Personally, I would be in favor of making normed classes take the algebra classes as arguments.

[Eric Wieser]

I mean in the source, but perhaps both concerns were expressed

[Eric Wieser]

I think @Sebastien Gouezel was opposed, or at least might remember what the opposition was

[Sebastien Gouezel]

Here is my feeling on this (not backed by any quantitative measurement!). When some classes are ubiquitous and used all the time to build new classes (which will again be used to build new classes), then bundling more stuff in one class (like [normed_field k] instead of [field k] [has_norm k] [is_normed_field k], say) ensures that there are less parameters in the stuff you build on top of it, making equality checking faster and avoiding exponential blowup when you build things on top of things on top of things.

normed_field is a class that definitely fits this description: it is used to build continuous linear maps, continuous multilinear maps, analytic maps, and so on.

TLDR: I'd go for completely bundled classes for the main players in the hierarchy, and mixins for less prominent properties.

[Anatole Dedecker]

I had a problem with that exactly once, which forced me to introduce the dumb typeclass docs#normed_linear_ordered_field (notice there are no compatibility conditions, this is exactly the union of two typeclasses), so it is really a problem but definitely not high priority imho

[Jireh Loreaux]

The problem I have with extending is that it leads to a bunch of extra classes we have to define. For example we have to have separate normed versions of all of the following: ring, comm_ring, non_unital_ring, non_unital_comm_ring, and for division rings I want to be able to consider both ones that satisfy norm_mul_le (for Gelfand-Mazur) and ones that satisfy norm_mul (this is the standard condition for normed_division_ring) and applies to the quaternions, for example.

Under the current setup, non_unital_normed_comm_ring doesn't even exist yet because I had trouble with timeouts that I have never gotten around to fixing, although I will need to get it working soon. It's currently impossible to have that distinction with division_rings without adding some sort of Prop mixin class is_division_ring analogous to is_field.

If we switch, then we only need a few norm type classes (subadditive, submultiplicative, multiplicative, and scalar submultiplicative, cstar_ring). All the ring versions collapse into one.

As a (minor) side benefit, it becomes possible to state certain results that are currently impossible to state in the standard way, e.g., a C-star-algebra has a unique C-star-norm; you can get around this currently by using the alternate version: injective star homomorphisms between C-star-algebras are isometric.

Now, I had thought that the issue was always one of term-size blowup, but if it's really just about source code, I would definitely prefer to switch for the reasons described above.

[Yaël Dillies]

Did you try whether the timeouts were caused by using new structures rather than old? I think using new structures for the normed hierarchy is an historical accident.

[Jireh Loreaux]

I have not checked that. I'll look into it tomorrow when I have time. Thanks.

[Sebastien Gouezel]

As I tried to say above, I think only the main players in the hierarchy should be fully bundled. I don't expect non_unital_normed_comm_ring to show up often, so having a mixin version for this one would be perfectly fine. Say that you have a mixin is_normed_semiring or whatever, then you could do [non_unital_comm_ring R] [has_norm R] [is_normed_semiring R], say. And you could define normed_field k as extends [field k] [has_norm k] [is_normed_semiring k]. I don't see any drawback to this kind of approach.

[Eric Wieser]

I don't think that type of extension is legal (at least for old style structures), but instances can be added manually to mean the same thing

[Eric Wieser]

But now you find that you don't actually end up writing many lemmas about normed_field because they hold more generally for a selection from that pile of more fine-grained typeclases

[Eric Wieser]

Which means that your "main players" end up not playing as much as they originally used to

[Eric Wieser]

(also, I don't think we currently have any motivation to separate has_norm from is_normed_semiring, the separation from the algebra bits seems to be the pain point)

[Sebastien Gouezel]

To me, the bundling is only useful when you build new definitions on top of it. For lemmas, it is better to have the fine-grained assumptions. Just like lemmas with covariant_class are perfect, but new definitions will rather build on linearly_ordered_field or whatever.

[Eric Wieser]

What sort of definition building on top of normed_field do you have in mind?

[Sebastien Gouezel]

Spaces of continuous linear maps or analytic maps, for instance.

[Eric Wieser]

What do you mean by "spaces of"? Do you have a concrete existing declaration in mind?

[Jireh Loreaux]

Sebastian, I will be working with non_unital_normed_comm_rings all the time. Any time you take a normal element in a non-unital C⋆-algebra, the continuous functional calculus is a map from continuous functions on the spectrum into the commutative and non-unital C⋆-subalgebra generated by that element. So, for me personally, this is a huge player. That's not to say that normed_fields aren't perhaps a bigger player, only that I don't think the mixin approach makes too much sense. In any case, I'll second Eric's point that really I am interested in separating the analysis classes from the algebra classes; all the normed_X classes should still extend has_norm.

[Jireh Loreaux]

Would it be possible, under the alternate paradigm, to simply define normed_field 𝕜 as simply extends field 𝕜, normed_ring' 𝕜 where normed_ring' is a normed ring where the norm is multiplicative? Would this solve your bundling issue?

[Jireh Loreaux]

Or does this not work because normed_ring' will be looking for some existing ring 𝕜 instance?

[Sebastien Gouezel]

Jireh Loreaux said:

Would it be possible, under the alternate paradigm, to simply define normed_field 𝕜 as simply extends field 𝕜, normed_ring' 𝕜 where normed_ring' is a normed ring where the norm is multiplicative? Would this solve your bundling issue?

Yes, I said two messages above that it seems completely viable to me to have mixins, and bundle some on them in the definition of normed_field. But the best answer would certainly be to try the refactor, and see if it creates a lot of timeouts or not. If it doesn't, them I would be fine with separating the algebra classes and the normed ones!

[Eric Wieser]

After this came up again in another thread, I've made an attempt at this at #18462, feel free to push to that branch

[Eric Wieser]

\[(semi)?normed_add_comm_group appears a total of 865 times, so this is going to be quite a slog even if it goes smoothly

[Jireh Loreaux]

I may not have time until late tonight, but I'll try to have a look then.

[Eric Wieser]

It's probably worth getting consensus on:

• Whether the general idea is ok
• Whether the port (port-status#analysis/normed/group/basic) is sufficiently far away / blocked by lean4 issues that it makes sense to do this in Lean 3
  before trying to knock out all the errors

[Eric Wieser]

A clever trick would be to write a python script that parses the error messages, and automatically inserts missing instance arguments where they are now needed

[Eric Wieser]

Unfortunately this has now hit the phase of the refactor where it's running into timeouts on pi types