search

math-comp / analysis

Mathematical Components compliant Analysis Library
Other
201 stars 44 forks source link

Endow R^o, C^o (which are copies of R, C) with structures #156

Open amahboubi opened 5 years ago

amahboubi commented 5 years ago

For now it is not clear how to proceed: is it broken or is documentation missing? Many lines in this file declare instances for C^o, using its convertibility with C but I still do not understand how things are supposed to work, now or after PR#270 in math-comp.

mkerjean commented 4 years ago

I would like to update this issue and suggest to remove the notation ^o for analysis.

In the current state of the library (branch mathcomp_master), the tag ^o is the only way to have a topology on a numFieldType as well as a lmodType structure on it.

As I see it, while it is understandable that no canonical algebra structure should be put on a ring, this became less clear in the case of fields, especially if one wants to deal with analysis. A function linear on C (resp. R) is always supposed to be linear with respect to C (resp. R) as underlying field, if not explicitly mentioned otherwise.

Moreover, the fact that when K is a numField (or a variant) only K^o has a topology and not K seems problematic. In certain cases, which may be related to PR#90 it leads to multiplication of the tags ^o on a single type.

The solution would be the creation of an copy of the structure numField endowed by inheritance with a lmodType structure and a pseudoMetricNormedZmodType structure.

What do you think ?

affeldt-aist commented 3 years ago

It is my understanding that PR #205 will "fix" this issue, right?