feat(ring_theory/polynomial/symmetric): degrees_esymm (#6718)

A lot of API also added for finset, finsupp, multiset, powerset_len
    
Co-authored-by: Hanting Zhang <hantingzhang03@gmail.com>

src/algebra/big_operators/basic.lean

@@ -91,6 +91,10 @@ theorem prod_eq_fold [comm_monoid β] (s : finset α) (f : α → β) :
   (∏ x in s, f x) = s.fold (*) 1 f :=
 rfl
 
+@[simp] lemma sum_multiset_singleton (s : finset α) :
+  s.sum (λ x, x ::ₘ 0) = s.val :=
+by simp [sum_eq_multiset_sum]
+
 end finset
 
 

src/data/finset/lattice.lean

@@ -670,9 +670,16 @@ lemma supr_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
   (⨆ x ∈ s.image f, g x) = (⨆ y ∈ s, g (f y)) :=
 by rw [← supr_coe, coe_image, supr_image, supr_coe]
 
-lemma sup_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
-  s.sup (g ∘ f) = (s.image f).sup g :=
-by { simp_rw [sup_eq_supr, comp_app], rw supr_finset_image, }
+lemma sup_finset_image {β γ : Type*} [semilattice_sup_bot β]
+  (f : γ → α) (g : α → β) (s : finset γ) :
+  (s.image f).sup g = s.sup (g ∘ f) :=
+begin
+  classical,
+  apply finset.induction_on s,
+  { simp },
+  { intros a s' ha ih,
+    rw [sup_insert, image_insert, sup_insert, ih] }
+end
 
 lemma infi_finset_image {f : γ → α} {g : α → β} {s : finset γ} :
   (⨅ x ∈ s.image f, g x) = (⨅ y ∈ s, g (f y)) :=

src/data/finset/powerset.lean

@@ -3,7 +3,7 @@ Copyright (c) 2018 Mario Carneiro. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Mario Carneiro
 -/
-import data.finset.basic
+import data.finset.lattice
 
 /-!
 # The powerset of a finset
@@ -106,6 +106,45 @@ theorem powerset_len_eq_filter {n} {s : finset α} :
   powerset_len n s = (powerset s).filter (λ x, x.card = n) :=
 by { ext, simp [mem_powerset_len] }
 
+lemma powerset_len_succ_insert [decidable_eq α] {x : α} {s : finset α} (h : x ∉ s) (n : ℕ) :
+  powerset_len n.succ (insert x s) = powerset_len n.succ s ∪ (powerset_len n s).image (insert x) :=
+begin
+  rw [powerset_len_eq_filter, powerset_insert, filter_union, ←powerset_len_eq_filter],
+  congr,
+  rw [powerset_len_eq_filter, image_filter],
+  congr' 1,
+  ext t,
+  simp only [mem_powerset, mem_filter, function.comp_app, and.congr_right_iff],
+  intro ht,
+  have : x ∉ t := λ H, h (ht H),
+  simp [card_insert_of_not_mem this, nat.succ_inj']
+end
+
+lemma powerset_len_nonempty {n : ℕ} {s : finset α} (h : n < s.card) :
+  (powerset_len n s).nonempty :=
+begin
+  classical,
+  induction s using finset.induction_on with x s hx IH generalizing n,
+  { simpa using h },
+  { cases n,
+    { simp },
+    { rw [card_insert_of_not_mem hx, nat.succ_lt_succ_iff] at h,
+      rw powerset_len_succ_insert hx,
+      refine nonempty.mono _ ((IH h).image (insert x)),
+      convert (subset_union_right _ _) } }
+end
+
+@[simp] lemma powerset_len_self (s : finset α) :
+  powerset_len s.card s = {s} :=
+begin
+  ext,
+  rw [mem_powerset_len, mem_singleton],
+  split,
+  { exact λ ⟨hs, hc⟩, eq_of_subset_of_card_le hs hc.ge },
+  { rintro rfl,
+    simp }
+end
+
 lemma powerset_card_bUnion [decidable_eq (finset α)] (s : finset α) :
   finset.powerset s = (range (s.card + 1)).bUnion (λ i, powerset_len i s) :=
 begin
@@ -117,5 +156,22 @@ begin
     exact mem_powerset.mpr (mem_powerset_len.mp ha).1, }
 end
 
+lemma powerset_len_sup [decidable_eq α] (u : finset α) (n : ℕ) (hn : n < u.card) :
+  (powerset_len n.succ u).sup id = u :=
+begin
+  apply le_antisymm,
+  { simp [mem_powerset_len, and.comm] },
+  { rw [sup_eq_bUnion, le_iff_subset, subset_iff],
+    cases (nat.succ_le_of_lt hn).eq_or_lt with h' h',
+    { simp [h'] },
+    { intros x hx,
+      simp only [mem_bUnion, exists_prop, id.def],
+      obtain ⟨t, ht⟩ : ∃ t, t ∈ powerset_len n (u.erase x) := powerset_len_nonempty _,
+      { refine ⟨insert x t, _, mem_insert_self _ _⟩,
+        rw [←insert_erase hx, powerset_len_succ_insert (not_mem_erase _ _)],
+        exact mem_union_right _ (mem_image_of_mem _ ht) },
+      { rwa [card_erase_of_mem hx, nat.lt_pred_iff] } } }
+end
+
 end powerset_len
 end finset

src/data/finsupp/basic.lean

@@ -213,6 +213,9 @@ if_neg h
 lemma single_eq_update : ⇑(single a b) = function.update 0 a b :=
 by rw [single_eq_indicator, ← set.piecewise_eq_indicator, set.piecewise_singleton]
 
+lemma single_eq_pi_single : ⇑(single a b) = pi.single a b :=
+single_eq_update
+
 @[simp] lemma single_zero : (single a 0 : α →₀ M) = 0 :=
 coe_fn_injective $ by simpa only [single_eq_update, coe_zero]
   using function.update_eq_self a (0 : α → M)
@@ -284,6 +287,18 @@ lemma single_left_inj (h : b ≠ 0) :
   and_false, or_false, eq_self_iff_true, and_true] using H,
  λ H, by rw [H]⟩
 
+lemma support_single_ne_bot (i : α) (h : b ≠ 0) :
+  (single i b).support ≠ ⊥ :=
+begin
+  have : i ∈ (single i b).support := by simpa using h,
+  intro H,
+  simpa [H]
+end
+
+lemma support_single_disjoint {b' : M} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : α} :
+  disjoint (single i b).support (single j b').support ↔ i ≠ j :=
+by simpa [support_single_ne_zero, hb, hb'] using ne_comm
+
 @[simp] lemma single_eq_zero : single a b = 0 ↔ b = 0 :=
 by simp [ext_iff, single_eq_indicator]
 
@@ -1090,6 +1105,25 @@ lemma multiset_sum_sum_index
 multiset.induction_on f rfl $ assume a s ih,
 by rw [multiset.sum_cons, multiset.map_cons, multiset.sum_cons, sum_add_index h₀ h₁, ih]
 
+lemma support_sum_eq_bUnion {α : Type*} {ι : Type*} {M : Type*} [add_comm_monoid M]
+  {g : ι → α →₀ M} (s : finset ι) (h : ∀ i₁ i₂, i₁ ≠ i₂ → disjoint (g i₁).support (g i₂).support) :
+  (∑ i in s, g i).support = s.bUnion (λ i, (g i).support) :=
+begin
+  apply finset.induction_on s,
+  { simp },
+  { intros i s hi,
+    simp only [hi, sum_insert, not_false_iff, bUnion_insert],
+    intro hs,
+    rw [finsupp.support_add_eq, hs],
+    rw [hs],
+    intros x hx,
+    simp only [mem_bUnion, exists_prop, inf_eq_inter, ne.def, mem_inter] at hx,
+    obtain ⟨hxi, j, hj, hxj⟩ := hx,
+    have hn : i ≠ j := λ H, hi (H.symm ▸ hj),
+    apply h _ _ hn,
+    simp [hxi, hxj] }
+end
+
 lemma multiset_map_sum [has_zero M] {f : α →₀ M} {m : β → γ} {h : α → M → multiset β} :
   multiset.map m (f.sum h) = f.sum (λa b, (h a b).map m) :=
 (f.support.sum_hom _).symm
@@ -1493,6 +1527,20 @@ lemma to_multiset_apply (f : α →₀ ℕ) : f.to_multiset = f.sum (λ a n, n 
 @[simp] lemma to_multiset_single (a : α) (n : ℕ) : to_multiset (single a n) = n •ℕ {a} :=
 by rw [to_multiset_apply, sum_single_index]; apply zero_nsmul
 
+lemma to_multiset_sum {ι : Type*} {f : ι → α →₀ ℕ} (s : finset ι) :
+  finsupp.to_multiset (∑ i in s, f i) = ∑ i in s, finsupp.to_multiset (f i) :=
+begin
+  apply finset.induction_on s,
+  { simp },
+  { intros i s hi,
+    simp [hi] }
+end
+
+lemma to_multiset_sum_single {ι : Type*} (s : finset ι) (n : ℕ) :
+  finsupp.to_multiset (∑ i in s, single i n) = n •ℕ s.val :=
+by simp_rw [to_multiset_sum, finsupp.to_multiset_single, multiset.singleton_eq_singleton,
+            sum_nsmul, sum_multiset_singleton]
+
 lemma card_to_multiset (f : α →₀ ℕ) : f.to_multiset.card = f.sum (λa, id) :=
 by simp [to_multiset_apply, add_monoid_hom.map_finsupp_sum, function.id_def]
 

src/data/fintype/basic.lean

@@ -1431,3 +1431,13 @@ def trunc_sigma_of_exists {α} [fintype α] {P : α → Prop} [decidable_pred P]
 @trunc_of_nonempty_fintype (Σ' a, P a) (exists.elim h $ λ a ha, ⟨⟨a, ha⟩⟩) _
 
 end trunc
+
+namespace multiset
+
+variables [fintype α] [decidable_eq α]
+
+@[simp] lemma count_univ (a : α) :
+  count a finset.univ.val = 1 :=
+count_eq_one_of_mem finset.univ.nodup (finset.mem_univ _)
+
+end multiset

src/data/multiset/lattice.lean

@@ -59,6 +59,15 @@ by rw [← sup_erase_dup, erase_dup_ext.2, sup_erase_dup, sup_add]; simp
   (ndinsert a s).sup = a ⊔ s.sup :=
 by rw [← sup_erase_dup, erase_dup_ext.2, sup_erase_dup, sup_cons]; simp
 
+lemma nodup_sup_iff {α : Type*} [decidable_eq α] {m : multiset (multiset α) } :
+  m.sup.nodup ↔ ∀ (a : multiset α), a ∈ m → a.nodup :=
+begin
+  apply m.induction_on,
+  { simp },
+  { intros a s h,
+    simp [h] }
+end
+
 end sup
 
 /-! ### inf -/

src/data/set/basic.lean

@@ -1746,6 +1746,28 @@ begin
     rw [hz x hx, hz y hy] }
 end
 
+@[simp] lemma pairwise_on_empty {α} (r : α → α → Prop) :
+  (∅ : set α).pairwise_on r :=
+λ _, by simp
+
+lemma pairwise_on_insert_of_symmetric {α} {s : set α} {a : α} {r : α → α → Prop}
+  (hr : symmetric r) :
+  (insert a s).pairwise_on r ↔ s.pairwise_on r ∧ ∀ b ∈ s, a ≠ b → r a b :=
+begin
+  refine ⟨λ h, ⟨_, _⟩, λ h, _⟩,
+  { exact h.mono (s.subset_insert a) },
+  { intros b hb hn,
+    exact h a (s.mem_insert _) b (set.mem_insert_of_mem _ hb) hn },
+  { intros b hb c hc hn,
+    rw [mem_insert_iff] at hb hc,
+    rcases hb with (rfl | hb);
+    rcases hc with (rfl | hc),
+    { exact absurd rfl hn },
+    { exact h.right _ hc hn },
+    { exact hr (h.right _ hb hn.symm) },
+    { exact h.left _ hb _ hc hn } }
+end
+
 end set
 
 open set

src/data/support.lean

@@ -257,4 +257,8 @@ begin
   simp
 end
 
+lemma support_single_disjoint {b' : B} (hb : b ≠ 0) (hb' : b' ≠ 0) {i j : A} :
+  disjoint (function.support (single i b)) (function.support (single j b')) ↔ i ≠ j :=
+by simpa [support_single, hb, hb'] using ne_comm
+
 end pi

src/order/compactly_generated.lean

@@ -144,7 +144,7 @@ begin
   classical,
   rw is_compact_element_iff_le_of_directed_Sup_le,
   intros d hemp hdir hsup,
-  change f with id ∘ f, rw finset.sup_finset_image,
+  change f with id ∘ f, rw ←finset.sup_finset_image,
   apply finset.sup_le_of_le_directed d hemp hdir,
   rintros x hx,
   obtain ⟨p, ⟨hps, rfl⟩⟩ := finset.mem_image.mp hx,

src/ring_theory/noetherian.lean

@@ -289,7 +289,7 @@ begin
     { suffices : u.sup id ≤ s, from le_antisymm husup this,
       rw [sSup, finset.sup_eq_Sup], exact Sup_le_Sup huspan, },
     obtain ⟨t, ⟨hts, rfl⟩⟩ := finset.subset_image_iff.mp huspan,
-    rw [←finset.sup_finset_image, function.comp.left_id, finset.sup_eq_supr, supr_rw,
+    rw [finset.sup_finset_image, function.comp.left_id, finset.sup_eq_supr, supr_rw,
       ←span_eq_supr_of_singleton_spans, eq_comm] at ssup,
     exact ⟨t, ssup⟩, },
 end

src/ring_theory/polynomial/symmetric.lean

@@ -188,6 +188,55 @@ end
 lemma esymm_is_symmetric (n : ℕ) : is_symmetric (esymm σ R n) :=
 by { intro, rw rename_esymm }
 
+lemma support_esymm'' (n : ℕ) [decidable_eq σ] [nontrivial R] :
+  (esymm σ R n).support = (powerset_len n (univ : finset σ)).bUnion
+    (λ t, (finsupp.single (∑ (i : σ) in t, finsupp.single i 1) (1:R)).support) :=
+begin
+  rw esymm_eq_sum_monomial,
+  simp only [monomial],
+  convert finsupp.support_sum_eq_bUnion (powerset_len n (univ : finset σ)) _,
+  intros s t hst d,
+  simp only [finsupp.support_single_ne_zero one_ne_zero, and_imp, inf_eq_inter, mem_inter,
+             mem_singleton],
+  rintro h rfl,
+  have := congr_arg finsupp.support h,
+  rw [finsupp.support_sum_eq_bUnion, finsupp.support_sum_eq_bUnion] at this,
+  { simp only [finsupp.support_single_ne_zero one_ne_zero, bUnion_singleton_eq_self] at this,
+    exact absurd this hst.symm },
+  all_goals { intros x y, simp [finsupp.support_single_disjoint] }
+end
+
+lemma support_esymm' (n : ℕ) [decidable_eq σ] [nontrivial R] :
+  (esymm σ R n).support =
+  (powerset_len n (univ : finset σ)).bUnion (λ t, {∑ (i : σ) in t, finsupp.single i 1}) :=
+begin
+  rw support_esymm'',
+  congr,
+  funext,
+  exact finsupp.support_single_ne_zero one_ne_zero
+end
+
+lemma support_esymm (n : ℕ) [decidable_eq σ] [nontrivial R] :
+  (esymm σ R n).support =
+  (powerset_len n (univ : finset σ)).image (λ t, ∑ (i : σ) in t, finsupp.single i 1) :=
+by { rw support_esymm', exact bUnion_singleton }
+
+lemma degrees_esymm [nontrivial R]
+  (n : ℕ) (hpos : 0 < n) (hn : n ≤ fintype.card σ) :
+  (esymm σ R n).degrees = (univ : finset σ).val :=
+begin
+  classical,
+  have : (finsupp.to_multiset ∘ λ (t : finset σ), ∑ (i : σ) in t, finsupp.single i 1) = finset.val,
+    { funext, simp [finsupp.to_multiset_sum_single] },
+  rw [degrees, support_esymm, sup_finset_image, this, ←comp_sup_eq_sup_comp],
+  { obtain ⟨k, rfl⟩ := nat.exists_eq_succ_of_ne_zero hpos.ne',
+    simpa using powerset_len_sup _ _ (nat.lt_of_succ_le hn) },
+  { intros,
+    simp only [union_val, sup_eq_union],
+    congr },
+  { simpa }
+end
+
 end elementary_symmetric
 
 end mv_polynomial