Separate Normed Module's ring and norm types

[zstone1]

Long story short, I want to work with modules over the complex numbers, but have the norms live in the real numbers. Things like infs and sups are defined only for realType, which makes sense. But in order to access those lemma, I must work over an R-module. This is not great.

I believe the problem is at the boundary of PseudoMetricNormedZmodule and NormedModule. The implementation of PseudoMetricNormedZmodule make sense. But when it comes to NormedModule, I'm forced to have scalars over the same ring as the norm. The fact that numDomain has a partial order is not good enough in practice, because I can't access any of the inf/sup facts, archimedian facts, ect.

I'm hoping that you guys have thought about the matter, and have a plan for it. If not I can imagine a handful of solutions. I'm happy to propose a solution and implement it, I just want to make sure I'm doing work that is inline your roadmap here.

[affeldt-aist]

@mkerjean has been experimenting with a norm over complex numbers and a real codomain: https://leanprover-community.github.io/lt2021/slides/kerjean_slides_lean21.pdf

[zstone1]

Defining complex holomorphic in terms of the cauchy Riemann equations is quite nice. This works well when working only in C because multiplication is the same as scaling. But if I want to define the spectrum, I need to work in a complex algebra, and I really need to scale by a complex number. Perhaps a suitable approach here is a CNormedModule R which is a NormedModule R, along with a new scaling opp over R[i].You'd end up with a mixin like

cscale : R[i] -> V -> V
ax1 : `|cscale z x| = Re`|x| * `|x|
ax2 : cscale( (r +i* 0) x = r *: x

This seems sufficient, and somewhat unintrusive. Lastly, you can show that a CNormedModule R is a NormedModule R[i]. I wonder if making that canonical would allow coq infer the right scaling in both R and R[i] cases....

I'd need to also build the CNormedAlgebra, and CBanachAlgebra to do any meaningful spectral theory, but that's not so bad. I may make a pull request with a candidate for this.

Now this approach isn't general enough for people who do analysis over the p-adic numbers, for example. Perhaps that's ok for now.

[zstone1]

Turns out the approach above is doomed. Coercions don't behave like I want. In particular, I want a coercion from CNormedModule.class_of >-> NormedModule.class_of R and CNormedModule.class_of >-> NormedModule.class_of C. Turns out this is impossible, as Coq will only accept one coercion for NormedModule.class_of. I'll need something a bit more creative, unfortunately.

[CohenCyril]

I have a prototype of canonical module over two different rings (R and C) here https://github.com/math-comp/real-closed/blob/complex_both_modules/theories/complex.v#L344-L366

It's indeed quite involved since canonical structures admit only one solution per projection. The idea is to dispatch the search, by cascading the inference. Unfortunately this is a pretty heavy machinery and we might start deploying it only when HB supports it, which is a middle to longterm goal...

So for the time being, we can use type aliases... as in @mkerjean development

[zstone1]

A question about prioritizing this work. It's possible to do this while we do the port to HB. However, doing it the traditional module theory way will require defining a normed-ring, a significant addition to the hierarchy. Instead of doing everything in !698, we could do it in three passes: first port the normedType code "as-is", then introduce a normed-ring structure. then generalize the existing structure. Is this a sensible approach? Or is it better to work specifically with a module over R or C structure?