degree of elementary symmetric polynomials

Stream: new members

[Hanting Zhang]

Besides the instance issue in the second proof, I would very much appreciate any suggestions for which direction to work in for both. Using finset, finsupp, and multiset at the same time is not fun.

import ring_theory.polynomial.symmetric
import ring_theory.polynomial.homogeneous
import data.mv_polynomial.basic
import data.multiset.basic

noncomputable theory

open fintype classical
open_locale big_operators

namespace mv_polynomial
variables {σ : Type*} [fintype σ]  {R : Type*} [comm_semiring R]

lemma support_esymm (n : ℕ) [decidable_eq σ] :
  (esymm σ R n).support = (finset.powerset_len n (finset.univ : finset σ)).image (λ t, ∑ i in t, finsupp.single i 1) :=
by sorry

lemma degrees_esymm (n : ℕ) [decidable_eq σ] : (esymm σ R n).degrees = (finset.univ : finset σ).val :=
begin
  simp only [degrees, support_esymm],
  convert ← finset.sup_finset_image,
  -- goal: semilattice_sup_bot_of_bounded_lattice (multiset σ) = multiset.semilattice_sup_bot
  sorry,
  sorry,
  sorry,
  sorry
end

end mv_polynomial

[Yakov Pechersky]

Some API to get you started:

@[simp] lemma multiset.count_univ [fintype α] (a : α) :
  multiset.count a finset.univ.val = 1 :=
multiset.count_eq_one_of_mem finset.univ.nodup (finset.mem_univ _)

[Hanting Zhang]

Oh, maybe I was not being explicit, but the main issue is the instance issue. I'm not able to bypass it using the usual congr trick. At the same time I'm not sure why instances ever break like this anyways, so I don't know how I should proceed to fix it properly.

[Kevin Buzzard]

After the convert some of your goals are data, and the reason those lattices aren't equal (or at least one of the reasons) is that one of them has a metavariable in the definition, which corresponds to a later sorry. convert does this. It's not good with type class inference, for example -- type class goals can be spat out as separate goals for later on, before unification takes place, it seems to me; often goals spat out by convert can be solved with apply_instance.

[Kevin Buzzard]

In this case one of your goals is ⊢ complete_lattice (multiset σ) and apply_instance doesn't solve it, and I'm not sure that such an instance can exist because {37},{37,37},{37,37,37,},... has no sup. So maybe you're converting the wrong lemma?

[Mario Carneiro]

there's no top in multiset

[Mario Carneiro]

it might be conditionally complete though

[Hanting Zhang]

The problem was that finset.sup_finset_image assumes the need of a complete lattice when there's no need for it. Having a semilattice_inf_bot suffices, but I had to rewrite the proof. (The one in the library uses supr to prove it, which adds the unneeded condition.)

[Yakov Pechersky]

Can you share your whole proof?

[Hanting Zhang]

It quite ugly right now, but here:

import ring_theory.polynomial.symmetric
import ring_theory.polynomial.homogeneous
import data.mv_polynomial.basic
import data.multiset.basic

noncomputable theory

open finset mv_polynomial
open_locale classical big_operators

variables {α : Type*} {M : Type*} [decidable_eq α] [comm_semiring M] [nontrivial M]

namespace mv_polymonial
variables {σ : Type*} [fintype σ] {R : Type*} [comm_semiring R]

lemma support_sum_eq {α : Type*} {ι : Type*} {M : Type*} [add_comm_monoid M]
  {g : ι → α →₀ M} (s : finset ι) (h : ∀ i₁ i₂, i₁ ≠ i₂ → disjoint (g i₁).support (g i₂).support) :
  (∑ i in s, g i).support = s.bUnion (λ i, (g i).support) :=
begin
  sorry
end

theorem finsupp.support_single {α : Type*} {M : Type*} [has_zero M] (a : α) (b : M) :
b ≠ 0 → (finsupp.single a b).support = {a} :=
begin
  intro hb,
  ext a',
  sorry
end

lemma support_esymm'' (n : ℕ) [decidable_eq σ] [nontrivial R] :
  (esymm σ R n).support = (powerset_len n (univ : finset σ)).bUnion (λ t, (finsupp.single (∑ (i : σ) in t, finsupp.single i 1) (1:R)).support) :=
begin
  rw esymm_eq_sum_monomial,
  simp only [monomial],
  convert support_sum_eq (powerset_len n (univ : finset σ)) _,
  intros i j hij d,
  simp only [finsupp.support_single _ (1:R) one_ne_zero],
  simp only [and_imp, inf_eq_inter, mem_inter, mem_singleton],
  have : 1 ≠ 0, { simp only [ne.def, not_false_iff, one_ne_zero] },
  intros h1 h2,
  have hi : (∑ (i : σ) in i, finsupp.single i 1).support = i,
  { rw support_sum_eq i _,
    simp [finsupp.support_single _ 1 this],
    intros i j hij,
    simp [finsupp.support_single _ 1 this],
    rw ← ne.def,
    exact hij.symm, },
  have hj : (∑ (i : σ) in j, finsupp.single i 1).support = j,
  { rw support_sum_eq j _,
    simp [finsupp.support_single _ 1 this],
    intros i j hij,
    simp [finsupp.support_single _ 1 this],
    rw ← ne.def,
    exact hij.symm},
  apply_fun finsupp.support at h1,
  apply_fun finsupp.support at h2,
  rw hi at h1,
  rw hj at h2,
  rw h1 at h2,
  contradiction,
end

lemma support_esymm' (n : ℕ) [decidable_eq σ] [nontrivial R] :
  (esymm σ R n).support = (powerset_len n (univ : finset σ)).bUnion (λ t, {∑ (i : σ) in t, finsupp.single i 1}) :=
begin
  rw support_esymm'',
  congr,
  funext,
  exact finsupp.support_single _ 1 one_ne_zero,
end

lemma support_esymm (n : ℕ) [decidable_eq σ] [nontrivial R] :
  (esymm σ R n).support =
  (powerset_len n (univ : finset σ)).image (λ t, ∑ (i : σ) in t, finsupp.single i 1) :=
begin
  rw support_esymm',
  exact bUnion_singleton,
end

lemma sup_finset_image' {α : Type*} {β : Type*} {γ : Type*}
  [decidable_eq α] [semilattice_sup_bot β] {f : γ → α} {g : α → β} (s : finset γ) :
  s.sup (g ∘ f) = (s.image f).sup g :=
begin
  apply finset.induction_on s,
  { simp },
  intros a s' ha ih,
  rw sup_insert,
  rw image_insert,
  rw sup_insert,
  rw ih,
end

lemma to_multiset_sum {ι : Type*} {f : ι → σ →₀ ℕ} (s : finset ι) :
finsupp.to_multiset (∑ i in s, f i) = ∑ i in s, finsupp.to_multiset (f i) :=
by sorry

lemma single_to_multiset :
  (finsupp.to_multiset ∘ λ (t : finset σ), ∑ (i : σ) in t, finsupp.single i 1) = λ t, t.val :=
begin
  funext,
  simp only [function.comp_app],
  rw to_multiset_sum,
  simp only [finsupp.to_multiset_single, one_nsmul], sorry
end

lemma degrees_esymm (n : ℕ) [decidable_eq σ] [nontrivial R] :
  (esymm σ R n).degrees = (univ : finset σ).val :=
begin
  rw degrees,
  rw support_esymm,
  rw (sup_finset_image' (powerset_len n univ)).symm,
  simp [single_to_multiset],
  sorry
end

end mv_polymonial

My willpower to fill the sorrys ran out, but they're all simple ones.

[Yakov Pechersky]

I'm filling it out, but just noticed: is it true for n = 0?

[Yakov Pechersky]

And also for n greater than card \sigma

[Hanting Zhang]

No for both. esymm \s R 0 is just 1, which has no variables, so the degrees set is empty. For card \s < n, esymm \s R n is a sum over nothing, so its degrees set is also empty.

[Yakov Pechersky]

Right, just clarifying

[Yakov Pechersky]

#6718

[Hanting Zhang]

Hooray! And thus we have the first step in the long journey to the Lindemann-Weierstrass theorem.

[Johan Commelin]

@Hanting Zhang That's a very nice target!