Zulip Chat Archive

Stream: new members

Topic: Underlying coefficients from span


view this post on Zulip Barinder Singh Banwait (Jun 15 2020 at 18:05):

I'm trying to establish the existence of the underlying coefficients of an element of a submodule spanned by a finite set, specifically:

import ring_theory.noetherian
open submodule

open_locale big_operators

def my_set (R) [integral_domain R] (r : R) (s : R) (n : ) :=
{ x |  (c :  × ) (hy: c  (finset.nat.antidiagonal n).erase 0, n), x = r ^ c.2 * s ^ c.1 }

lemma mwe (R) [integral_domain R] (n : ) (r s : R) (s_non_zero : s  0) :
  r^n  span R (my_set R r s n)   (f :   R) (h_f: f 0 = 1),
   ij in finset.nat.antidiagonal n, f ij.1 * r ^ ij.2 * s ^ ij.1 = 0 :=
begin
  sorry,
end

It looks like finsupp.mem_span_iff_total might be relevant, but I can't seem to get it to work :cold_sweat:

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:12):

My first reaction is that maybe we should try to apply a bit more "force" to make finsupp.mem_span_iff_total behave.

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:13):

Let me try

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:16):

@Barinder Singh Banwait Voila:

begin
  intro H,
  rw  subtype.val_image_univ (my_set R r s n) at H,
  rw finsupp.mem_span_iff_total at H,
end

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:17):

The trick is that mem_span_iff_total wants to work with an indexed family, instead of a subset. So we replace my_set with the family indexed by my_set.

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:18):

huh, somehow that's not accomplishing the goal for me ... probably because i haven't git pulled mathlib in a while

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:25):

Hmm, this part of mathlib didn't change, I think.

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:25):

What kind of error do you get?

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:28):

it's not an error per se, it's just an unsolved goal. i thought that pulling latest mathlib might fix it, but still not; i've got this in my tactic state:

Tactic State
1 goal
R : Type u_1,
_inst_1 : integral_domain R,
n : ,
r s : R,
s_non_zero : s  0,
H :
   (l : subtype (my_set R r s n)  R) (H : l  finsupp.supported R R set.univ),
    (finsupp.total (subtype (my_set R r s n)) R R subtype.val) l = r ^ n
  (f :   R) (h_f : f 0 = 1),
     (ij :  × ) in finset.nat.antidiagonal n, f ij.fst * r ^ ij.snd * s ^ ij.fst = 0

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:34):

where are the coefficients in the statement of H? In the goal they're encoded by f : ℕ → R, but in H I can't quite figure out where they are ... is it the l : subtype (my_set R r s n) →₀ R?

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:34):

Ooh, sure... I didn't prove the lemma

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:34):

I only did the first step (-;

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:35):

You can now do cases H, or

rcases H with f, __garbage, hf,

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:35):

I think that it might be better to change my_set.

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:35):

right ok, thanks for clarifying and for setting me on the right path!

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:36):

Everything might become easier, if you make it a function on a suitable indexing set, and then take the span of the image of a suitable subset.

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:36):

Let me try something

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:38):

hmmm ok, well i'm open to changing my_set, though doing that will surely mean other things in my project will need fixing!

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:40):

Something like

import ring_theory.noetherian
open submodule

open_locale big_operators

variables {R : Type} [integral_domain R]

def my_set (r : R) (s : R) (n : ) :=
(finset.nat.antidiagonal n).erase 0, n

def aux (r : R) (s : R) : ( × )  R :=
λ c, r ^ c.2 * s ^ c.1

lemma mwe (R) [integral_domain R] (n : ) (r s : R) (s_non_zero : s  0) :
  r^n  span R (aux r s '' (my_set r s n))   (f :   R) (h_f: f n = 1),
   ij in finset.nat.antidiagonal n, f ij.2 * r ^ ij.2 * s ^ ij.1 = 0 :=
begin
  intro H,
  rw finsupp.mem_span_iff_total at H,
  rcases H with f, __garbage, hf,
  -- sorry
end

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:41):

As you can see, this also make mem_span_iff_total work without complaining

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:43):

lemma mwe (R) [integral_domain R] (n : ) (r s : R) (s_non_zero : s  0) :
  r^n  span R (aux r s '' (my_set r s n))   (f :   R) (h_f: f n = 1),
   ij in finset.nat.antidiagonal n, f ij.2 * r ^ ij.2 * s ^ ij.1 = 0 :=
begin
  intro H,
  rw finsupp.mem_span_iff_total at H,
  rcases H with f, __garbage, hf,
  let g :   R := λ i, if hi : i < n then f (n - i, i) else 1,
  have hg1 : g n = 1,
  { dsimp only [g], rw [dif_neg], exact lt_irrefl n },
  use [g, hg1],
  have : (0,n)  finset.nat.antidiagonal n,
  { rw finset.nat.mem_antidiagonal, erw zero_add, },
  rw  finset.insert_erase this,
  rw finset.sum_insert (finset.not_mem_erase _ _),
  erw [hg1, one_mul, pow_zero, mul_one],
  -- sorry
end

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:44):

Now we need to extract some juice out of hf

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:45):

rw [finsupp.total_apply, finsupp.sum] at hf,

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:46):

woah, there's loads here that I don't know!!! dsimp, not_mem_erase, lt_irrefl

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:47):

Oooh, also, because of this change __garbage is no longer garbage, but actually useful (-;

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:47):

So it deserves a prettier name (-;

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:48):

lemma mwe (R) [integral_domain R] (n : ) (r s : R) (s_non_zero : s  0) :
  r^n  span R (aux r s '' (my_set r s n))   (f :   R) (h_f: f n = 1),
   ij in finset.nat.antidiagonal n, f ij.2 * r ^ ij.2 * s ^ ij.1 = 0 :=
begin
  intro H,
  rw finsupp.mem_span_iff_total at H,
  rcases H with f, hf_support, hf,
  let g :   R := λ i, if hi : i < n then f (n - i, i) else 1,
  have hg1 : g n = 1,
  { dsimp only [g], rw [dif_neg], exact lt_irrefl n },
  use [g, hg1],
  have : (0,n)  finset.nat.antidiagonal n,
  { rw finset.nat.mem_antidiagonal, erw zero_add, },
  rw  finset.insert_erase this,
  rw finset.sum_insert (finset.not_mem_erase _ _),
  erw [hg1, one_mul, pow_zero, mul_one],
  rw [finsupp.total_apply, finsupp.sum] at hf,
  erw  hf,
  -- sorry
end

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:48):

Now I first need to vacuum clean the living room(-;

view this post on Zulip Barinder Singh Banwait (Jun 17 2020 at 18:49):

you've been a massive help Johan! i'm going need to digest all of this

view this post on Zulip Johan Commelin (Jun 17 2020 at 18:49):

Btw, I hope I got the (n - i, i) right. You might need to swap things somewhere...


Last updated: May 08 2021 at 10:12 UTC