feat(data/finset/sym): Symmetric powers of a finset (#11142)

This defines `finset.sym` and `finset.sym2`, which are the `finset` analogs of `sym` and `sym2`, in a new file `data.finset.sym`.

Author: YaelDillies

src/data/finset/basic.lean

@@ -2545,6 +2545,10 @@ lemma disjoint_filter_filter {s t : finset α} {p q : α → Prop} [decidable_pr
   (disjoint s t) → disjoint (s.filter p) (t.filter q) :=
 disjoint.mono (filter_subset _ _) (filter_subset _ _)
 
+lemma disjoint_filter_filter_neg (s : finset α) (p : α → Prop) [decidable_pred p] :
+  disjoint (s.filter p) (s.filter $ λ a, ¬ p a) :=
+(disjoint_filter.2 $ λ a _, id).symm
+
 lemma disjoint_iff_disjoint_coe {α : Type*} {a b : finset α} [decidable_eq α] :
   disjoint a b ↔ disjoint (↑a : set α) (↑b : set α) :=
 by { rw [finset.disjoint_left, set.disjoint_left], refl }

src/data/finset/prod.lean

@@ -110,6 +110,10 @@ let ⟨xy, hxy⟩ := h in ⟨xy.2, (mem_product.1 hxy).2⟩
 @[simp] lemma nonempty_product : (s.product t).nonempty ↔ s.nonempty ∧ t.nonempty :=
 ⟨λ h, ⟨h.fst, h.snd⟩, λ h, h.1.product h.2⟩
 
+@[simp] lemma product_eq_empty {s : finset α} {t : finset β} : s.product t = ∅ ↔ s = ∅ ∨ t = ∅ :=
+by rw [←not_nonempty_iff_eq_empty, nonempty_product, not_and_distrib, not_nonempty_iff_eq_empty,
+  not_nonempty_iff_eq_empty]
+
 @[simp] lemma singleton_product {a : α} :
   ({a} : finset α).product t = t.map ⟨prod.mk a, prod.mk.inj_left _⟩ :=
 by { ext ⟨x, y⟩, simp [and.left_comm, eq_comm] }
@@ -172,5 +176,10 @@ end
 
 @[simp] lemma off_diag_empty : (∅ : finset α).off_diag = ∅ := rfl
 
+@[simp] lemma diag_union_off_diag : s.diag ∪ s.off_diag = s.product s :=
+filter_union_filter_neg_eq _ _
+
+@[simp] lemma disjoint_diag_off_diag : disjoint s.diag s.off_diag := disjoint_filter_filter_neg _ _
+
 end diag
 end finset

src/data/finset/sym.lean

@@ -0,0 +1,159 @@
+/-
+Copyright (c) 2021 Yaël Dillies. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Yaël Dillies
+-/
+import data.finset.prod
+import data.sym.sym2
+
+/-!
+# Symmetric powers of a finset
+
+This file defines the symmetric powers of a finset as `finset (sym α n)` and `finset (sym2 α)`.
+
+## Main declarations
+
+* `finset.sym`: The symmetric power of a finset. `s.sym n` is all the multisets of cardinality `n`
+  whose elements are in `s`.
+* `finset.sym2`: The symmetric square of a finset. `s.sym2` is all the pairs whose elements are in
+  `s`.
+
+## TODO
+
+`finset.sym` forms a Galois connection between `finset α` and `finset (sym α n)`. Similar for
+`finset.sym2`.
+-/
+
+namespace finset
+variables {α : Type*} [decidable_eq α] {s t : finset α} {a b : α}
+
+lemma is_diag_mk_of_mem_diag {a : α × α} (h : a ∈ s.diag) : sym2.is_diag ⟦a⟧ :=
+(sym2.is_diag_iff_proj_eq _).2 ((mem_diag _ _).1 h).2
+
+lemma not_is_diag_mk_of_mem_off_diag {a : α × α} (h : a ∈ s.off_diag) : ¬ sym2.is_diag ⟦a⟧ :=
+by { rw sym2.is_diag_iff_proj_eq, exact ((mem_off_diag _ _).1 h).2.2 }
+
+section sym2
+variables {m : sym2 α}
+
+/-- Lifts a finset to `sym2 α`. `s.sym2` is the finset of all pairs with elements in `s`. -/
+protected def sym2 (s : finset α) : finset (sym2 α) := (s.product s).image quotient.mk
+
+@[simp] lemma mem_sym2_iff : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s :=
+begin
+  refine mem_image.trans
+    ⟨_, λ h, ⟨m.out, mem_product.2 ⟨h _ m.out_fst_mem, h _ m.out_snd_mem⟩, m.out_eq⟩⟩,
+  rintro ⟨⟨a, b⟩, h, rfl⟩,
+  rw sym2.ball,
+  rwa mem_product at h,
+end
+
+lemma mk_mem_sym2_iff : ⟦(a, b)⟧ ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s := by rw [mem_sym2_iff, sym2.ball]
+
+@[simp] lemma sym2_empty : (∅ : finset α).sym2 = ∅ := rfl
+
+@[simp] lemma sym2_eq_empty : s.sym2 = ∅ ↔ s = ∅ :=
+by rw [finset.sym2, image_eq_empty, product_eq_empty, or_self]
+
+@[simp] lemma sym2_nonempty : s.sym2.nonempty ↔ s.nonempty :=
+by rw [finset.sym2, nonempty.image_iff, nonempty_product, and_self]
+
+alias sym2_nonempty ↔ _ finset.nonempty.sym2
+
+attribute [protected] finset.nonempty.sym2
+
+@[simp] lemma sym2_univ [fintype α] : (univ : finset α).sym2 = univ := rfl
+
+@[simp] lemma sym2_singleton (a : α) : ({a} : finset α).sym2 = {sym2.diag a} :=
+by rw [finset.sym2, singleton_product_singleton, image_singleton, sym2.diag]
+
+@[simp] lemma diag_mem_sym2_iff : sym2.diag a ∈ s.sym2 ↔ a ∈ s := mk_mem_sym2_iff.trans $ and_self _
+
+@[simp] lemma sym2_mono (h : s ⊆ t) : s.sym2 ⊆ t.sym2 :=
+λ m he, mem_sym2_iff.2 $ λ a ha, h $ mem_sym2_iff.1 he _ ha
+
+lemma image_diag_union_image_off_diag :
+  s.diag.image quotient.mk ∪ s.off_diag.image quotient.mk = s.sym2 :=
+by { rw [←image_union, diag_union_off_diag], refl }
+
+end sym2
+
+section sym
+variables {n : ℕ} {m : sym α n}
+
+/-- Lifts a finset to `sym α n`. `s.sym n` is the finset of all unordered tuples of cardinality `n`
+with elements in `s`. -/
+protected def sym (s : finset α) : Π n, finset (sym α n)
+| 0       := {∅}
+| (n + 1) := s.sup $ λ a, (sym n).image $ _root_.sym.cons a
+
+@[simp] lemma sym_zero : s.sym 0 = {∅} := rfl
+@[simp] lemma sym_succ : s.sym (n + 1) = s.sup (λ a, (s.sym n).image $ sym.cons a) := rfl
+
+@[simp] lemma mem_sym_iff : m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s :=
+begin
+  induction n with n ih,
+  { refine mem_singleton.trans ⟨_, λ _, sym.eq_nil_of_card_zero _⟩,
+    rintro rfl,
+    exact λ a ha, ha.elim },
+  refine mem_sup.trans  ⟨_, λ h, _⟩,
+  { rintro ⟨a, ha, he⟩ b hb,
+    rw mem_image at he,
+    obtain ⟨m, he, rfl⟩ := he,
+    rw sym.mem_cons at hb,
+    obtain rfl | hb := hb,
+    { exact ha },
+    { exact ih.1 he _ hb } },
+  { obtain ⟨a, m, rfl⟩ := m.exists_eq_cons_of_succ,
+    exact ⟨a, h _ $ sym.mem_cons_self _ _,
+      mem_image_of_mem _ $ ih.2 $ λ b hb, h _ $ sym.mem_cons_of_mem hb⟩ }
+end
+
+@[simp] lemma sym_empty (n : ℕ) : (∅ : finset α).sym (n + 1) = ∅ := rfl
+
+lemma repeat_mem_sym (ha : a ∈ s) (n : ℕ) : sym.repeat a n ∈ s.sym n :=
+mem_sym_iff.2 $ λ b hb, by rwa (sym.mem_repeat.1 hb).2
+
+protected lemma nonempty.sym (h : s.nonempty) (n : ℕ) : (s.sym n).nonempty :=
+let ⟨a, ha⟩ := h in ⟨_, repeat_mem_sym ha n⟩
+
+@[simp] lemma sym_singleton (a : α) (n : ℕ) : ({a} : finset α).sym n = {sym.repeat a n} :=
+eq_singleton_iff_nonempty_unique_mem.2 ⟨(singleton_nonempty _).sym n,
+  λ s hs, sym.eq_repeat_iff.2 $ λ b hb, eq_of_mem_singleton $ mem_sym_iff.1 hs _ hb⟩
+
+lemma eq_empty_of_sym_eq_empty (h : s.sym n = ∅) : s = ∅ :=
+begin
+  rw ←not_nonempty_iff_eq_empty at ⊢ h,
+  exact λ hs, h (hs.sym _),
+end
+
+@[simp] lemma sym_eq_empty : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅ :=
+begin
+  cases n,
+  { exact iff_of_false (singleton_ne_empty _) (λ h, (h.1 rfl).elim) },
+  { refine ⟨λ h, ⟨n.succ_ne_zero, eq_empty_of_sym_eq_empty h⟩, _⟩,
+    rintro ⟨_, rfl⟩,
+    exact sym_empty _ }
+end
+
+@[simp] lemma sym_nonempty : (s.sym n).nonempty ↔ n = 0 ∨ s.nonempty :=
+by simp_rw [nonempty_iff_ne_empty, ne.def, sym_eq_empty, not_and_distrib, not_ne_iff]
+
+alias sym2_nonempty ↔ _ finset.nonempty.sym2
+
+attribute [protected] finset.nonempty.sym2
+
+@[simp] lemma sym_univ [fintype α] (n : ℕ) : (univ : finset α).sym n = univ :=
+eq_univ_iff_forall.2 $ λ s, mem_sym_iff.2 $ λ a _, mem_univ _
+
+@[simp] lemma sym_mono (h : s ⊆ t) (n : ℕ): s.sym n ⊆ t.sym n :=
+λ m hm, mem_sym_iff.2 $ λ a ha, h $ mem_sym_iff.1 hm _ ha
+
+@[simp] lemma sym_inter (s t : finset α) (n : ℕ) : (s ∩ t).sym n = s.sym n ∩ t.sym n :=
+by { ext m, simp only [mem_inter, mem_sym_iff, imp_and_distrib, forall_and_distrib] }
+
+@[simp] lemma sym_union (s t : finset α) (n : ℕ) : s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n :=
+union_subset (sym_mono (subset_union_left s t) n) (sym_mono (subset_union_right s t) n)
+
+end sym
+end finset

src/data/sym/basic.lean

@@ -38,6 +38,8 @@ show these are equivalent in `sym.sym_equiv_sym'`.
 -/
 def sym (α : Type u) (n : ℕ) := {s : multiset α // s.card = n}
 
+instance sym.has_coe (α : Type*) (n : ℕ) : has_coe (sym α n) (multiset α) := coe_subtype
+
 /--
 This is the `list.perm` setoid lifted to `vector`.
 
@@ -51,7 +53,7 @@ local attribute [instance] vector.perm.is_setoid
 
 namespace sym
 
-variables {α : Type u} {n : ℕ}
+variables {α : Type u} {n : ℕ} {s : sym α n} {a b : α}
 
 /--
 The unique element in `sym α 0`.
@@ -157,6 +159,17 @@ def repeat (a : α) (n : ℕ) : sym α n := ⟨multiset.repeat a n, multiset.car
 
 lemma repeat_succ {a : α} {n : ℕ} : repeat a n.succ = a :: repeat a n := rfl
 
+lemma coe_repeat : (repeat a n : multiset α) = multiset.repeat a n := rfl
+
+@[simp] lemma mem_repeat : b ∈ repeat a n ↔ n ≠ 0 ∧ b = a := multiset.mem_repeat
+
+lemma eq_repeat_iff : s = repeat a n ↔ ∀ b ∈ s, b = a :=
+begin
+  rw [subtype.ext_iff, coe_repeat],
+  convert multiset.eq_repeat',
+  exact s.2.symm,
+end
+
 lemma exists_mem (s : sym α n.succ) : ∃ a, a ∈ s :=
 multiset.card_pos_iff_exists_mem.1 $ s.2.symm ▸ n.succ_pos
 

src/data/sym/card.lean

@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Yaël Dillies, Bhavik Mehta
 -/
 import algebra.big_operators.basic
-import data.sym.sym2
+import data.finset.sym
 
 /-!
 # Stars and bars
@@ -42,8 +42,7 @@ namespace sym2
 variables {α : Type*} [decidable_eq α]
 
 /-- The `diag` of `s : finset α` is sent on a finset of `sym2 α` of card `s.card`. -/
-lemma card_image_diag (s : finset α) :
-  (s.diag.image quotient.mk).card = s.card :=
+lemma card_image_diag (s : finset α) : (s.diag.image quotient.mk).card = s.card :=
 begin
   rw [card_image_of_inj_on, diag_card],
   rintro ⟨x₀, x₁⟩ hx _ _ h,
@@ -105,10 +104,21 @@ begin
   exact and_iff_right ⟨a, mem_univ _, ha⟩,
 end
 
-protected lemma card [fintype α] :
-  card (sym2 α) = card α * (card α + 1) / 2 :=
-by rw [←fintype.card_congr (@equiv.sum_compl _ is_diag (sym2.is_diag.decidable_pred α)),
-  fintype.card_sum, card_subtype_diag, card_subtype_not_diag, nat.choose_two_right, add_comm,
-  ←nat.triangle_succ, nat.succ_sub_one, mul_comm]
+/-- Finset **stars and bars** for the case `n = 2`. -/
+lemma _root_.finset.card_sym2 (s : finset α) : s.sym2.card = s.card * (s.card + 1) / 2 :=
+begin
+  rw [←image_diag_union_image_off_diag, card_union_eq, sym2.card_image_diag,
+    sym2.card_image_off_diag, nat.choose_two_right, add_comm, ←nat.triangle_succ, nat.succ_sub_one,
+    mul_comm],
+  rintro m he,
+  rw [inf_eq_inter, mem_inter, mem_image, mem_image] at he,
+  obtain ⟨⟨a, ha, rfl⟩, b, hb, hab⟩ := he,
+  refine not_is_diag_mk_of_mem_off_diag hb _,
+  rw hab,
+  exact is_diag_mk_of_mem_diag ha,
+end
+
+/-- Type **stars and bars** for the case `n = 2`. -/
+protected lemma card [fintype α] : card (sym2 α) = card α * (card α + 1) / 2 := finset.card_sym2 _
 
 end sym2

src/data/sym/sym2.lean

@@ -176,6 +176,21 @@ instance : has_mem α (sym2 α) := ⟨mem⟩
 lemma mem_mk_left (x y : α) : x ∈ ⟦(x, y)⟧ := ⟨y, rfl⟩
 lemma mem_mk_right (x y : α) : y ∈ ⟦(x, y)⟧ := eq_swap.subst $ mem_mk_left y x
 
+@[simp] lemma mem_iff {a b c : α} : a ∈ ⟦(b, c)⟧ ↔ a = b ∨ a = c :=
+{ mp  := by { rintro ⟨_, h⟩, rw eq_iff at h, tidy },
+  mpr := by { rintro ⟨_⟩; subst a, { apply mem_mk_left }, apply mem_mk_right } }
+
+lemma out_fst_mem (e : sym2 α) : e.out.1 ∈ e := ⟨e.out.2, by rw [prod.mk.eta, e.out_eq]⟩
+lemma out_snd_mem (e : sym2 α) : e.out.2 ∈ e := ⟨e.out.1, by rw [eq_swap, prod.mk.eta, e.out_eq]⟩
+
+lemma ball {p : α → Prop} {a b : α} : (∀ c ∈ ⟦(a, b)⟧, p c) ↔ p a ∧ p b :=
+begin
+  refine ⟨λ h, ⟨h _ $ mem_mk_left _ _, h _ $ mem_mk_right _ _⟩, λ h c hc, _⟩,
+  obtain rfl | rfl := sym2.mem_iff.1 hc,
+  { exact h.1 },
+  { exact h.2 }
+end
+
 /--
 Given an element of the unordered pair, give the other element using `classical.some`.
 See also `mem.other'` for the computable version.
@@ -187,10 +202,6 @@ classical.some h
 lemma other_spec {a : α} {z : sym2 α} (h : a ∈ z) : ⟦(a, h.other)⟧ = z :=
 by erw ← classical.some_spec h
 
-@[simp] lemma mem_iff {a b c : α} : a ∈ ⟦(b, c)⟧ ↔ a = b ∨ a = c :=
-{ mp  := by { rintro ⟨_, h⟩, rw eq_iff at h, tidy },
-  mpr := by { rintro ⟨_⟩; subst a, { apply mem_mk_left }, apply mem_mk_right } }
-
 lemma other_mem {a : α} {z : sym2 α} (h : a ∈ z) : h.other ∈ z :=
 by { convert mem_mk_right a h.other, rw other_spec h }