## Stream: new members

### Topic: degree of elementary symmetric polynomials

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


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


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

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

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

#### Mario Carneiro (Mar 16 2021 at 08:25):

there's no top in multiset

#### Mario Carneiro (Mar 16 2021 at 08:26):

it might be conditionally complete though

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

#### Yakov Pechersky (Mar 16 2021 at 15:28):

Can you share your whole proof?

#### 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,
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 (Mar 16 2021 at 18:36):

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

#### Yakov Pechersky (Mar 16 2021 at 18:52):

And also for n greater than card \sigma

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

#### Yakov Pechersky (Mar 16 2021 at 19:01):

Right, just clarifying

#6718

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

#### Johan Commelin (Mar 17 2021 at 06:43):

@Hanting Zhang That's a very nice target!

Last updated: Dec 20 2023 at 11:08 UTC