# Zulip Chat Archive

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

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

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