The norm of a normedModule should be valued in a realType, not in its field of scalar. Definition of subNumDomain.

[mkerjean]

Consider V : normedModType K with K : numFieldType. As of now, its norm is of type `| _ | : V -> K. However, it should be more specifically of type `| _ | : V -> R for R: realTypeand a subType of K. In particular, this will become handy in complex analysis, or allow more generality in the Hahn-Banach theorem, which, as of now, can be instantiated only on normed modules over R.

An easy way to do that is to change the definition of normedModule as such:

HB.mixin Record PseudoMetricNormedZmod_ConvexTvs_isNormedModule (C: numDomainType)
  (R : realType) V   
& PseudoMetricNormedZmod R V & ConvexTvs C V := {
  val : R -> C ;
  ival : injective val;  
  normrZ : forall (l : C) (x : V), val (`| l *: x |) = `| l | * (val `| x |) :> C
}.

However, this is a bit pedestrian as it overlooks the availability of subtypes to handle R. Sadly, the definition of subNumDomain seems to be intricate, due to duplication issues between the domain and a codomain of a norm.

Looking at the definition of NumDomain,

 #[short(type="numDomainType")]
HB.structure Definition NumDomain := { R of
     GRing.IntegralDomain R &
     NumZmodule R &
     NormedZmodule (POrderZmodule.clone R _) R &
     NumZmod_isNumRing R
  }. 

the definition of SubNumDomain should be

 #[short(type="subNumDomainType")]
HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) := 
{ U of
    SubChoice S U &
     GRing.IntegralDomain U &
     NumZmodule U &
     SubNormedZmodule (POrderZmodule.clone U _) M S U &
     NumZmod_isNumRing U
  }.

However, this triggers an error, as M is supposed to be a numDomain over M, not U. Likewise

#[short(type="subNumDomainType")]
HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) := 
{ U of
    SubChoice S U &
     GRing.IntegralDomain U &
     NumZmodule U &
     SubNormedZmodule (POrderZmodule.clone M _) M S U &
     NumZmod_isNumRing U
  }.

triggers an error, as U is supposed to be a numDomain over U, not M.

How can we solve that ? It looks like this approach of using subtypes does not work. Could this be an issue of making hierarchy-builder understand the \val : U -> M coercion between norm : U -> U and norm : M -> M when declaring the subNumDomainType structure?

@CohenCyril, maybe you have some HB magic in mind that could help us ?

[mkerjean]

I tried to change the subNormedZmodType structure by adding a coval parameter, but this does not work either, as rocq does not find the right type on val when defining subNumDomainType.

HB.mixin Record Zmodule_isSubNormed (R : porderZmodType)  (R' : porderZmodType) (coval :  R' -> R) (M : normedZmodType R)
  (S : pred M) U & SubType M S U & NormedZmodule R' U := {
  norm_valE : forall x : U, norm ((val : U -> M) x) = coval (norm x)
}.

#[short(type="subNormedZmodType")]
HB.structure Definition SubNormedZmodule (R : porderZmodType) (R' : porderZmodType) (coval :  R' -> R) 
    (M : normedZmodType R) (S : pred M) :=
  { U of SubChoice M S U & Num.NormedZmodule R U & GRing.SubZmodule M S U
       & @Zmodule_isSubNormed R R' coval M S U }.

[...]

#[short(type="subNumDomainType")]
  HB.structure Definition SubNumDomain (M : numDomainType) (S : pred M) :=
  { U of
      SubChoice M S U &  NumDomain U &
      @SubNormedZmodule (POrderZmodule.clone U _) (POrderZmodule.clone M _)  (\val) M S U
  }.

[CohenCyril]

The problem is deeper than that: when dealing with incomplete fields and spaces over incomplete fields, the norm cannot go to a realType because an incomplete field cannot have a realType as a subtype... I agree it is a problem though, and I would lean towards the following indirection: have normed spaces have there norm with codomain in the field of scalars of their field of scalars. E.g. a $R$ vector space $U$ would actually by a $R^o$ vector space hence with norm of type $U \to R$ and a $R[i]$ vector space have norm in $U \to R$. That way this would work if $R$ is a field of reals or a real closed field...
WDYT?

[mkerjean]

Thank you for your detailed answer @CohenCyril . I'm not sure I understand it entirely: do you want to instantiate every vector space on a numfield as a vector space over $R$ or $C$? Or do you want to ask $K$-normed spaces to always be defined as vector spaces over $K$, where $K$ should itself be an $R$-vector space for R : realtype ? IE do you want to ask any numdomain to be a $R$-vector space ? Is this always true in the instances we use ?
BTW the issue will also happen for topological vector spaces, as we basically replace the norm of normed vector spaces by a family of seminorms, for which we also need to take sup in their codomain - I stumbled upon it when dealing with gauge functions.

[CohenCyril]

I'm not sure I understand it entirely: do you want to instantiate every vector space on a numfield as a vector space over $R$ or $C$? Or do you want to ask $K$-normed spaces to always be defined as vector spaces over $K$, where $K$ should itself be an $R$-vector space for R : realtype ? IE do you want to ask any numdomain to be a $R$-vector space ? Is this always true in the instances we use ?

I think we I want the $K$, in the $K$-normed spaces we use in analysis, to be themselves normed $\mathbb{R}$-algebras.

[mkerjean]

To be sure, how is this different from the suggested solution, that is, defining tvs or normed spaces over K-modules, where K admits a real type as a subnumdomain? If the implications are the same (restricting the lmodules over which we are doing analysis), is there a way to make the definition of subnumdomain work ?

[CohenCyril]

I guess the difference is that it does not hardwire realType (a fundamentally classical object) in the hierarchy.

[mkerjean]

I'm not sure I understand it entirely: do you want to instantiate every vector space on a numfield as a vector space over
R
or
C
? Or do you want to ask
K
-normed spaces to always be defined as vector spaces over
K
, where
K
should itself be an
R
-vector space for R : realtype ? IE do you want to ask any numdomain to be a
R
-vector space ? Is this always true in the instances we use ?

I think we I want the K , in the K -normed spaces we use in analysis, to be themselves normed R -algebras.

Are you suggesting a new structure , joining the R-algebras and the numDomain ? Regarding your comment about hardwiring Realtype, let me just say that this was not our idea. We wanted to make the norm of a numdomain have its values into a subtype of this same numdomain, possibly itself, and instanciating this subtype with a RealType when doing analysis.

[CohenCyril]

Yes exactly. Then we are on the same page.