Zulip Chat Archive

Stream: new members

Topic: degree of elementary symmetric polynomials


view this post on Zulip Hanting Zhang (Mar 15 2021 at 20:49):

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

view this post on Zulip Yakov Pechersky (Mar 15 2021 at 21:17):

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 _)

view this post on Zulip Hanting Zhang (Mar 15 2021 at 22:02):

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.

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 08:21):

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.

view this post on Zulip Kevin Buzzard (Mar 16 2021 at 08:24):

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?

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:25):

there's no top in multiset

view this post on Zulip Mario Carneiro (Mar 16 2021 at 08:26):

it might be conditionally complete though

view this post on Zulip Hanting Zhang (Mar 16 2021 at 15:27):

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

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 15:28):

Can you share your whole proof?

view this post on Zulip Hanting Zhang (Mar 16 2021 at 16:41):

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.

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 18:36):

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

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 18:52):

And also for n greater than card \sigma

view this post on Zulip Hanting Zhang (Mar 16 2021 at 19:01):

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.

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 19:01):

Right, just clarifying

view this post on Zulip Yakov Pechersky (Mar 16 2021 at 22:58):

#6718

view this post on Zulip Hanting Zhang (Mar 17 2021 at 00:35):

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

view this post on Zulip Johan Commelin (Mar 17 2021 at 06:43):

@Hanting Zhang That's a very nice target!


Last updated: May 11 2021 at 14:11 UTC