Multisets of exponent vectors

Mathlib's Finsupp.toMultiset sends an exponent vector e : α →₀ ℕ to the multiset in which each a occurs e a times. Its cardinality is the total degree of e. This file also computes it on exponent vectors built from unit steps Finsupp.single a 1: adding one unit step conses its index, and a sum of unit steps along a finite family is the multiset of values of the family. The coefficients of such a sum are the letter counts of the family: the number of indices at which it takes each value.

Main results

• Finsupp.card_toMultiset_eq_degree: card (toMultiset e) = e.degree.
• Finsupp.toMultiset_add_single_one: toMultiset (e + single a 1) = a ::ₘ toMultiset e.
• Finsupp.toMultiset_sum_single_one: toMultiset (∑ i ∈ s, single (p i) 1) = s.val.map p.
• Finsupp.sum_single_one_apply: along a family f indexed by a finite type, the coefficient of a in ∑ t, single (f t) 1 is the number of indices t with f t = a; Finsupp.sum_sum_single_one_apply and Finsupp.sum_single_one_apply_ne_zero_iff record that these letter counts sum to the number of indices and are nonzero exactly at the values of f.
• Finsupp.exists_sum_single_eq_iff: the letter counts of ordered n-tuples are exactly the exponent vectors of total degree n.

The same unit steps summed along a list, with coefficients in any additive commutative monoid with one, count the occurrences of each letter; in characteristic zero these counts determine a constant list.

• List.sum_map_single_one_apply: (l.map fun k ↦ single k 1).sum a = l.count a.
• List.eq_replicate_of_sum_map_single_one_eq: a list whose letter counts are those of m copies of i is m copies of i.

theorem Finsupp.card_toMultiset_eq_degree {α : Type u_1} (d : α →₀ ℕ) : (toMultiset d).card = degree d

The number of letters of the monomial with exponent vector d is its total degree. This is not a simp lemma: Finsupp.card_toMultiset already rewrites the left-hand side to d.sum fun _ => id, so tagging it would leave it out of simp-normal form.

theorem Finsupp.toMultiset_add_single_one {α : Type u_1} (e : α →₀ ℕ) (a : α) : toMultiset (e + single a 1) = a ::ₘ toMultiset e

Adding one unit step at a to an exponent vector conses a onto its multiset.

theorem Finsupp.toMultiset_sum_single_one {α : Type u_1} {ι : Type u_2} (s : Finset ι) (p : ι → α) : toMultiset (∑ i ∈ s, single (p i) 1) = Multiset.map p s.val

The multiset of a sum of unit steps along a family p indexed by a finset s is the multiset of the values of p on s.

theorem Finsupp.sum_single_one_apply {α : Type u_1} {ι : Type u_2} [Fintype ι] [DecidableEq α] (f : ι → α) (a : α) : (∑ t : ι, single (f t) 1) a = {t : ι | f t = a}.card

The letter counts of a family: the coefficient of a in ∑ₜ single (f t) 1 is the number of indices t with f t = a.

theorem Finsupp.sum_sum_single_one_apply {α : Type u_1} {ι : Type u_2} [Fintype ι] {f : ι → α} {F : Finset α} (hf : ∀ (t : ι), f t ∈ F) : ∑ a ∈ F, (∑ t : ι, single (f t) 1) a = Fintype.card ι

The letter counts of a family with values in F sum, over F, to the number of indices.

theorem Finsupp.sum_single_one_apply_ne_zero_iff {α : Type u_1} {ι : Type u_2} [Fintype ι] {f : ι → α} {a : α} : (∑ t : ι, single (f t) 1) a ≠ 0 ↔ ∃ (t : ι), f t = a

A value is taken by a family exactly when its letter count is nonzero.

theorem Finsupp.exists_sum_single_eq_iff {α : Type u_1} {n : ℕ} (l : α →₀ ℕ) : (∃ (f : Fin n → α), ∑ t : Fin n, single (f t) 1 = l) ↔ (l.sum fun (x : α) (k : ℕ) => k) = n

The letter counts of ordered n-tuples are exactly the exponent vectors of total degree n.

theorem List.sum_map_single_one_apply {α : Type u_1} {R : Type u_2} [AddCommMonoidWithOne R] [DecidableEq α] (l : List α) (a : α) : (map (fun (k : α) => Finsupp.single k 1) l).sum a = ↑(count a l)

Summing the unit steps single k 1 along a list counts the occurrences of each letter.

theorem List.eq_replicate_of_sum_map_single_one_eq {α : Type u_1} {R : Type u_2} [AddCommMonoidWithOne R] [CharZero R] {l : List α} {i : α} {m : ℕ} (hl : (map (fun (k : α) => Finsupp.single k 1) l).sum = Finsupp.single i ↑m) : l = replicate m i

In characteristic zero, a list whose sum of unit steps is m times the unit step at i is the list of m copies of i.