mv_polynomial questions

Stream: maths

[Kevin Buzzard]

@Shing Tak Lam has been thinking about multivariate polynomials and gave me these three puzzles:

lemma single_eq_C_mul_X (s : S) (a : R) (n : ℕ): monomial (single s n) a = C a * (X s)^n := sorry
lemma erase_single (var : S) (n : ℕ): (erase var (single var n)) = 0 := sorry
lemma erase_single_ne (v1 v2 : S) (n : ℕ) (hv : v1 ≠ v2): (erase v1 (single v2 n)) = single v2 n := sorry

Independently, I was wondering whether we have the multivariable polynomial analogue of the statement that a polynomial p equals the sum of coeff p m * X ^m.

[Johan Commelin]

Re the independent question: I think we only have if for single variable polynomials: https://github.com/leanprover-community/mathlib/search?q=as_sum&unscoped_q=as_sum

[Kenny Lau]

wait... how do you search on github??

[Kevin Buzzard]

lemma finsupp.eq_zero_iff {α : Type*} {β : Type*} [has_zero β] (f : α →₀ β) :
  f = 0 ↔ ∀ x : α, f x = 0 :=
begin
  split,
  { intro hf,
    rw hf,
    intro x,
    refl,
  },
  { intro h,
    ext x,
    exact h x
  }
end

open_locale classical

lemma erase_single (var : S) (n : ℕ): (erase var (single var n)) = 0 :=
begin
  rw finsupp.eq_zero_iff,
  intro x,
  by_cases hx : x = var,
  { rw hx,
    apply erase_same,
  },
  { rw erase_ne hx,
    apply single_eq_of_ne,
    symmetry, assumption
  }
end

I don't know my way around finsupp. Am I making a mountain out of a molehill?

[Jason KY.]

Kenny Lau said:

wait... how do you search on github??

https://help.github.com/en/github/searching-for-information-on-github/about-searching-on-github

[Marc Huisinga]

Kenny Lau said:

wait... how do you search on github??

often with plenty of pain because there's still no way to do exact string searches (it's in the beta for some repos, though)

[Kenny Lau]

import data.mv_polynomial

open finsupp mv_polynomial

universes u v

variables {R : Type u} {S : Type v} [comm_ring R]

lemma single_eq_C_mul_X (s : S) (a : R) (n : ℕ): monomial (single s n) a = C a * (X s)^n :=
by rw [← zero_add (single s n), monomial_add_single, C]

lemma erase_single (var : S) (n : ℕ): (erase var (single var n)) = 0 :=
begin
  ext s, classical, by_cases hs : s = var,
  { rw [hs, erase_same], refl },
  { rw [erase_ne hs], exact single_eq_of_ne (ne.symm hs) }
end

lemma erase_single_ne (v1 v2 : S) (n : ℕ) (hv : v1 ≠ v2): (erase v1 (single v2 n)) = single v2 n :=
begin
  ext s, classical, by_cases hs : s = v1,
  { rw [hs, erase_same, single_eq_of_ne (hv.symm)] },
  { rw [erase_ne hs] }
end

[Kevin Buzzard]

Nice, thanks Kenny. I thought it was a bit annoying that by_cases gave as a case ¬s = var. Would we rather have s ≠ var? Then you can do hs.symm instead of ne.symm hs

[Mario Carneiro]

eq_zero_iff looks like a version of extensionality

[Mario Carneiro]

it should just be a rewrite with ext_iff

[Scott Morrison]

I would love to change the behaviour of by_cases to produce ≠.

[Scott Morrison]

I would also love to remove ne.def from the simp set.

[Mario Carneiro]

removing ne.def would cause similar problems as noted with gt here

[Scott Morrison]

hmm, okay, I guess I don't understand.

[Scott Morrison]

(what about reversing the direction of ne.def, and keeping it as a simp lemma?)

[Chris Hughes]

I'd like to make ne notation. I think the only lemma about ne is ne.symm, so it's no great loss.