[Merged by Bors] - feat: Complete homogeneous and monomial symmetric polynomials

Mathlib/Combinatorics/Enumerative/Partition.lean

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Bhavik Mehta
 -/
 import Mathlib.Combinatorics.Enumerative.Composition
+import Mathlib.Data.Multiset.Dedup
 import Mathlib.Data.Nat.Parity
 import Mathlib.Tactic.ApplyFun
 
@@ -102,6 +103,25 @@ def ofSums (n : ℕ) (l : Multiset ℕ) (hl : l.sum = n) : Partition n where
 def ofMultiset (l : Multiset ℕ) : Partition l.sum := ofSums _ l rfl
 #align nat.partition.of_multiset Nat.Partition.ofMultiset
 
+/-- An element `s` of `Sym σ n` induces a partition given by its multiplicities. -/
+def ofSym {n : ℕ} {σ : Type*} (s : Sym σ n) [DecidableEq σ] : n.Partition where
+  parts := s.1.dedup.map s.1.count
+  parts_pos := by simp [Multiset.count_pos]
+  parts_sum := by
+    have : sum (map (fun a ↦ count a s.1) s.1.dedup) =
+      Finset.sum (toFinset s.1) fun a ↦ count a s.1 := rfl
+    rw [this, Multiset.toFinset_sum_count_eq]
+    exact s.2
+
+lemma ofSym_map {n : ℕ} {σ τ : Type*} [DecidableEq σ] [DecidableEq τ] (e : σ ≃ τ) (s : Sym σ n) :
+    Nat.Partition.ofSym (s.map e) = Nat.Partition.ofSym s := by
+  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, toFinset_val, mk.injEq]
+  rw [Multiset.dedup_map_of_injective]
+  simp only [map_map, Function.comp_apply]
+  congr; funext i
+  rw [← Multiset.count_map_eq_count' e]
+  all_goals exact e.injective
+
 /-- The partition of exactly one part. -/
 def indiscrete (n : ℕ) : Partition n := ofSums n {n} rfl
 #align nat.partition.indiscrete_partition Nat.Partition.indiscrete

Mathlib/Data/Multiset/Dedup.lean

@@ -122,6 +122,13 @@ theorem dedup_map_dedup_eq [DecidableEq β] (f : α → β) (s : Multiset α) :
   simp [dedup_ext]
 #align multiset.dedup_map_dedup_eq Multiset.dedup_map_dedup_eq
 
+theorem dedup_map_of_injective [DecidableEq β] {f : α → β} (hinj : Function.Injective f)
+    (s : Multiset α) : dedup (map f s) = map f (dedup s) := by
+  rw [← dedup_map_dedup_eq]
+  apply Multiset.dedup_eq_self.mpr
+  rw [Multiset.nodup_map_iff_of_injective hinj]
+  exact Multiset.nodup_dedup s
+
 @[simp]
 theorem dedup_nsmul {s : Multiset α} {n : ℕ} (h0 : n ≠ 0) : (n • s).dedup = s.dedup := by
   ext a

Mathlib/Data/Sym/Basic.lean

@@ -535,6 +535,21 @@ theorem mem_append_iff {s' : Sym α m} : a ∈ s.append s' ↔ a ∈ s ∨ a ∈
   Multiset.mem_add
 #align sym.mem_append_iff Sym.mem_append_iff
 
+/--
+Defines an equivalence between `α` and `Sym α 1`.
+-/
+@[simps apply]
+def oneEquiv : α ≃ Sym α 1 where
+  toFun a := ⟨{a}, by simp⟩
+  invFun s := Quotient.liftOn (Equiv.subtypeQuotientEquivQuotientSubtype
+      (·.length = 1) _ (fun l ↦ Iff.rfl) (fun l l' ↦ by rfl) s)
+    (fun l ↦ l.1.head <| List.length_pos.mp <| by simp)
+    fun ⟨l, h⟩ ⟨l', h'⟩ _perm ↦ by
+      obtain ⟨a, rfl⟩ := List.length_eq_one.mp h'
+      exact List.eq_of_mem_singleton (_perm.mem_iff.mp <| List.head_mem _)
+  left_inv a := by rfl
+  right_inv := by rintro ⟨⟨l⟩, h⟩; obtain ⟨a, rfl⟩ := List.length_eq_one.mp h; rfl
+
 /-- Fill a term `m : Sym α (n - i)` with `i` copies of `a` to obtain a term of `Sym α n`.
 This is a convenience wrapper for `m.append (replicate i a)` that adjusts the term using
 `Sym.cast`. -/

Mathlib/RingTheory/MvPolynomial/Symmetric.lean

@@ -3,9 +3,12 @@ Copyright (c) 2020 Hanting Zhang. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Hanting Zhang, Johan Commelin
 -/
+
 import Mathlib.Algebra.Algebra.Subalgebra.Basic
-import Mathlib.Algebra.MvPolynomial.Rename
 import Mathlib.Algebra.MvPolynomial.CommRing
+import Mathlib.Algebra.MvPolynomial.Rename
+import Mathlib.Combinatorics.Enumerative.Partition
+import Mathlib.Data.Sym.Basic
 
 #align_import ring_theory.mv_polynomial.symmetric from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 
@@ -23,15 +26,24 @@ We also prove some basic facts about them.
 
 * `MvPolynomial.esymm`
 
+* `MvPolynomial.hsymm`
+
 * `MvPolynomial.psum`
 
+* `MvPolynomial.msymm`
+
 ## Notation
 
 + `esymm σ R n` is the `n`th elementary symmetric polynomial in `MvPolynomial σ R`.
 
++ `hsymm σ R n` is the `n`th complete homogeneous symmetric polynomial in `MvPolynomial σ R`.
+
 + `psum σ R n` is the degree-`n` power sum in `MvPolynomial σ R`, i.e. the sum of monomials
   `(X i)^n` over `i ∈ σ`.
 
++ `msymm σ R μ` is the monomial symmetric polynomial whose exponents set are the parts
+  of `μ ⊢ n` in `MvPolynomial σ R`.
+
 As in other polynomial files, we typically use the notation:
 
 + `σ τ : Type*` (indexing the variables)
@@ -176,17 +188,47 @@ def renameSymmetricSubalgebra [CommSemiring R] (e : σ ≃ τ) :
     (AlgHom.ext <| fun p => Subtype.ext <| by simp)
     (AlgHom.ext <| fun p => Subtype.ext <| by simp)
 
+variable (σ R : Type*) [CommSemiring R] [CommSemiring S] [Fintype σ] [Fintype τ]
+
+/-! ### Multiplicativity on partitions -/
+
+/-- Given a sequence of `MvPolynomial` functions `f` and a partition `μ` of size `n`,
+`muProduct` computes the product of applying each function in `f` to the parts of `μ`. -/
+def muProduct {n : ℕ} (f : ℕ → MvPolynomial σ R) (μ : n.Partition) : MvPolynomial σ R :=
+  Multiset.prod (μ.parts.map f)
+
+lemma muProduct_def {n : ℕ} (f : ℕ → MvPolynomial σ R) (μ : n.Partition) :
+    muProduct σ R f μ = Multiset.prod (μ.parts.map f) := rfl
+
+@[simp]
+theorem muProduct_indiscrete_zero (f : ℕ → MvPolynomial σ R) :
+    muProduct σ R f (Nat.Partition.indiscrete 0) = 1 := by
+  simp only [muProduct, Nat.Partition.partition_zero_parts, Multiset.map_zero, Multiset.prod_zero]
+
+@[simp]
+theorem muProduct_indiscrete_of_pos (n : ℕ) (f : ℕ → MvPolynomial σ R) (npos : n > 0) :
+    muProduct σ R f (Nat.Partition.indiscrete n) = f n := by
+  rw [muProduct, Nat.Partition.indiscrete_parts, Multiset.map_singleton, Multiset.prod_singleton]
+  linarith
+
 section ElementarySymmetric
 
 open Finset
 
-variable (σ R) [CommSemiring R] [CommSemiring S] [Fintype σ] [Fintype τ]
-
 /-- The `n`th elementary symmetric `MvPolynomial σ R`. -/
 def esymm (n : ℕ) : MvPolynomial σ R :=
   ∑ t in powersetCard n univ, ∏ i in t, X i
 #align mv_polynomial.esymm MvPolynomial.esymm
 
+lemma esymm_def (n : ℕ) : esymm σ R n = ∑ t in powersetCard n univ, ∏ i in t, X i := rfl
+
+/--
+`esymmMu` is the product of the symmetric polynomials `esymm μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition.
+-/
+def esymmMu {n : ℕ} (μ : n.Partition) : MvPolynomial σ R :=
+  muProduct σ R (esymm σ R) μ
+
 /-- The `n`th elementary symmetric `MvPolynomial σ R` is obtained by evaluating the
 `n`th elementary symmetric at the `Multiset` of the monomials -/
 theorem esymm_eq_multiset_esymm : esymm σ R = (univ.val.map X).esymm := by
@@ -216,6 +258,19 @@ theorem esymm_zero : esymm σ R 0 = 1 := by
   simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]
 #align mv_polynomial.esymm_zero MvPolynomial.esymm_zero
 
+@[simp]
+theorem esymm_one : esymm σ R 1 = ∑ i, X i := by
+  simp only [esymm, powersetCard_one, sum_map, Function.Embedding.coeFn_mk, prod_singleton]
+
+theorem esymmMu_zero : esymmMu σ R (Nat.Partition.indiscrete 0) = 1 := by
+  simp only [esymmMu, esymm_zero, muProduct_indiscrete_zero]
+
+@[simp]
+theorem esymmMu_onePart (n : ℕ) : esymmMu σ R (Nat.Partition.indiscrete n) = esymm σ R n := by
+  cases n
+  · simp only [esymmMu, esymm_zero, muProduct_indiscrete_zero]
+  · simp only [esymmMu, gt_iff_lt, Nat.zero_lt_succ, muProduct_indiscrete_of_pos]
+
 theorem map_esymm (n : ℕ) (f : R →+* S) : map f (esymm σ R n) = esymm σ S n := by
   simp_rw [esymm, map_sum, map_prod, map_X]
 #align mv_polynomial.map_esymm MvPolynomial.map_esymm
@@ -300,26 +355,100 @@ theorem degrees_esymm [Nontrivial R] (n : ℕ) (hpos : 0 < n) (hn : n ≤ Fintyp
 
 end ElementarySymmetric
 
+section CompleteHomogeneousSymmetric
+
+open Finset Multiset Sym
+
+variable [DecidableEq σ] [DecidableEq τ]
+
+/-- The `n`th complete homogeneous symmetric `MvPolynomial σ R`. -/
+def hsymm (n : ℕ) : MvPolynomial σ R := ∑ s : Sym σ n, (s.1.map X).prod
+
+lemma hsymm_def (n : ℕ) : hsymm σ R n = ∑ s : Sym σ n, (s.1.map X).prod := rfl
+
+/--
+`hsymmMu` is the product of the symmetric polynomials `hsymm μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition.
+-/
+def hsymmMu {n : ℕ} (μ : n.Partition) : MvPolynomial σ R :=
+  muProduct σ R (hsymm σ R) μ
+
+lemma hsymmMu_def {n : ℕ} (μ : n.Partition) : hsymmMu σ R μ =
+    Multiset.prod (μ.parts.map (hsymm σ R)) := rfl
+
+@[simp]
+theorem hsymm_zero : hsymm σ R 0 = 1 := by
+  simp only [hsymm, univ_unique, eq_nil_of_card_zero, val_eq_coe, Sym.coe_nil, Multiset.map_zero,
+    prod_zero, sum_const, Finset.card_singleton, one_smul]
+
+@[simp]
+theorem hsymm_one : hsymm σ R 1 = ∑ i, X i := by
+  simp only [hsymm, univ_unique]
+  symm
+  apply Fintype.sum_equiv oneEquiv
+  intro i
+  simp only [oneEquiv_apply, Multiset.map_singleton, Multiset.prod_singleton]
+
+theorem hsymmMu_zero : hsymmMu σ R (Nat.Partition.indiscrete 0) = 1 := by
+  simp only [hsymmMu, hsymm_zero, muProduct_indiscrete_zero]
+
+@[simp]
+theorem hsymmMu_onePart (n : ℕ) : hsymmMu σ R (Nat.Partition.indiscrete n) = hsymm σ R n := by
+  cases n
+  · simp only [hsymmMu, hsymm_zero, muProduct_indiscrete_zero]
+  · simp only [hsymmMu, gt_iff_lt, Nat.zero_lt_succ, muProduct_indiscrete_of_pos]
+
+theorem map_hsymm (n : ℕ) (f : R →+* S) : map f (hsymm σ R n) = hsymm σ S n := by
+  simp_rw [hsymm, map_sum, ← Multiset.prod_hom']
+  simp only [val_eq_coe, map_X]
+
+theorem rename_hsymm (n : ℕ) (e : σ ≃ τ) : rename e (hsymm σ R n) = hsymm τ R n := by
+  simp_rw [hsymm, map_sum, ← prod_hom', rename_X]
+  apply Fintype.sum_equiv (equivCongr e)
+  simp only [val_eq_coe, equivCongr_apply, Sym.coe_map, Multiset.map_map, Function.comp_apply,
+    implies_true]
+
+theorem hsymm_isSymmetric (n : ℕ) : IsSymmetric (hsymm σ R n) := rename_hsymm _ _ n
+
+end CompleteHomogeneousSymmetric
+
 section PowerSum
 
 open Finset
 
-variable (σ R) [CommSemiring R] [Fintype σ] [Fintype τ]
-
 /-- The degree-`n` power sum -/
 def psum (n : ℕ) : MvPolynomial σ R := ∑ i, X i ^ n
 
 lemma psum_def (n : ℕ) : psum σ R n = ∑ i, X i ^ n := rfl
 
+/--
+`psumMu` is the product of the symmetric polynomials `psum μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition.
+-/
+def psumMu {n : ℕ} (μ : n.Partition) : MvPolynomial σ R :=
+  muProduct σ R (psum σ R) μ
+
+lemma psumMu_def {n : ℕ} (μ : n.Partition) : psumMu σ R μ =
+    Multiset.prod (μ.parts.map (psum σ R)) := rfl
+
 @[simp]
 theorem psum_zero : psum σ R 0 = Fintype.card σ := by
-  simp only [psum, _root_.pow_zero, ← cast_card]
-  exact rfl
+  simp [psum, _root_.pow_zero, ← cast_card]
+  rfl
 
 @[simp]
 theorem psum_one : psum σ R 1 = ∑ i, X i := by
   simp only [psum, _root_.pow_one]
 
+@[simp]
+theorem psumMu_zero : psumMu σ R (Nat.Partition.indiscrete 0) = 1 := by
+  simp only [psumMu, muProduct_indiscrete_zero]
+
+@[simp]
+theorem psumMu_onePart (n : ℕ) (npos : n > 0) :
+    psumMu σ R (Nat.Partition.indiscrete n) = psum σ R n := by
+  simp only [psumMu, npos, muProduct_indiscrete_of_pos]
+
 @[simp]
 theorem rename_psum (n : ℕ) (e : σ ≃ τ) : rename e (psum σ R n) = psum τ R n := by
   simp_rw [psum, map_sum, map_pow, rename_X, e.sum_comp (X · ^ n)]
@@ -328,4 +457,64 @@ theorem psum_isSymmetric (n : ℕ) : IsSymmetric (psum σ R n) := rename_psum _
 
 end PowerSum
 
+section MonomialSymmetric
+-- open Multiset
+
+variable [DecidableEq σ] [DecidableEq τ]
+
+/-- The monomial symmetric `MvPolynomial σ R` with exponent set μ. -/
+def msymm {n : ℕ} (μ : n.Partition) : MvPolynomial σ R :=
+  ∑ s : {a : Sym σ n // Nat.Partition.ofSym a = μ},  (s.1.1.map X).prod
+
+lemma msymm_def {n : ℕ} (μ : n.Partition) : msymm σ R μ =
+    ∑ s : {a : Sym σ n // Nat.Partition.ofSym a = μ}, (s.1.1.map X).prod := rfl
+
+@[simp]
+theorem msymm_zero : msymm σ R (Nat.Partition.indiscrete 0) = 1 := by
+  rw [msymm, Fintype.sum_subsingleton]
+  swap
+  exact ⟨(Sym.nil : Sym σ 0), by rfl⟩
+  simp only [Sym.val_eq_coe, Sym.coe_nil, Multiset.map_zero, Multiset.prod_zero]
+
+@[simp]
+theorem msymm_one : msymm σ R (Nat.Partition.indiscrete 1) = ∑ i, X i := by
+  symm
+  let f : σ ≃ { a // Nat.Partition.ofSym a = Nat.Partition.indiscrete 1 } := {
+    toFun := fun a => ⟨Sym.oneEquiv a, by ext; simp⟩
+    invFun := fun a => Sym.oneEquiv.symm a.1
+    left_inv := by intro a; simp only [Sym.oneEquiv_apply]; rfl
+    right_inv := by intro a; simp only [Equiv.apply_symm_apply, Subtype.coe_eta]
+  }
+  apply Fintype.sum_equiv f
+  intro i
+  have : (X i : MvPolynomial σ R) = Multiset.prod (Multiset.map X {i}) := by
+    simp only [Multiset.map_singleton, Multiset.prod_singleton]
+  rw [this]
+  rfl
+
+@[simp]
+theorem rename_msymm {n : ℕ} (μ : n.Partition) (e : σ ≃ τ) :
+    rename e (msymm σ R μ) = msymm τ R μ := by
+  simp only [msymm._eq_1, Sym.val_eq_coe, map_sum]
+  let f : {a : Sym σ n // Nat.Partition.ofSym a = μ} ≃ {a : Sym τ n // Nat.Partition.ofSym a = μ} :=
+  {
+    toFun := fun a => ⟨Sym.equivCongr e a, by
+      simp only [Sym.equivCongr_apply, Nat.Partition.ofSym_map, a.2]⟩
+    invFun := fun a => ⟨Sym.equivCongr e.symm a, by
+      simp only [Sym.equivCongr_apply, Nat.Partition.ofSym_map, a.2]⟩
+    left_inv := by intro a; simp
+    right_inv := by intro a; simp
+  }
+  apply Fintype.sum_equiv f
+  intro a
+  rw [← Multiset.prod_hom, Multiset.map_map]
+  congr
+  simp only [Sym.equivCongr_apply, Equiv.coe_fn_mk, Sym.coe_map, Multiset.map_map,
+    Function.comp_apply, rename_X, f]
+
+theorem msymm_isSymmetric {n : ℕ} (μ : n.Partition) : IsSymmetric (msymm σ R μ) :=
+  rename_msymm _ _ μ
+
+end MonomialSymmetric
+
 end MvPolynomial