Zulip Chat Archive

Stream: new members

Topic: submodule.span as_sum


view this post on Zulip 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

view this post on Zulip Alex J. Best (Feb 26 2021 at 20:08):

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

view this post on Zulip Damiano Testa (Feb 26 2021 at 20:18):

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

view this post on Zulip 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).

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 13:33):

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

view this post on Zulip 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!

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 13:40):

You should be using finsupp.sum I think

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 13:40):

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

view this post on Zulip 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:

view this post on Zulip Damiano Testa (Feb 27 2021 at 13:41):

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

view this post on Zulip 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

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Feb 27 2021 at 13:42):

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

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip 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?

view this post on Zulip 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!

view this post on Zulip Scott Morrison (Feb 27 2021 at 13:56):

(smul_add_hom R M).flip m

view this post on Zulip 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.

view this post on Zulip 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!)

view this post on Zulip 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...

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 27 2021 at 16:30):

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

view this post on Zulip 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

view this post on Zulip Damiano Testa (Feb 27 2021 at 17:22):

PR #6457

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 17:28):

Thanks!

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:10):

actually, this is what I was doing:

  obtain c, csup, rfl := span_as_sum_mine hm,

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:10):

I could try with explicit type ascription.

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 18:11):

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

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:12):

Yes, some max {...} weirdness

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 18:13):

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

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:13):

Type ascription is not looking good either

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (Feb 27 2021 at 18:15):

My version doesn't have the universe issues

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:17):

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

view this post on Zulip 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.

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:20):

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

view this post on Zulip 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.

view this post on Zulip 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!

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:23):

Thanks!

view this post on Zulip 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).

I asked about the universe issue in #general

view this post on Zulip Damiano Testa (Feb 27 2021 at 18:34):

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

I saw the universe issue question, thanks!

view this post on Zulip Eric Wieser (Feb 27 2021 at 19:04):

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

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Mar 01 2021 at 18:41):

Yeah Alex pointed that out ages ago


Last updated: May 18 2021 at 16:25 UTC