fintype enumerating a multiset

Stream: new members

[Notification Bot]

Xavier Roblot has marked this topic as unresolved.

[Xavier Roblot]

I am following up on this question since I have a hard time proving that multiset.card P.roots = fintype.card σ when I define σ = {x // x ∈ P.roots}. That is the following result:

import field_theory.splitting_field

open_locale classical polynomial

example {K : Type*} [field K] (P : K[X]) (h : P ≠ 0):
  multiset.card P.roots = fintype.card { x // x ∈ P.roots} :=
begin
  sorry,
end

[Kyle Miller]

Oh, sorry, I misunderstood what you were asking initially and gave you a type that enumerates the unique elements of the multiset (without duplicates).

[Xavier Roblot]

Oh, that explained why I had a hard time proving it :sweat_smile:

[Xavier Roblot]

Still, I would be very grateful if somebody could help me with my original question...

[Kyle Miller]

@Xavier Roblot It seems like there's not a way to turn a multiset into a Type with the same number of elements already. Here's a go at it:

import data.fintype.card
import algebra.big_operators

open_locale big_operators

instance {α : Type*} [decidable_eq α] : has_coe_to_sort (multiset α) Type* :=
⟨λ m, Σ (x : m.to_finset), fin (m.count x)⟩

-- Just to check that this instance works:
example {α : Type*} [decidable_eq α] [fintype α] (m : multiset α) : fintype m :=
infer_instance

lemma multiset.card_coe {α : Type*} [decidable_eq α] [fintype α] (m : multiset α) :
  fintype.card m = m.card :=
begin
  unfold_coes,
  simp,
  transitivity ∑ x in m.to_finset, multiset.count x m,
  convert finset.sum_coe_sort _ (λ x, m.count x),
  simp,
end

[Kyle Miller]

This adds a coercion from multiset to Type where elements are ordered pairs (x, i), with i indexing which x this is in the multiset.

[Xavier Roblot]

Thanks! That’s great. Maybe it should be in mathlib?

[Kyle Miller]

@Xavier Roblot This might be better to define first:

import data.fintype.card
import algebra.big_operators

/-- Construct a finset whose elements enumerate the elements of the multiset `m`. -/
def multiset.to_enum_finset {α : Type*} [decidable_eq α] (m : multiset α) : finset (α × ℕ) :=
m.to_finset.bUnion (λ x, (finset.range (m.count x)).map ⟨prod.mk x, prod.mk.inj_left x⟩)

@[simp]
lemma multiset.mem_to_enum_finset {α : Type*} [decidable_eq α] (m : multiset α) (p : α × ℕ) :
  p ∈ m.to_enum_finset ↔ p.1 ∈ m ∧ p.2 < m.count p.1 :=
begin
  simp only [multiset.to_enum_finset, finset.mem_bUnion, multiset.mem_to_finset,
    finset.mem_map, finset.mem_range, function.embedding.coe_fn_mk, exists_prop],
  split,
  { rintro ⟨x, hx, i, hi, rfl⟩,
    exact ⟨hx, hi⟩ },
  { rintro ⟨h1, h2⟩,
    exact ⟨p.1, h1, p.2, h2, prod.mk.eta⟩ },
end

@[simp]
lemma multiset.coe_to_enum_finset {α : Type*} [decidable_eq α] (m : multiset α) :
  (m.to_enum_finset : set (α × ℕ)) = {p | p.1 ∈ m ∧ p.2 < m.count p.1} :=
by { ext, simp }

@[mono]
lemma multiset.to_enum_finset_mono {α : Type*} [decidable_eq α] {m₁ m₂ : multiset α}
  (h : m₁ ≤ m₂) : m₁.to_enum_finset ⊆ m₂.to_enum_finset :=
begin
  rintro ⟨x, i⟩,
  simp only [multiset.mem_to_enum_finset, and_imp],
  intros hx hi,
  refine ⟨multiset.mem_of_le h hx, _⟩,
  calc i < multiset.count x m₁ : hi
     ... ≤ multiset.count x m₂ : multiset.le_iff_count.mp h x,
end

@[simp]
lemma multiset.card_to_enum_finset {α : Type*} [decidable_eq α] (m : multiset α) :
  m.to_enum_finset.card = m.card :=
begin
  rw [multiset.to_enum_finset, finset.card_bUnion],
  { simp, },
  { simp only [multiset.mem_to_finset, ne.def],
    rintros x hx y hy hxy ⟨a, i⟩,
    simp only [finset.inf_eq_inter, finset.mem_inter, finset.mem_map, finset.mem_range,
      function.embedding.coe_fn_mk, prod.mk.inj_iff, exists_prop, exists_eq_right_right,
      finset.bot_eq_empty, finset.not_mem_empty, and_imp],
    rintros - rfl - rfl,
    contradiction, },
end

[Kyle Miller]

That way we have finsets that satisfy some order properties (like the to_enum_finset_mono lemma), and there are fewer dependent types.

[Kyle Miller]

I'm not sure what the right name for this is. multiset.to_enum_finset makes it seem like it's enumerating all the elements in some order, but it's only enumerating repeats (so for example the multiset with 1,2,2,3 would give the finset {(1,0), (2,0), (2,1), (3,0)}).

[Yakov Pechersky]

from collections import Counter :snake:

[Yakov Pechersky]

Probably defined via a list fold then into the quotient with a proof that the fold commutes, no longer N^2 construction

[Yakov Pechersky]

Unless my fold is hiding N^2 due to the cons

[Xavier Roblot]

Kyle Miller said:

I'm not sure what the right name for this is. multiset.to_enum_finset makes it seem like it's enumerating all the elements in some order, but it's only enumerating repeats (so for example the multiset with 1,2,2,3 would give the finset {(1,0), (2,0), (2,1), (3,0)}).

Yes, basically, you are making a finset from a multiset without deleting duplicates. Something multiset.to_finset_with_dup could work maybe

[Eric Wieser]

Is there an XY problem here where using docs#multiset.prod instead of docs#finset.prod would avoid the problem?

[Xavier Roblot]

Well, I guess I could change the statement of docs#mv_polynomial.prod_X_add_C_coeff and other results in vieta to use multiset instead of finset...

[Violeta Hernández]

You might want to make a def for the n-th symmetric polynomial of the roots of a polynomial, and give expressions in terms of finset.prod and multiset.prod

[Violeta Hernández]

(if I understand the problem correctly)

[Eric Wieser]

Xavier Roblot said:

Well, I guess I could change the statement of docs#mv_polynomial.prod_X_add_C_coeff and other results in vieta to use multiset instead of finset...

I think this is the way to go. It's a lot easier to derive finset results from multiset results than it is to go the other way around

[Xavier Roblot]

Violeta Hernández said:

You might want to make a def for the n-th symmetric polynomial of the roots of a polynomial, and give expressions in terms of finset.prod and multiset.prod

These results exist already more or less in ring_theory.polynomial.vieta but there are not used anywhere else...

Oh, I see. I think I misunderstood what you meant...

[Xavier Roblot]

Eric Wieser said:

Xavier Roblot said:

Well, I guess I could change the statement of docs#mv_polynomial.prod_X_add_C_coeff and other results in vieta to use multiset instead of finset...

I think this is the way to go. It's a lot easier to derive finset results from multiset results than it is to go the other way around

Ok. I'll PR that. I still think that the code of Kyle might be useful at some point in the future.

[Xavier Roblot]

Ok, after spending some time thinking about it and trying several options, I do not think that replacing fintype with multiset in ring_theory.polynomial.vieta and, for consistency,ring_theory.polynomial.symmetric is the way go. I mean it is certainly possible, although probably quite messy, but even from a mathematical point of view I do not think it makes sense: in this file, we work with polynomials whose coefficients are in some ring $R[X_i]_{i \in \sigma}$ with the $X_i$'s some indeterminates indexed by a type $\sigma$. It does make sense here to have $\sigma$ being a multiset.

It is only when we want to evaluate the indeterminates $X_i$ to some value $r_i \in R$, that it makes sense to have the possibility to repeat values. At the moment, this evaluation is done by providing a function $\sigma \to R$ where σ is a fintype. So the missing link is a way to construct such a function when we want its image be a multiset. I don't know how to that. Kyle is providing a solution above by creating a fintype that enumerates the elements of a multiset, but there might be other solutions.

[Eric Wieser]

(I had a look too, and did some cleanup in #14866)

[Xavier Roblot]

Ok, I have found a short solution. I'll still have to see if I can make it work all the way: I lift the multiset s to a list L and then enumerate the elements of L using finset.range L.length. The result is not very pretty...

[Junyan Xu]

Here is a way of using fin s.card as the indexing type:

import data.multiset.basic
noncomputable def multiset.of_fin_card {α} (s : multiset α) (n : fin s.card) :=
s.to_list.nth_le n.1 (by { convert n.2, rw [← multiset.coe_card, multiset.coe_to_list] })

Not sure if it's simpler or more complicated than your short solution.

[Junyan Xu]

By the way, if your goal is #11523, I don't think you need to invoke mathlib's Vieta theorem. @Riccardo Brasca's post says:

Let R be an integrally closed domain with fraction field K and let f : polynomial R be monic. If f = g * h over K, then g and h have coefficients in R. Indeed, we can assume that g and h are monic (by factoring out the leading coefficients). If L is a splitting field of f, then writing f as a product of linear factors over L we see that both g and h are product of factors of the form X - a, where a ranges over a subset of the roos of f, that are algebraic over R by assumption. By Vieta, the coefficients of g and h are also algebraic over R, but lie K and so they are in R.

But in fact you just need that g.map (K -> L) is g'.map (integral_closure of R in L -> L) for some g', and this g' can be defined to be the multiset product of X - C a over roots a of g.map (K -> L). Although (g.map (K -> L)).roots : multiset L, the roots of g.map (K -> L) are also roots of f.map (R -> L) so they lie in the integral closure, and you can use docs#multiset.attach combined with docs#multiset.map to get the desired multiset (integral closure) of roots. g' is then a polynomial over the integral closure and automatically has coefficients in the integral closure.

[Xavier Roblot]

Thanks for your answer. So far, things seem nicer with your def than with what I had so far. My end goal here is a formula to bound the coefficients of a polynomial in terms of bounds on its roots. This is needed for the FLT regular project to prove Kronecker's theorem : an algebraic integer whose conjugates are all of absolute value 1 is a root of unity. Now, I know I can get this result with what's already in ring_theory.polynomial.vieta but I thought it would be nice to prove along the way the classical formula between the roots and coefficients of a polynomial. In fact, Alex J. Best already had a proof of that result that we use to prove Kronecker's theorem in the FLT regular project, but it is done from scratch and is quite intricate. Since we want to PR Kronecker's theorem in mathlib, I wanted to redo the proof using what's already in ring_theory.polynomial.vieta.

[Riccardo Brasca]

Yes, any polynomial will do the trick, it is unrelated to being symmetric or whatever

[Junyan Xu]

The multiset version of the theorem docs#mv_polynomial.prod_X_add_C_coeff in the original post is the following:

lemma multiset_prod_X_add_C_coeff (s : multiset R) (k : ℕ) (h : k ≤ s.card) :
  (s.map (λ r, polynomial.C r + polynomial.X)).prod.coeff k =
  ((s.powerset_len (card σ - k)).map multiset.prod).sum :=

which should follow from that theorem using the indexing functionmultiset.of_fin_card and some lemmas that should exist in mathlib. I'm currently taking a look. Have you been able to prove it? Once it's proved, it's easy to deduce the formula between roots and coefficients, by taking s to be p.roots.map neg.

[Junyan Xu]

@Xavier Roblot I have been able to prove the multiset version:

import data.multiset.basic
import ring_theory.polynomial.vieta

lemma fin_range_eq_univ (n : ℕ) : finset.fin_range n = finset.univ :=
finset.eq_univ_of_forall finset.mem_fin_range

lemma multiset.length_to_list {α} (s : multiset α) : s.to_list.length = s.card :=
by rw [← multiset.coe_card, s.coe_to_list]

noncomputable def multiset.of_fin_card {α} (s : multiset α) (n : fin s.card) :=
s.to_list.nth_le n (by { rw s.length_to_list, exact n.2 })

lemma list.map_nth_le {α} (l : list α) :
  l = (list.fin_range l.length).map (λ n, l.nth_le n n.2) :=
list.ext_le (by rw [list.length_map, list.length_fin_range]) $ λ n h _,
begin
  rw ← list.nth_le_map_rev, congr,
  { rw list.nth_le_fin_range, refl },
  { rw list.length_fin_range, exact h },
end

lemma multiset.exists_fin_map_eq {α} (s : multiset α) :
  ∃ n (f : fin n → α), (@finset.univ (fin n) _).val.map f = s :=
⟨s.card, s.of_fin_card, begin
  conv_rhs { rw ← s.coe_to_list },
  convert multiset.coe_map _ _,
  convert ← s.to_list.map_nth_le,
  { exact s.length_to_list },
  { rw fin.heq_fun_iff s.length_to_list, intro, refl },
  { exact s.length_to_list },
end⟩

variables {R : Type*}
lemma multiset_prod_X_add_C_coeff [comm_semiring R] (s : multiset R) (k : ℕ) (h : k ≤ s.card) :
  (s.map (λ r, polynomial.C r + polynomial.X)).prod.coeff k =
  ((s.powerset_len (s.card - k)).map multiset.prod).sum :=
begin
  obtain ⟨n, f, rfl⟩ := s.exists_fin_map_eq,
  rw [multiset.map_map, ← finset.prod_eq_multiset_prod, mv_polynomial.prod_X_add_C_coeff],
  swap, { convert h, rw multiset.card_map, refl },
  rw [multiset.powerset_len_map, ← finset.map_val_val_powerset_len],
  rw [finset.sum_eq_multiset_sum, multiset.map_map, multiset.map_map],
  congr, rw multiset.card_map, refl,
end

[Xavier Roblot]

Hey, that’s great! I spent a couple of hours yesterday trying to make it work without going anywhere. I guess there is still a lot I need to learn about Lean and mathlib. Can you PR this into mathlib? It would be a great addition and allow me to PR Kronecker theorem. As you said, getting the result I need from your result is straightforward.

[Junyan Xu]

Sure, I'll PR it later. It's still a bit nontrivial to deal with the negations (to extract a power of -1 as a factor), so I should probably include a version with X - C r in vieta.lean; then you can directly plug it into docs#polynomial.C_leading_coeff_mul_prod_multiset_X_sub_C.

[Junyan Xu]

#14908
will add PR description later