submodule.span as_sum

Stream: new members

[Damiano Testa]

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]

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

[Damiano Testa]

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

[Kevin Buzzard]

You could probably drop su completely and just sum over c.support (assuming this is a finset).

[Damiano Testa]

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]

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]

Damiano surely the first line is apply span_induction hm, and then you should have four straightforward goals.

[Kevin Buzzard]

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

[Kevin Buzzard]

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

[Damiano Testa]

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

[Kevin Buzzard]

You should be using finsupp.sum I think

[Kevin Buzzard]

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

[Damiano Testa]

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]

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

[Kevin Buzzard]

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

[Damiano Testa]

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]

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

[Damiano Testa]

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]

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]

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

[Kevin Buzzard]

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]

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]

(smul_add_hom R M).flip m

[Kevin Buzzard]

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]

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]

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]

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]

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]

Does rw [finsupp.coe_smul] at hx, exact right_ne_zero_of_mul hx appear better?

[Damiano Testa]

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]

PR #6457

[Kevin Buzzard]

Thanks!

[Damiano Testa]

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]

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]

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]

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]

actually, this is what I was doing:

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

[Damiano Testa]

I could try with explicit type ascription.

[Kevin Buzzard]

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

[Damiano Testa]

Yes, some max {...} weirdness

[Kevin Buzzard]

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

[Damiano Testa]

Type ascription is not looking good either

[Kevin Buzzard]

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

[Kevin Buzzard]

My version doesn't have the universe issues

[Damiano Testa]

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]

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

[Damiano Testa]

In my VSCode, they compile. I am on toric in lean liquid

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

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]

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]

Thanks!

[Kevin Buzzard]

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).

I asked about the universe issue in #general

[Damiano Testa]

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

I saw the universe issue question, thanks!

[Eric Wieser]

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

[Eric Wieser]

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]

Yeah Alex pointed that out ages ago