feat: the nth symmetric power is equivalent to maps of total mass `…

…n`. (#11360)

Co-authored-by: Eric Wieser <wieser.eric@gmail.com>

Mathlib/Algebra/BigOperators/Basic.lean

@@ -2444,6 +2444,13 @@ theorem toFinset_sum_count_eq (s : Multiset α) : ∑ a in s.toFinset, s.count a
     _ = card s := by simp
 #align multiset.to_finset_sum_count_eq Multiset.toFinset_sum_count_eq
 
+@[simp]
+theorem sum_count_eq [Fintype α] (s : Multiset α) : ∑ a, s.count a = Multiset.card s := by
+  rw [← toFinset_sum_count_eq, ← Finset.sum_filter_ne_zero]
+  congr
+  ext
+  simp
+
 theorem count_sum' {s : Finset β} {a : α} {f : β → Multiset α} :
     count a (∑ x in s, f x) = ∑ x in s, count a (f x) := by
   dsimp only [Finset.sum]

Mathlib/Data/Finsupp/Multiset.lean

@@ -65,6 +65,7 @@ theorem toMultiset_sum_single (s : Finset ι) (n : ℕ) :
   simp_rw [toMultiset_sum, Finsupp.toMultiset_single, sum_nsmul, sum_multiset_singleton]
 #align finsupp.to_multiset_sum_single Finsupp.toMultiset_sum_single
 
+@[simp]
 theorem card_toMultiset (f : α →₀ ℕ) : Multiset.card (toMultiset f) = f.sum fun _ => id := by
   simp [toMultiset_apply, map_finsupp_sum, Function.id_def]
 #align finsupp.card_to_multiset Finsupp.card_toMultiset
@@ -192,6 +193,10 @@ theorem toFinsupp_inter (s t : Multiset α) : toFinsupp (s ∩ t) = toFinsupp s
   ext
   simp [inf_eq_min]
 
+@[simp]
+theorem toFinsupp_sum_eq (s : Multiset α) : s.toFinsupp.sum (fun _ ↦ id) = Multiset.card s := by
+  rw [← Finsupp.card_toMultiset, toFinsupp_toMultiset]
+
 end Multiset
 
 @[simp]
@@ -251,3 +256,46 @@ end Finsupp
 theorem Multiset.toFinsupp_strictMono [DecidableEq ι] : StrictMono (@Multiset.toFinsupp ι _) :=
   (@Finsupp.orderIsoMultiset ι).symm.strictMono
 #align multiset.to_finsupp_strict_mono Multiset.toFinsupp_strictMono
+
+namespace Sym
+
+variable (α)
+variable [DecidableEq α] (n : ℕ)
+
+/-- The `n`th symmetric power of a type `α` is naturally equivalent to the subtype of
+finitely-supported maps `α →₀ ℕ` with total mass `n`.
+
+See also `Sym.equivNatSumOfFintype` when `α` is finite. -/
+def equivNatSum :
+    Sym α n ≃ {P : α →₀ ℕ // P.sum (fun _ ↦ id) = n} :=
+  Multiset.toFinsupp.toEquiv.subtypeEquiv <| by simp
+
+@[simp] lemma coe_equivNatSum_apply_apply (s : Sym α n) (a : α) :
+    (equivNatSum α n s : α →₀ ℕ) a = (s : Multiset α).count a :=
+  rfl
+
+@[simp] lemma coe_equivNatSum_symm_apply (P : {P : α →₀ ℕ // P.sum (fun _ ↦ id) = n}) :
+    ((equivNatSum α n).symm P : Multiset α) = Finsupp.toMultiset P :=
+  rfl
+
+/-- The `n`th symmetric power of a finite type `α` is naturally equivalent to the subtype of maps
+`α → ℕ` with total mass `n`.
+
+See also `Sym.equivNatSum` when `α` is not necessarily finite. -/
+noncomputable def equivNatSumOfFintype [Fintype α] :
+    Sym α n ≃ {P : α → ℕ // ∑ i, P i = n} :=
+  (equivNatSum α n).trans <| Finsupp.equivFunOnFinite.subtypeEquiv <| by simp [Finsupp.sum_fintype]
+
+@[simp] lemma coe_equivNatSumOfFintype_apply_apply [Fintype α] (s : Sym α n) (a : α) :
+    (equivNatSumOfFintype α n s : α → ℕ) a = (s : Multiset α).count a :=
+  rfl
+
+@[simp] lemma coe_equivNatSumOfFintype_symm_apply [Fintype α] (P : {P : α → ℕ // ∑ i, P i = n}) :
+    ((equivNatSumOfFintype α n).symm P : Multiset α) = ∑ a, ((P : α → ℕ) a) • {a} := by
+  obtain ⟨P, hP⟩ := P
+  change Finsupp.toMultiset (Finsupp.equivFunOnFinite.symm P) = Multiset.sum _
+  ext a
+  rw [Multiset.count_sum]
+  simp [Multiset.count_singleton]
+
+end Sym