## 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)), _⟩,
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,
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,
have : ∑ (x : M) in {m}, (c1 + finsupp.single m a) x • x = a • m,
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],
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,


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],
{ 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,
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],
{ 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), _),
ext m s,
simp [mul_smul r s m] },
{ exact (((smul_add_hom R M).flip) m).map_zero } } }
end


PR #6457

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],
{ 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), _),
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)), _⟩,
-- 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,
-- 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 [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,
-- next, we split the other sum
-- now we clear a • m1 and one of the sums, since they are equal on both sides
-- 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 smulling 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!

Thanks!

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

Oh lol, I didn't use finsupp.coe_smulbecause 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).

#### 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