## Stream: new members

### Topic: Underlying coefficients from span

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

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

Let me try

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


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

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

#### Johan Commelin (Jun 17 2020 at 18:25):

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

#### Johan Commelin (Jun 17 2020 at 18:25):

What kind of error do you get?

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


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

#### Johan Commelin (Jun 17 2020 at 18:34):

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

#### Johan Commelin (Jun 17 2020 at 18:34):

I only did the first step (-;

#### Johan Commelin (Jun 17 2020 at 18:35):

You can now do cases H, or

rcases H with ⟨f, __garbage, hf⟩,


#### Johan Commelin (Jun 17 2020 at 18:35):

I think that it might be better to change my_set.

#### Barinder Singh Banwait (Jun 17 2020 at 18:35):

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

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

#### Johan Commelin (Jun 17 2020 at 18:36):

Let me try something

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

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


#### Johan Commelin (Jun 17 2020 at 18:41):

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

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


#### Johan Commelin (Jun 17 2020 at 18:44):

Now we need to extract some juice out of hf

#### Johan Commelin (Jun 17 2020 at 18:45):

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


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

#### Johan Commelin (Jun 17 2020 at 18:47):

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

#### Johan Commelin (Jun 17 2020 at 18:47):

So it deserves a prettier name (-;

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


#### Johan Commelin (Jun 17 2020 at 18:48):

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

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

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