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

Mathlib/Combinatorics/Enumerative/Partition.lean

@@ -99,6 +99,34 @@ 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
+    show ∑ a ∈ s.1.toFinset, count a s.1 = n
+    rw [toFinset_sum_count_eq]
+    exact s.2
+
+variable {n : ℕ} {σ τ : Type*} [DecidableEq σ] [DecidableEq τ]
+
+lemma ofSym_map (e : σ ≃ τ) (s : Sym σ n) :
+    ofSym (s.map e) = ofSym s := by
+  simp only [ofSym, Sym.val_eq_coe, Sym.coe_map, toFinset_val, mk.injEq]
+  rw [Multiset.dedup_map_of_injective e.injective]
+  simp only [map_map, Function.comp_apply]
+  congr; funext i
+  rw [← Multiset.count_map_eq_count' e _ e.injective]
+
+/-- An equivalence between `σ` and `τ` induces an equivalence between the subtypes of `Sym σ n` and
+`Sym τ n` corresponding to a given partition. -/
+def ofSym_shape_equiv (μ : Partition n) (e : σ ≃ τ) :
+    {x : Sym σ n // ofSym x = μ} ≃ {x : Sym τ n // ofSym x = μ} where
+  toFun := fun x => ⟨Sym.equivCongr e x, by simp [ofSym_map, x.2]⟩
+  invFun := fun x => ⟨Sym.equivCongr e.symm x, by simp [ofSym_map, x.2]⟩
+  left_inv := by intro x; simp
+  right_inv := by intro x; simp
+
 /-- The partition of exactly one part. -/
 def indiscrete (n : ℕ) : Partition n := ofSums n {n} rfl
 #align nat.partition.indiscrete_partition Nat.Partition.indiscrete
@@ -123,6 +151,21 @@ instance UniquePartitionZero : Unique (Partition 0) where
 instance UniquePartitionOne : Unique (Partition 1) where
   uniq _ := Partition.ext _ _ <| by simp
 
+lemma ofSym_one (s : Sym σ 1) : ofSym s = indiscrete 1 := by
+  ext; simp
+
+/-- The equivalence between `σ` and `1`-tuples of elements of σ -/
+def ofSym_equiv_onePart (σ : Type*) [DecidableEq σ] : σ ≃
+    { a : Sym σ 1 // ofSym a = indiscrete 1 } where
+  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]
+
+@[simp]
+lemma ofSym_equiv_onePart_apply (i : σ) :
+    ((ofSym_equiv_onePart σ) i : Multiset σ) = {i} := rfl
+
 /-- The number of times a positive integer `i` appears in the partition `ofSums n l hl` is the same
 as the number of times it appears in the multiset `l`.
 (For `i = 0`, `Partition.non_zero` combined with `Multiset.count_eq_zero_of_not_mem` gives that

Mathlib/Data/Sym/Basic.lean

@@ -534,6 +534,19 @@ 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 := (Equiv.subtypeQuotientEquivQuotientSubtype
+      (·.length = 1) _ (fun l ↦ Iff.rfl) (fun l l' ↦ by rfl) s).liftOn
+    (fun l ↦ l.1.head <| List.length_pos.mp <| by simp)
+    fun ⟨_, _⟩ ⟨_, h⟩ ↦ fun 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/NewtonIdentities.lean

@@ -198,7 +198,7 @@ private theorem esymm_to_weight (k : ℕ) : k * esymm σ R k =
 private theorem esymm_mul_psum_summand_to_weight (k : ℕ) (a : ℕ × ℕ) (ha : a ∈ antidiagonal k) :
     ∑ A ∈ powersetCard a.fst univ, ∑ j, weight σ R k (A, j) =
     (-1) ^ a.fst * esymm σ R a.fst * psum σ R a.snd := by
-  simp only [esymm, psum_def, weight, ← mul_assoc, mul_sum]
+  simp only [esymm, psum, weight, ← mul_assoc, mul_sum]
   rw [sum_comm]
   refine sum_congr rfl fun x _ ↦ ?_
   rw [sum_mul]

Mathlib/RingTheory/MvPolynomial/Symmetric.lean

@@ -4,16 +4,16 @@ 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.Combinatorics.Enumerative.Partition
 
 #align_import ring_theory.mv_polynomial.symmetric from "leanprover-community/mathlib"@"2f5b500a507264de86d666a5f87ddb976e2d8de4"
 
 /-!
 # Symmetric Polynomials and Elementary Symmetric Polynomials
 
-This file defines symmetric `MvPolynomial`s and elementary symmetric `MvPolynomial`s.
-We also prove some basic facts about them.
+This file defines symmetric `MvPolynomial`s and the bases of elementary, complete homogeneous,
+power sum, and monomial symmetric `MvPolynomial`s. We also prove some basic facts about them.
 
 ## Main declarations
 
@@ -23,15 +23,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)
@@ -70,27 +79,22 @@ end Multiset
 
 namespace MvPolynomial
 
-variable {σ : Type*} {R : Type*}
-variable {τ : Type*} {S : Type*}
+variable {σ τ : Type*} {R S : Type*}
 
 /-- A `MvPolynomial φ` is symmetric if it is invariant under
 permutations of its variables by the `rename` operation -/
 def IsSymmetric [CommSemiring R] (φ : MvPolynomial σ R) : Prop :=
   ∀ e : Perm σ, rename e φ = φ
 #align mv_polynomial.is_symmetric MvPolynomial.IsSymmetric
 
-variable (σ R)
-
 /-- The subalgebra of symmetric `MvPolynomial`s. -/
-def symmetricSubalgebra [CommSemiring R] : Subalgebra R (MvPolynomial σ R) where
+def symmetricSubalgebra (σ R : Type*) [CommSemiring R] : Subalgebra R (MvPolynomial σ R) where
   carrier := setOf IsSymmetric
   algebraMap_mem' r e := rename_C e r
   mul_mem' ha hb e := by rw [map_mul, ha, hb]
   add_mem' ha hb e := by rw [map_add, ha, hb]
 #align mv_polynomial.symmetric_subalgebra MvPolynomial.symmetricSubalgebra
 
-variable {σ R}
-
 @[simp]
 theorem mem_symmetricSubalgebra [CommSemiring R] (p : MvPolynomial σ R) :
     p ∈ symmetricSubalgebra σ R ↔ p.IsSymmetric :=
@@ -174,24 +178,30 @@ 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 τ]
+
 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 ∈ powersetCard n univ, ∏ i ∈ t, X i
 #align mv_polynomial.esymm MvPolynomial.esymm
 
+/--
+`esymmPart` is the product of the symmetric polynomials `esymm μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition.
+-/
+def esymmPart {n : ℕ} (μ : n.Partition) : MvPolynomial σ R := (μ.parts.map (esymm σ R)).prod
+
 /-- 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
   exact funext fun n => (esymm_map_val X _ n).symm
 #align mv_polynomial.esymm_eq_multiset_esymm MvPolynomial.esymm_eq_multiset_esymm
 
-theorem aeval_esymm_eq_multiset_esymm [Algebra R S] (f : σ → S) (n : ℕ) :
+theorem aeval_esymm_eq_multiset_esymm [Algebra R S] (n : ℕ) (f : σ → S) :
     aeval f (esymm σ R n) = (univ.val.map f).esymm n := by
   simp_rw [esymm, aeval_sum, aeval_prod, aeval_X, esymm_map_val]
 #align mv_polynomial.aeval_esymm_eq_multiset_esymm MvPolynomial.aeval_esymm_eq_multiset_esymm
@@ -210,10 +220,18 @@ theorem esymm_eq_sum_monomial (n : ℕ) :
 #align mv_polynomial.esymm_eq_sum_monomial MvPolynomial.esymm_eq_sum_monomial
 
 @[simp]
-theorem esymm_zero : esymm σ R 0 = 1 := by
-  simp only [esymm, powersetCard_zero, sum_singleton, prod_empty]
+theorem esymm_zero : esymm σ R 0 = 1 := by simp [esymm]
 #align mv_polynomial.esymm_zero MvPolynomial.esymm_zero
 
+@[simp]
+theorem esymm_one : esymm σ R 1 = ∑ i, X i := by simp [esymm, powersetCard_one]
+
+theorem esymmPart_zero : esymmPart σ R (.indiscrete 0) = 1 := by simp [esymmPart]
+
+@[simp]
+theorem esymmPart_onePart (n : ℕ) : esymmPart σ R (.indiscrete n) = esymm σ R n := by
+  cases n <;> simp [esymmPart]
+
 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
@@ -230,12 +248,10 @@ theorem rename_esymm (n : ℕ) (e : σ ≃ τ) : rename e (esymm σ R n) = esymm
     _ = ∑ t ∈ powersetCard n univ, ∏ i ∈ t, X i := by rw [map_univ_equiv]
 #align mv_polynomial.rename_esymm MvPolynomial.rename_esymm
 
-theorem esymm_isSymmetric (n : ℕ) : IsSymmetric (esymm σ R n) := by
-  intro
-  rw [rename_esymm]
+theorem esymm_isSymmetric (n : ℕ) : IsSymmetric (esymm σ R n) := rename_esymm _ _ n
 #align mv_polynomial.esymm_is_symmetric MvPolynomial.esymm_isSymmetric
 
-theorem support_esymm'' (n : ℕ) [DecidableEq σ] [Nontrivial R] :
+theorem support_esymm'' [DecidableEq σ] [Nontrivial R] (n : ℕ) :
     (esymm σ R n).support =
       (powersetCard n (univ : Finset σ)).biUnion fun t =>
         (Finsupp.single (∑ i ∈ t, Finsupp.single i 1) (1 : R)).support := by
@@ -260,23 +276,21 @@ theorem support_esymm'' (n : ℕ) [DecidableEq σ] [Nontrivial R] :
   all_goals intro x y; simp [Finsupp.support_single_disjoint]
 #align mv_polynomial.support_esymm'' MvPolynomial.support_esymm''
 
-theorem support_esymm' (n : ℕ) [DecidableEq σ] [Nontrivial R] :
-    (esymm σ R n).support =
-      (powersetCard n (univ : Finset σ)).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1} := by
+theorem support_esymm' [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
+    (powersetCard n (univ : Finset σ)).biUnion fun t => {∑ i ∈ t, Finsupp.single i 1} := by
   rw [support_esymm'']
   congr
   funext
   exact Finsupp.support_single_ne_zero _ one_ne_zero
 #align mv_polynomial.support_esymm' MvPolynomial.support_esymm'
 
-theorem support_esymm (n : ℕ) [DecidableEq σ] [Nontrivial R] :
-    (esymm σ R n).support =
-      (powersetCard n (univ : Finset σ)).image fun t => ∑ i ∈ t, Finsupp.single i 1 := by
+theorem support_esymm [DecidableEq σ] [Nontrivial R] (n : ℕ) : (esymm σ R n).support =
+    (powersetCard n (univ : Finset σ)).image fun t => ∑ i ∈ t, Finsupp.single i 1 := by
   rw [support_esymm']
   exact biUnion_singleton
 #align mv_polynomial.support_esymm MvPolynomial.support_esymm
 
-theorem degrees_esymm [Nontrivial R] (n : ℕ) (hpos : 0 < n) (hn : n ≤ Fintype.card σ) :
+theorem degrees_esymm [Nontrivial R] {n : ℕ} (hpos : 0 < n) (hn : n ≤ Fintype.card σ) :
     (esymm σ R n).degrees = (univ : Finset σ).val := by
   classical
     have :
@@ -298,25 +312,69 @@ 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
+
+/-- `hsymmPart` is the product of the symmetric polynomials `hsymm μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition. -/
+def hsymmPart {n : ℕ} (μ : n.Partition) : MvPolynomial σ R := (μ.parts.map (hsymm σ R)).prod
+
+@[simp]
+theorem hsymm_zero : hsymm σ R 0 = 1 := by simp [hsymm, eq_nil_of_card_zero]
+
+@[simp]
+theorem hsymm_one : hsymm σ R 1 = ∑ i, X i := by
+  symm
+  apply Fintype.sum_equiv oneEquiv
+  simp only [oneEquiv_apply, Multiset.map_singleton, Multiset.prod_singleton, implies_true]
+
+theorem hsymmPart_zero : hsymmPart σ R (.indiscrete 0) = 1 := by simp [hsymmPart]
+
+@[simp]
+theorem hsymmPart_onePart (n : ℕ) : hsymmPart σ R (.indiscrete n) = hsymm σ R n := by
+  cases n <;> simp [hsymmPart]
+
+theorem map_hsymm (n : ℕ) (f : R →+* S) : map f (hsymm σ R n) = hsymm σ S n := by
+  simp [hsymm, ← Multiset.prod_hom']
+
+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
+
+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
+/-- `psumPart` is the product of the symmetric polynomials `psum μᵢ`,
+where `μ = (μ₁, μ₂, ...)` is a partition. -/
+def psumPart {n : ℕ} (μ : n.Partition) : MvPolynomial σ R := (μ.parts.map (psum σ R)).prod
+
+@[simp]
+theorem psum_zero : psum σ R 0 = Fintype.card σ := by simp [psum]
+
+@[simp]
+theorem psum_one : psum σ R 1 = ∑ i, X i := by simp [psum]
 
 @[simp]
-theorem psum_zero : psum σ R 0 = Fintype.card σ := by
-  simp only [psum, _root_.pow_zero, ← cast_card]
-  exact rfl
+theorem psumPart_zero : psumPart σ R (.indiscrete 0) = 1 := by simp [psumPart]
 
 @[simp]
-theorem psum_one : psum σ R 1 = ∑ i, X i := by
-  simp only [psum, _root_.pow_one]
+theorem psumPart_indiscrete {n : ℕ} (npos : n ≠ 0) :
+    psumPart σ R (.indiscrete n) = psum σ R n := by simp [psumPart, npos]
 
 @[simp]
 theorem rename_psum (n : ℕ) (e : σ ≃ τ) : rename e (psum σ R n) = psum τ R n := by
@@ -326,4 +384,37 @@ theorem psum_isSymmetric (n : ℕ) : IsSymmetric (psum σ R n) := rename_psum _
 
 end PowerSum
 
+section MonomialSymmetric
+
+variable [DecidableEq σ] [DecidableEq τ] {n : ℕ}
+
+/-- The monomial symmetric `MvPolynomial σ R` with exponent set μ. -/
+def msymm  (μ : n.Partition) : MvPolynomial σ R :=
+  ∑ s : {a : Sym σ n // .ofSym a = μ},  (s.1.1.map X).prod
+
+@[simp]
+theorem msymm_zero : msymm σ R (.indiscrete 0) = 1 := by
+  rw [msymm, Fintype.sum_subsingleton _ ⟨(Sym.nil : Sym σ 0), by rfl⟩]
+  simp
+
+@[simp]
+theorem msymm_one : msymm σ R (.indiscrete 1) = ∑ i, X i := by
+  symm
+  apply Fintype.sum_equiv (Nat.Partition.ofSym_equiv_onePart σ)
+  simp
+
+@[simp]
+theorem rename_msymm (μ : n.Partition) (e : σ ≃ τ) :
+    rename e (msymm σ R μ) = msymm τ R μ := by
+  rw [msymm, map_sum]
+  apply Fintype.sum_equiv (Nat.Partition.ofSym_shape_equiv μ e)
+  intro
+  rw [← Multiset.prod_hom, Multiset.map_map, Nat.Partition.ofSym_shape_equiv]
+  simp
+
+theorem msymm_isSymmetric (μ : n.Partition) : IsSymmetric (msymm σ R μ) :=
+  rename_msymm _ _ μ
+
+end MonomialSymmetric
+
 end MvPolynomial