# Zulip Chat Archive

## Stream: new members

### Topic: submodule.span as_sum

#### Damiano Testa (Feb 26 2021 at 19:24):

Dear All,

is something like the lemma below already available in mathlib?

Thanks!

```
import linear_algebra.basis
open_locale big_operators
lemma submodule.span_as_sum {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
(m : M) (s : set M) (hm : m ∈ submodule.span R s) :
∃ su : finset M, ∃ c : M →₀ R,
c.support = su ∧ (c.support : set M) ⊆ s ∧ ((∑ i in su, c i • i) = m) :=
begin
sorry
end
```

#### Alex J. Best (Feb 26 2021 at 20:08):

I think the forward direction of docs#finsupp.mem_span_iff_total might help?

#### Damiano Testa (Feb 26 2021 at 20:18):

Thank you, this seems very close to what I want!

#### Kevin Buzzard (Feb 26 2021 at 20:59):

You could probably drop `su`

completely and just sum over `c.support`

(assuming this is a `finset`

).

#### Damiano Testa (Feb 26 2021 at 21:13):

Kevin, yes, thanks! I initially have a version where the support of `c`

was contained in `su`

, but not necessarily equal to it, since it seemed useful, but then I managed to prove it in this form and did not look back at it. You are right that, as is, `su`

is determined by everything else!

#### Damiano Testa (Feb 27 2021 at 07:09):

It is not pretty, but it works...

```
lemma submodule.span_as_sum {R : Type*} [semiring R] [semimodule R M]
(m : M) (s : set M) (hm : m ∈ submodule.span R s) :
∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (∑ i in c.support, c i • i) = m :=
begin
obtain ⟨T, Tv, mT⟩ := mem_span_finite_of_mem_span hm,
revert mT Tv m s,
refine finset.induction_on T (λ m s ms es me, ⟨0, by simpa [eq_comm] using me⟩) _,
refine λ m S ms ih m1 s m1s ims m1i, _,
rw [finset.coe_insert] at m1i,
choose a z hz ide using mem_span_insert.mp m1i,
subst ide,
obtain ⟨c1, c1ss, rfl⟩ := ih z S hz rfl.subset hz,
by_cases a0 : a = 0,
{ refine ⟨c1, λ g hg, ims (finset.mem_insert_of_mem (c1ss hg)), _⟩,
rw [a0, zero_smul, zero_add] },
have mc1 : m ∉ c1.support := λ h, ms (finset.mem_coe.mp (set.mem_of_mem_of_subset h c1ss)),
refine ⟨c1 + finsupp.single m a, λ h hs, ims _, _⟩,
{ rw [finset.mem_coe, finset.insert_eq, finset.mem_union, finset.mem_singleton],
obtain F : h = m ∨ h ∈ c1.support.val := by simpa [finsupp.support_single_ne_zero a0,
finset.union_comm] using set.mem_of_mem_of_subset hs finsupp.support_add,
cases F,
{ exact or.inl F },
{ exact or.inr (finset.coe_subset.mp c1ss F) } },
{ clear m1i m1s hz ih,
have dc1m : disjoint c1.support (finsupp.single m a).support,
{ rw [finsupp.support_single_ne_zero a0],
exact finset.disjoint_singleton.mpr mc1 },
have cpa : (c1 + finsupp.single m a).support = c1.support ∪ {m},
{ ext x,
rw ← finsupp.support_single_ne_zero a0,
refine ⟨λ h, finsupp.support_add h, λ h, _⟩,
refine finset.mem_of_subset (eq.subset _) h,
rw finsupp.support_add_eq dc1m },
have : ∑ (x : M) in {m}, (c1 + finsupp.single m a) x • x = a • m,
{ rw [finset.sum_singleton, finsupp.coe_add, pi.add_apply, add_smul, finsupp.single_eq_same],
refine add_left_eq_self.mpr _,
rw [finsupp.not_mem_support_iff.mp mc1, zero_smul] },
rw [cpa, finset.sum_union (by rwa finsupp.support_single_ne_zero a0 at dc1m), add_comm],
rw [this, finsupp.coe_add],
simp_rw [pi.add_apply, add_smul, finset.sum_add_distrib],
refine (add_right_inj _).mpr (add_right_eq_self.mpr _),
refine finset.sum_eq_zero (λ x xc1, _),
convert zero_smul _ x,
rw [← finsupp.not_mem_support_iff, finsupp.support_single_ne_zero a0, finset.not_mem_singleton],
rintros rfl,
exact mc1 xc1 }
end
```

#### Kevin Buzzard (Feb 27 2021 at 13:10):

Damiano surely the first line is ` apply span_induction hm,`

and then you should have four straightforward goals.

#### Kevin Buzzard (Feb 27 2021 at 13:10):

If you can't get it from what is already there then it should be straightforward to prove directly by induction.

#### Kevin Buzzard (Feb 27 2021 at 13:33):

I'm trying it and it seems a bit shorter but it's still a struggle :-(

#### Damiano Testa (Feb 27 2021 at 13:39):

I agree, it puts stuff in the right places, but the proof does not seem much shorter. It is more "guided", certainly!

#### Kevin Buzzard (Feb 27 2021 at 13:40):

You should be using `finsupp.sum`

I think

#### Kevin Buzzard (Feb 27 2021 at 13:40):

Of course in my opinion you should be avoiding finsets completely and using finsum ;-)

#### Damiano Testa (Feb 27 2021 at 13:41):

ok, but, to be honest, I lost the strength to continue with this, now that it is proved and proof irrelevance will not look at how... :smile:

#### Damiano Testa (Feb 27 2021 at 13:41):

Besides, this is simply a step to prove something for the liquid project

#### Kevin Buzzard (Feb 27 2021 at 13:42):

Your goal is `∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (finsupp.sum c (λ m r, r • m)) = m`

#### Damiano Testa (Feb 27 2021 at 13:42):

I can now prove that if, in a Z-module with a pairing, you take the dual of a set containing a basis, then the dual is entirely on one side of a hyperplane!

#### Damiano Testa (Feb 27 2021 at 13:42):

Not especially exciting, but it is getting the machinery working for lattice stuff

#### Damiano Testa (Feb 27 2021 at 13:44):

Ok, I may give this `finsupp.sum`

instead of `finset.sum`

a go, but later. I actually did not know that there was a difference and simply went for what Lean accepted as a well-formed statement and that was correct mathematically...

#### Kevin Buzzard (Feb 27 2021 at 13:45):

`finsupp.sum`

is much better because it knows the key fact that summing over `support f`

is the same as summing over any set containing `support f`

.

#### Damiano Testa (Feb 27 2021 at 13:46):

Ah, this would save indeed a few lines, certainly towards the bottom of the proof, and likely earlier than that as well!

#### Kevin Buzzard (Feb 27 2021 at 13:52):

Another trick with `finsupp.sum`

(which I'm learning as I'm proving) is that it's better to work with

```
def foo {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M] (m : M) :
R →+ M :=
{ to_fun := λ r, r • m,
map_zero' := zero_smul _ m,
map_add' := λ x y, add_smul x y m}
```

Does this map already have a name?

#### Damiano Testa (Feb 27 2021 at 13:56):

Is this the "orbit of `m`

" map? I am simply trying to parse the math side, not implying that if it is, then I know what it is in Lean!

#### Scott Morrison (Feb 27 2021 at 13:56):

`(smul_add_hom R M).flip m`

#### Kevin Buzzard (Feb 27 2021 at 13:57):

Thanks Scott. The reason it's useful is that stuff like docs#finsupp.sum_add_index' needs not just that the map you're summing over is M -> R -> M but M -> R ->+ M.

#### Kevin Buzzard (Feb 27 2021 at 14:28):

Here's my effort:

```
import linear_algebra.basis
open submodule
open_locale big_operators classical
open finsupp
lemma submodule.span_as_sum {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
(m : M) (s : set M) (hm : m ∈ submodule.span R s) :
∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (∑ i in c.support, c i • i) = m :=
begin
change ∃ c : M →₀ R, (c.support : set M) ⊆ s ∧
(finsupp.sum c (λ m, (smul_add_hom R M).flip m)) = m,
apply span_induction hm; clear hm m,
{ intros m hm,
use finsupp.single m 1,
split,
{ intros x hx,
rw [finset.mem_coe, mem_support_single] at hx,
rwa hx.1 },
{ simp } },
{ use 0,
simp },
{ rintros x y ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩,
use c + d,
split,
{ refine set.subset.trans _ (set.union_subset hc hd),
rw [← finset.coe_union, finset.coe_subset],
exact support_add },
{ simp } },
{ rintros r m ⟨c, hc, rfl⟩,
use r • c,
split,
{ intros x hx,
apply hc,
rw [finset.mem_coe, mem_support_iff] at hx ⊢,
intro h1, apply hx,
simp [h1] },
{ rw sum_smul_index', swap, simp,
convert (add_monoid_hom.map_finsupp_sum (smul_add_hom R M r) _ _).symm,
ext m s,
simp [mul_smul r s m] } },
end
```

It taught me a bunch about `finsupp.sum`

(e.g. its existence!)

#### Kevin Buzzard (Feb 27 2021 at 14:32):

I wonder if it would have been less painful if the support was just a set -- several times I had to do a finset <-> set dance. The goal is (exists x, X and Y) so after the induction and the split there are eight goals; each one only took a few lines but it all adds up...

#### Damiano Testa (Feb 27 2021 at 15:40):

Thanks Kevin! I like how structured your proof is. Besides, it can be broken into 4 shorter lemmas, which is good!

Do you think it should be in mathlib? I am using it in `toric`

.

#### Kevin Buzzard (Feb 27 2021 at 16:25):

Whenever I see a lemma like this I wonder whether in fact it's needed in the intended application or whether one can get away with just doing induction. I would definitely consider changing the statement of the lemma to what I `change`

it to on line 1, but I don't see why it can't go in mathlib, I would imagine that there's a better way of proving `r • (c x) ≠ 0 -> (c x) ≠ 0`

rather than `intro h1, apply hx, simp [h1]`

but everything else looks OK to me.

#### Damiano Testa (Feb 27 2021 at 16:30):

Does `rw [finsupp.coe_smul] at hx, exact right_ne_zero_of_mul hx`

appear better?

#### Damiano Testa (Feb 27 2021 at 16:43):

If it seems alright, this is a slightly shortened version of your proof that, I think, is still readable. I could compress it further, but not much, I think.

```
lemma submodule.span_as_sum {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
{m : M} {s : set M} (hm : m ∈ submodule.span R s) :
∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (c.sum (λ m, (smul_add_hom R M).flip m)) = m :=
begin
refine span_induction hm (λ x hx, _) ⟨0, by simp⟩ _ _; clear hm m,
{ refine ⟨finsupp.single x 1, λ y hy, _, by simp⟩,
rw [finset.mem_coe, mem_support_single] at hy,
rwa hy.1 },
{ rintros x y ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩,
refine ⟨c + d, _, by simp⟩,
refine set.subset.trans _ (set.union_subset hc hd),
rw [← finset.coe_union, finset.coe_subset],
exact support_add },
{ rintros r m ⟨c, hc, rfl⟩,
refine ⟨r • c, λ x hx, hc _, _⟩,
{ rw [finset.mem_coe, mem_support_iff] at hx ⊢,
rw [finsupp.coe_smul] at hx,
exact right_ne_zero_of_mul hx },
{ rw sum_smul_index' (λ (m : M), _),
{ convert (add_monoid_hom.map_finsupp_sum (smul_add_hom R M r) _ _).symm,
ext m s,
simp [mul_smul r s m] },
{ exact (((smul_add_hom R M).flip) m).map_zero } } }
end
```

#### Damiano Testa (Feb 27 2021 at 17:22):

PR #6457

#### Kevin Buzzard (Feb 27 2021 at 17:28):

Thanks!

#### Damiano Testa (Feb 27 2021 at 17:32):

No problem!

In the actual version, I begun the proof with a `classical`

, since otherwise some of the finsets would complain.

I agree that using the definition of the submodule spanned as "the infimum of the submodules [...]" should be the standard approach, but sometimes I think that using linear combinations can be simpler/shorter.

#### Damiano Testa (Feb 27 2021 at 17:54):

The other notable difference, is that I made implicit the assumptions `{m : M}`

and `{s : set M}`

, since they can be read off from the last assumption `(hm : m ∈ submodule.span R s)`

.

(This change already appears in the shortened version above.)

#### Damiano Testa (Feb 27 2021 at 18:07):

Something strange happens with `M`

when I try to apply Kevin's version. This is what the checks say:

```
-- Kevin's formulation
#check @submodule.span_as_sum
submodule.span_as_sum :
∀ {R : Type u_1} {M : Type (max u_2 u_3)} [_inst_1 : semiring R] [_inst_2 : add_comm_group M]
[_inst_3 : semimodule R M] {m : M} {s : set M},
m ∈ span R s →
(∃ (c : M →₀ R), ↑(c.support) ⊆ s ∧ c.sum (λ (i : M), ⇑(⇑((smul_add_hom R M).flip) i)) = m)
-- original formulation
#check @submodule.span_as_sum_mine
submodule.span_as_sum_mine :
∀ {R : Type u_1} {M : Type u_2} [_inst_1 : semiring R] [_inst_2 : add_comm_group M] [_inst_3 : semimodule R M]
{m : M} {s : set M},
m ∈ span R s → (∃ (c : M →₀ R), ↑(c.support) ⊆ s ∧ ∑ (i : M) in c.support, ⇑c i • i = m)
```

This actually means that I can apply the older version, but not the newer one. Am I doing something wrong?

#### Kevin Buzzard (Feb 27 2021 at 18:09):

Try `refine`

-- `apply`

isn't always as smart as it could be. But it could be the problem with the smul_add_hom. I bet `convert`

works.

#### Damiano Testa (Feb 27 2021 at 18:10):

actually, this is what I was doing:

```
obtain ⟨c, csup, rfl⟩ := span_as_sum_mine hm,
```

#### Damiano Testa (Feb 27 2021 at 18:10):

I could try with explicit type ascription.

#### Kevin Buzzard (Feb 27 2021 at 18:11):

oh wait what -- you have universe issues, right?

#### Damiano Testa (Feb 27 2021 at 18:12):

Yes, some `max {...}`

weirdness

#### Kevin Buzzard (Feb 27 2021 at 18:13):

That's the problem, Lean won't be able to unify the universes

#### Damiano Testa (Feb 27 2021 at 18:13):

Type ascription is not looking good either

#### Kevin Buzzard (Feb 27 2021 at 18:14):

I can't even get your version of my proof to compile -- can you post a MWE?

#### Kevin Buzzard (Feb 27 2021 at 18:15):

My version doesn't have the universe issues

#### Damiano Testa (Feb 27 2021 at 18:15):

```
import linear_algebra.basis
open submodule
open_locale big_operators classical
open finsupp
lemma submodule.span_as_sum {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
{m : M} {s : set M} (hm : m ∈ submodule.span R s) :
∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (c.sum (λ i, (smul_add_hom R M).flip i)) = m :=
begin
refine span_induction hm (λ x hx, _) ⟨0, by simp⟩ _ _; clear hm m,
{ refine ⟨finsupp.single x 1, λ y hy, _, by simp⟩,
rw [finset.mem_coe, mem_support_single] at hy,
rwa hy.1 },
{ rintros x y ⟨c, hc, rfl⟩ ⟨d, hd, rfl⟩,
refine ⟨c + d, _, by simp⟩,
refine set.subset.trans _ (set.union_subset hc hd),
rw [← finset.coe_union, finset.coe_subset],
exact support_add },
{ rintros r m ⟨c, hc, rfl⟩,
refine ⟨r • c, λ x hx, hc _, _⟩,
{ rw [finset.mem_coe, mem_support_iff] at hx ⊢,
rw [finsupp.coe_smul] at hx,
exact right_ne_zero_of_mul hx },
{ rw sum_smul_index' (λ (m : M), _),
{ convert (add_monoid_hom.map_finsupp_sum (smul_add_hom R M r) _ _).symm,
ext m s,
simp [mul_smul r s m] },
{ exact (((smul_add_hom R M).flip) m).map_zero } } }
end
/- Ideally, I would be able to prove this using the lemma above, but I cannot... -/
lemma submodule.span_as_sum_mine {R M : Type*} [semiring R] [add_comm_group M] [semimodule R M]
{m : M} {s : set M} (hm : m ∈ submodule.span R s) :
∃ c : M →₀ R, (c.support : set M) ⊆ s ∧ (∑ i in c.support, c i • i) = m :=
begin
-- the element `m` is in the span of `s`, if it is in the span of a finite subset `T ⊆ s`
obtain ⟨T, Tv, mT⟩ := mem_span_finite_of_mem_span hm,
-- now that we know that our element `m` is in the span of `T ⊆ S`, we no longer need to carry
-- around that it is also in the span of `S`
clear hm,
-- prepare for doing induction on
revert m s,
-- induction on the finset `T`: the base case `T = ∅` is trivial.
refine finset.induction_on T (λ m s es me, ⟨0, by simpa [eq_comm] using me⟩) _,
-- clear unneded clutter (not sure why this did not go away on its own)
clear T,
-- induction step: we add an element `m1` to the finset `T`, we have an element `m`
-- in the span of `T ∪ {m1}`
refine λ m1 T m1T ih m s ims m1i, _,
-- move sets/finsets around
rw [finset.coe_insert] at m1i,
-- we isolate the coefficient `a` of `m1`
obtain ⟨a, z, hz, rfl⟩ : ∃ (a : R) (z : M) (H : z ∈ span R ↑T), m = a • m1 + z :=
mem_span_insert.mp m1i,
-- apply the induction hypothesis to obtain the coefficients for the elements of `T`
obtain ⟨c1, c1ss, rfl⟩ : ∃ (c : M →₀ R), (c.support) ⊆ T ∧ ∑ (i : M) in c.support, c i • i = z :=
ih rfl.subset hz,
-- separate the cases in which the coefficient `a` of the "new" element `m1` vanishes...
by_cases a0 : a = 0,
{ -- in this case, the coefficients that we get by induction work straight away
refine ⟨c1, λ g hg, ims (finset.mem_insert_of_mem (c1ss hg)), _⟩,
rw [a0, zero_smul, zero_add] },
-- or the new coefficient `a` is non-zero
-- the new element `m1` is not in the support of the coefficients for `m` arising from the
-- induction hypothesis
have mc1 : m1 ∉ c1.support := λ h, m1T (finset.mem_coe.mp (set.mem_of_mem_of_subset h c1ss)),
-- by construction, the support of `c1` does not contain `m1`
have dc1m : disjoint c1.support (finsupp.single m1 a).support,
{ rw [finsupp.support_single_ne_zero a0],
exact finset.disjoint_singleton.mpr mc1 },
-- moreover, the involved coefficients are really the coefficients appearing in the support
-- of `c1` and `{m1}`
have cpa : (c1 + finsupp.single m1 a).support = c1.support ∪ {m1},
{ ext x,
rw ← finsupp.support_single_ne_zero a0,
refine ⟨λ h, finsupp.support_add h, λ h, _⟩,
refine finset.mem_of_subset (eq.subset _) h,
rw finsupp.support_add_eq dc1m },
-- of course, `m` is the sum of the coefficients coming from the induction and
-- the new coefficient `a` for `m1`
refine ⟨c1 + finsupp.single m1 a, λ h hs, ims _, _⟩,
-- make sure that the support is still contained in `T ∪ {m1}`
{ -- we use `hs`, once we undo trivialities
rw [cpa, finset.union_comm] at hs,
refine set.mem_of_mem_of_subset hs _,
rw [← finset.insert_eq, finset.coe_insert, finset.coe_insert],
exact set.insert_subset_insert c1ss },
-- in this branch, we show that the element `m` really is the sum that we claim it is
{ -- remove clutter from the proof
clear m1i m1T hz ih,
-- a complicated way of writing `a • m1`, as a sum over the singleton `{m1}`
have : ∑ (x : M) in {m1}, (c1 + finsupp.single m1 a) x • x = a • m1,
{ rw [finset.sum_singleton, finsupp.coe_add, pi.add_apply, add_smul, finsupp.single_eq_same],
refine add_left_eq_self.mpr _,
rw [finsupp.not_mem_support_iff.mp mc1, zero_smul] },
-- we start by matching up term, first one of the sums equals `a • m1`
rw [cpa, finset.sum_union (by rwa finsupp.support_single_ne_zero a0 at dc1m), add_comm,
this, finsupp.coe_add],
-- next, we split the other sum
simp_rw [pi.add_apply, add_smul, finset.sum_add_distrib],
-- now we clear `a • m1` and one of the sums, since they are equal on both sides
refine (add_right_inj _).mpr (add_right_eq_self.mpr _),
-- we show that the remaining sum vanishes, by showing that all its terms vanish
refine finset.sum_eq_zero (λ x xc1, _),
-- it suffices to show that we are `smul`ling by `0`
convert zero_smul _ x,
-- for this, it suffices to show that `x` is not equal to `m1`
rw [← finsupp.not_mem_support_iff, finsupp.support_single_ne_zero a0, finset.not_mem_singleton],
-- since `x` is in the support of `c1`, it follows that `x ≠ m1`, the proof is by contradiction
rintros rfl,
exact mc1 xc1 }
end
#check @submodule.span_as_sum
#check @submodule.span_as_sum_mine
```

#### Damiano Testa (Feb 27 2021 at 18:15):

These are your proof first, then mine. I changed your statement to the statement after the `change`

in your original proof.

#### Damiano Testa (Feb 27 2021 at 18:17):

In my VSCode, they compile. I am on `toric`

in lean liquid

#### Kevin Buzzard (Feb 27 2021 at 18:17):

```
open finsupp
universe u
lemma submodule.span_as_sum {R : Type*} {M : Type u} [semiring R] ...
```

seems to fix the universe issues. No idea what's going on there.

#### Damiano Testa (Feb 27 2021 at 18:20):

This is very strange. Should I then change the PR as well?

#### Kevin Buzzard (Feb 27 2021 at 18:20):

With universes on, the `M : Type*`

version of mine compiles to

```
submodule.span_as_sum.{u_1 u_2 u_3} :
∀ {R : Type u_1} {M : Type (max u_2 u_3)} [_inst_1 : semiring.{u_1} R] [_inst_2 : add_comm_group.{(max u_2 u_3)} M]
[_inst_3 : semimodule.{u_1 (max u_2 u_3)} R M] {m : M} {s : set.{(max u_2 u_3)} M},
m ∈ span.{u_1 (max u_2 u_3)} R s →
(∃ (c : M →₀ R),
↑(c.support) ⊆ s ∧ c.sum (λ (i : M), ⇑(⇑((smul_add_hom.{u_1 (max u_2 u_3)} R M).flip) i)) = m)
```

so it introduces three universes but never spots that `max u_2 u_3`

is the only time `u_2`

and `u_3`

are used.

#### Damiano Testa (Feb 27 2021 at 18:23):

Yes, it does compile, but I could not apply it.

In any case, I added the explicit universe in the PR as well and now I can apply it in my other file!

#### Damiano Testa (Feb 27 2021 at 18:23):

Thanks!

#### Kevin Buzzard (Feb 27 2021 at 18:31):

Oh lol, I didn't use `finsupp.coe_smul`

because my mathlib was 2 days old and it was added yesterday :P (that's why your version of my proof didn't compile for me).

I asked about the universe issue in #general

#### Damiano Testa (Feb 27 2021 at 18:34):

The importance of a fresh copy of mathlib... Ahaha

I saw the universe issue question, thanks!

#### Eric Wieser (Feb 27 2021 at 19:04):

It's nice to see lemmas I add being used immediately :)

#### Eric Wieser (Mar 01 2021 at 18:23):

Turns out the proof of the lemma was:

```
begin
conv_lhs { rw ←set.image_id s },
simp_rw ←exists_prop,
exact finsupp.mem_span_iff_total R,
end
```

docs#finsupp.mem_span_iff_total

#### Kevin Buzzard (Mar 01 2021 at 18:41):

Yeah Alex pointed that out ages ago

Last updated: May 18 2021 at 16:25 UTC