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

Activity

1. mkerjean commented on May 1, 2026

   

   mkerjean

   on May 1, 2026

   CollaboratorAuthor

   More actions

   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
     }.
   
   
2. CohenCyril commented on May 4, 2026

   

   CohenCyril

   on May 4, 2026

   Last edited by CohenCyril

   Member

   More actions

   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?
3. mkerjean commented on May 4, 2026

   

   mkerjean

   on May 4, 2026

   CollaboratorAuthor

   More actions

   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.
4. CohenCyril commented on May 4, 2026

   

   CohenCyril

   on May 4, 2026

   Last edited by CohenCyril

   Member

   More actions

   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.

   👍React with 👍1Reacted by Marie Kerjean
5. mkerjean commented on May 5, 2026

   

   mkerjean

   on May 5, 2026

   CollaboratorAuthor

   More actions

   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 ?
6. CohenCyril commented on May 5, 2026

   

   CohenCyril

   on May 5, 2026

   Member

   More actions

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

   👍React with 👍1Reacted by Marie Kerjean
7. mkerjean commented on May 8, 2026

   

   mkerjean

   on May 8, 2026

   Last edited by mkerjean

   CollaboratorAuthor

   More actions

   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.
8. CohenCyril commented on May 8, 2026

   

   CohenCyril

   on May 8, 2026

   Member

   More actions

   Yes exactly. Then we are on the same page.