While section function_space in topology.v allows to sum `l l' : (U -> V)`

when `V : zmodtype`

, this does not seem to extend to `l l' : { linear U -> V}`

. Are there canonical definitions missing on linear function space or am I doing something wrong ?

U and V are expected to be lmodType R

```
(* {linear U -> V} == the interface type for linear functions, i.e., a *)
(* Structure that encapsulates the linear property *)
(* for functions f : U -> V; both U and V must have *)
(* lmodType R structures, for the same R. *)
```

~~and indeed it seems to work in that case~~ (not really I mistyped \+)

Indeed, I was testing if when `U V : lmodType R`

and it fails for me :

```
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Context (R : numFieldType) (U : lmodType R) (V : lmodType R).
Variables (f g : U -> V ).
Check (f + g).
Variables (l l': {linear U -> V}).
Fail Check (l + l').
```

with

```
The term "l" has type "{linear U -> V}" while it is expected to have type
"GRing.Zmodule.sort ?V".
```

```
Goal ((l : U -> V) + l') = ((l' : U -> V) + l).
by rewrite addrC.
```

but this is not satisfactory

Can you define this?

`Canonical linear_zmodType (R : ringType) (T M : lmodType R) := ZmodType {linear T -> M} (linear_zmodMixin T M).`

This would make your example go through but I cannot right now figure out the code for linear_zmodMixin.

Yes, this is what I am doing now.

(It shouldn't be too hard if you are accustomed to ssralg, I am failing to use the notation correctly right now :-/)

But I am rusted on on ssralg structure, so it's taking me some time :-)

Same here. Please let me know.

How am I supposed to prove `Linear _ = Linear _ `

, that is the equality between two linear functions (I want to use funeqE on the underlyong functions) ?

Hi, in mathcomp core, `linear`

has to be distinguished from `'Hom(_, _)`

which is what I think you are looking for.

`linear`

is the structure to infer linearity, while `'Hom(_, _)`

is has algebraic structural properties (you can perform this addition you desperatly want on it)

The correpondance is given by the `linfun`

interface which gives you everything you need to go back and forth

This is deeply rooted in mathcomp strategic bias to be **very** conservative wrt to Coq axioms, without which it is impossible to have linearity be both a structure **and** an extensional object (because of both the absence of functional extensionality and general proof irrelevance without axioms)

Haaaaa, that's it, great, thank you very much !

Cyril Cohen said:

This is deeply rooted in mathcomp stragedic bias to be

veryconservative wrt to Coq axioms, without which it is impossible to have linearity be both a structureandan extensional object (because of both the absence of functional extensionality and general proof irrelevance without axioms)

Could that be simplified in mc-analysis or is it not possible/not worth it ?

That could totally be simplified, and I guess it would be worth it, even though it would create a lot of redundancy

but that (redundancy) is a burden we already bear...

In particular a lot of vector space theory and field extension theory is tied to `'Hom(_, _)`

and it would be really problematic to have to duplicate it...

Do you think you could live with `'Hom(_, _)`

and use `linfun`

and `lfunE`

explicitly?

Cyril Cohen said:

Do you think you could live with

`Hom(_, _)`

and use`linfun`

and`lfunE`

explicitly?

For the moment completely, it was more of a rhetorical question. Thank you for all the explanations !

Still trying to make `'Hom(_, _)`

work though, is there something to be imported ?

Just `From mathcomp Require Import vector.`

What is your problem?

oh, I see!!! You probably need a finite dimensional vector space as of today... you are not in a finite dimension context are you?

I am working with `lmodtype`

If not, there is no way around definition {linear _ -> _} as a zmodule

ok, back to canonical definitions then :-)

You can do it by subtyping, just by proving linearity is closed under addition though, as in https://github.com/math-comp/analysis/blob/18a3c6d315ffd425e13e6e9c19fce5e90f275d43/theories/lebesgue_integral.v#L625-L709

We can make a short call to get you started with this technique, or you can build it from scratch, as you prefer

I should be ok, thanks !

What is the equivalent of `FiniteSum.Build`

here ? Just `Linear `

?

(This is indeed the constructor.)

Marie Kerjean said:

What is the equivalent of

`FiniteSum.Build`

here ? Just`Linear`

?

`Linear`

is the equivalent of the 3 lines here https://github.com/math-comp/analysis/blob/18a3c6d315ffd425e13e6e9c19fce5e90f275d43/theories/lebesgue_integral.v#L631-L633

Any idea why here I need to define the linearity predicate with an explicite `GRing.Scale.op`

? If I juste declare the predicate as `Definition linear_pred : {pred U -> V} := mem [set f | linear f]. `

then `Linear (set_mem linear_pred)`

does not typecheck. Is there some classical `Hint`

that I should have ?

Your question seem to turn around the same ideas that I'm about in the mathcomp- users stream: how linearity works within mathcomp.

I was still having trouble with `linear`

as a predicate. `Definition linear_pred : {pred U -> V} := mem [set f | linear f].`

does not work while it works when unfolding the notation linear: `Definition linear_pred : {pred U -> V} := mem [set f | lmorphism_for *:%R f]`

. Is that to be expected or is there a way around it ?

I'm afraid I really don't know this area of the math-comp. I do see the problem you're describing. But if there is an straightforward solution, it's something beyond my abilities.

Marie Kerjean said:

(solved, message deleted)

Could you please restore your message and post your solution? It puzzled me and it can help people to understand what you did.

Last updated: Feb 09 2023 at 02:02 UTC