Underlying coefficients from span

Stream: new members

[Barinder Singh Banwait]

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]

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]

Let me try

[Johan Commelin]

@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]

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]

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

[Johan Commelin]

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

[Johan Commelin]

What kind of error do you get?

[Barinder Singh Banwait]

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]

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]

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

[Johan Commelin]

I only did the first step (-;

[Johan Commelin]

You can now do cases H, or

rcases H with ⟨f, __garbage, hf⟩,

[Johan Commelin]

I think that it might be better to change my_set.

[Barinder Singh Banwait]

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

[Johan Commelin]

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]

Let me try something

[Barinder Singh Banwait]

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]

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]

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

[Johan Commelin]

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]

Now we need to extract some juice out of hf

[Johan Commelin]

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

[Barinder Singh Banwait]

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

[Johan Commelin]

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

[Johan Commelin]

So it deserves a prettier name (-;

[Johan Commelin]

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]

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

[Barinder Singh Banwait]

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

[Johan Commelin]

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