Are abstract vector spaces where "free L" doesn't require a finite L and use dimension computations to define the notion available somewhere?

I'm trying my hand at something simple, but not managing to get along that well:

```
Lemma free_by_inj: forall n: nat, forall L:n.-tuple E, injective u -> free L -> free (map u L).
Proof.
move=> n L inju.
move/freeP => freeL.
apply/freeP.
move=> k lincomb0.
```

and here I'm stuck because I don't know how to express that lincomb(f)=f(lincomb). Then I'll probably be stuck expressing that f(lincomb)=0 means lincomb=0... but then I'll know I'll be able to apply my freeL hypothesis and win.

Julien Puydt said:

Are abstract vector spaces where "free L" doesn't require a finite L and use dimension computations to define the notion available somewhere?

No at the current time there is no such development, if there were, it would be in a library which accept classical logic (such as mathcomp/analysis)...

Julien Puydt said:

I'm trying my hand at something simple, but not managing to get along that well:

`Lemma free_by_inj: forall n: nat, forall L:n.-tuple E, injective u -> free L -> free (map u L). Proof. move=> n L inju. move/freeP => freeL. apply/freeP. move=> k lincomb0.`

and here I'm stuck because I don't know how to express that lincomb(f)=f(lincomb). Then I'll probably be stuck expressing that f(lincomb)=0 means lincomb=0... but then I'll know I'll be able to apply my freeL hypothesis and win.

I miss some context to answer this...

(I mean, litterally the context variables)

OK, I guessed your context, here is one way to continue your proof:

```
From mathcomp Require Import all_ssreflect all_algebra.
Local Open Scope ring_scope.
Import GRing.Theory.
Section test.
Variables (R : fieldType) (E : vectType R).
Lemma map_free (u : {linear E -> E}) (n : nat) (vs : n.-tuple E) :
injective u -> free vs -> free (map u vs).
Proof.
move=> inju freeL; apply/freeP => k /= /eqP.
under eq_bigr do rewrite (nth_map 0) ?size_tuple// -linearZ.
by rewrite -linear_sum raddf_eq0// => /eqP; apply: freeP.
Qed.
End test.
```

Thus, the missing pieces you were asking for were `linear_sum`

and `raddf_eq0`

, which are both generic theorems about linear and additive maps.

Thanks! I'll have to study it: I think (nth_map 0) makes no sense for me, the "under eq_bigr do ..." isn't familiar, and I'm pretty sure at some point I knew why apply and apply: were different. You guessed my environment quite right ; the only difference is that I had (R: fieldType) (E F: vectType R) (u: 'Hom(E, F)) because I didn't want an endomorphism.

Ok, why is the freeP lemma expressed with = 0 while the raddf_eq0 is expressed with == 0?

That is the reason why the proof has several /eqP. That's not what bothers me the most, but I'm starting with what seem more low-hanging fruits

Let me rewrite the example with comments to be clearer on what I get (or not) from the various steps:

```
From mathcomp Require Import all_ssreflect all_algebra.
Local Open Scope ring_scope.
Import GRing.Theory.
Section rewrite_from_Cyril_Cohen.
Variables (R : fieldType) (E F : vectType R) (u : 'Hom(E, F)).
Lemma map_free (n : nat) (vs : n.-tuple E) : injective u -> free vs -> free (map u vs).
Proof.
move=> inju freeL. (* usual introductions *)
apply/freeP => k. (* classical freeness, introducing a family of scalars *)
move => /eqP. (* switch = 0 to == 0 *)
under eq_bigr do rewrite (nth_map 0) ?size_tuple//. (* unclear sum manipulation *)
under eq_bigr do rewrite -linearZ. (* linear maps are homogeneous *)
rewrite -linear_sum. (* linear maps are additive *)
rewrite raddf_eq0 //. (* classical injectivity -- uses == 0 *)
move => /eqP. (* switch back from == 0 to = 0 *)
by apply:freeP. (* recognize the goal as expressing a freeness *)
Qed.
End rewrite_from_Cyril_Cohen.
```

Ok, why is the freeP lemma expressed with = 0 while the raddf_eq0 is expressed with == 0?

This is again because of the constructive setting in mathcomp, boolean equality makes reasoning easier since equivalences are equalities (and thus can be rewritten with) and the excluded middle holds. Sometimes it is thus preferable to use `_ == _`

and sometimes `_ = _`

.

Last updated: Jul 15 2024 at 21:02 UTC