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.
• A Fintype (Sym2 α) instance that does not require DecidableEq α.

TODO

Finset.sym forms a Galois connection between Finset α and Finset (Sym α n). Similar for Finset.sym2.

def Finset.sym2 {α : Type u_1} (s : Finset α) : Finset (Sym2 α)

s.sym2 is the finset of all unordered pairs of elements from s. It is the image of s ×ˢ s under the quotient α × α → Sym2 α.

@[simp]

theorem Finset.sym2_val {α : Type u_1} (s : Finset α) : s.sym2.val = s.val.sym2

theorem Finset.mk_mem_sym2_iff {α : Type u_1} {s : Finset α} {a b : α} : s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s

@[simp]

theorem Finset.mem_sym2_iff {α : Type u_1} {s : Finset α} {m : Sym2 α} : m ∈ s.sym2 ↔ ∀ a ∈ m, a ∈ s

@[simp]

theorem Finset.coe_sym2 {α : Type u_1} {m : Finset α} : ↑m.sym2 = (↑m).sym2

theorem Finset.sym2_cons {α : Type u_1} (a : α) (s : Finset α) (ha : a ∉ s) : (cons a s ha).sym2 = (map (Sym2.mkEmbedding a) (cons a s ha)).disjUnion s.sym2 ⋯

theorem Finset.sym2_insert {α : Type u_1} [DecidableEq α] (a : α) (s : Finset α) : (insert a s).sym2 = image (fun (b : α) => s(a, b)) (insert a s) ∪ s.sym2

theorem Finset.sym2_map {α : Type u_1} {β : Type u_2} (f : α ↪ β) (s : Finset α) : (map f s).sym2 = map f.sym2Map s.sym2

theorem Finset.sym2_image {α : Type u_1} {β : Type u_2} [DecidableEq β] (f : α → β) (s : Finset α) : (image f s).sym2 = image (Sym2.map f) s.sym2

@[implicit_reducible]

instance Sym2.instFintype {α : Type u_1} [Fintype α] : Fintype (Sym2 α)

@[simp]

theorem Finset.sym2_univ {α : Type u_1} [Fintype α] (inst : Fintype (Sym2 α) := Sym2.instFintype) : univ.sym2 = univ

@[simp]

theorem Finset.sym2_mono {α : Type u_1} {s t : Finset α} (h : s ⊆ t) : s.sym2 ⊆ t.sym2

theorem Finset.monotone_sym2 {α : Type u_1} : Monotone Finset.sym2

theorem Finset.injective_sym2 {α : Type u_1} : Function.Injective Finset.sym2

theorem Finset.strictMono_sym2 {α : Type u_1} : StrictMono Finset.sym2

theorem Finset.sym2_toFinset {α : Type u_1} [DecidableEq α] (m : Multiset α) : m.toFinset.sym2 = m.sym2.toFinset

@[simp]

theorem Finset.sym2_empty {α : Type u_1} : ∅.sym2 = ∅

@[simp]

theorem Finset.sym2_eq_empty {α : Type u_1} {s : Finset α} : s.sym2 = ∅ ↔ s = ∅

@[simp]

theorem Finset.sym2_nonempty {α : Type u_1} {s : Finset α} : s.sym2.Nonempty ↔ s.Nonempty

theorem Finset.Nonempty.sym2 {α : Type u_1} {s : Finset α} : s.Nonempty → s.sym2.Nonempty

Alias of the reverse direction of Finset.sym2_nonempty.

@[simp]

theorem Finset.sym2_singleton {α : Type u_1} (a : α) : {a}.sym2 = {Sym2.diag a}

theorem Finset.card_sym2 {α : Type u_1} (s : Finset α) : s.sym2.card = (s.card + 1).choose 2

Finset stars and bars for the case n = 2.

theorem Finset.sym2_eq_image {α : Type u_1} {s : Finset α} [DecidableEq α] : s.sym2 = image (Function.uncurry Sym2.mk) (s ×ˢ s)

theorem Finset.isDiag_mk_of_mem_diag {α : Type u_1} {s : Finset α} {a b : α} (h : (a, b) ∈ s.diag) : s(a, b).IsDiag

theorem Finset.not_isDiag_mk_of_mem_offDiag {α : Type u_1} {s : Finset α} {a b : α} (h : (a, b) ∈ s.offDiag) : ¬s(a, b).IsDiag

@[simp]

theorem Finset.diag_mem_sym2_mem_iff {α : Type u_1} {s : Finset α} {a : α} : (∀ b ∈ Sym2.diag a, b ∈ s) ↔ a ∈ s

theorem Finset.diag_mem_sym2_iff {α : Type u_1} {s : Finset α} {a : α} : Sym2.diag a ∈ s.sym2 ↔ a ∈ s

theorem Finset.image_diag_union_image_offDiag {α : Type u_1} {s : Finset α} [DecidableEq α] : image (Function.uncurry Sym2.mk) s.diag ∪ image (Function.uncurry Sym2.mk) s.offDiag = s.sym2

def Finset.sym {α : Type u_1} [DecidableEq α] (s : Finset α) (n : ℕ) : Finset (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.

@[simp]

theorem Finset.sym_zero {α : Type u_1} {s : Finset α} [DecidableEq α] : s.sym 0 = {∅}

@[simp]

theorem Finset.sym_succ {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} : s.sym (n + 1) = s.sup fun (a : α) => image (Sym.cons a) (s.sym n)

@[simp]

theorem Finset.mem_sym_iff {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} {m : Sym α n} : m ∈ s.sym n ↔ ∀ a ∈ m, a ∈ s

theorem Finset.sym_map {α : Type u_1} {β : Type u_2} [DecidableEq α] [DecidableEq β] {n : ℕ} (g : α ↪ β) (s : Finset α) : (map g s).sym n = map { toFun := Sym.map ⇑g, inj' := ⋯ } (s.sym n)

theorem Finset.sym_empty {α : Type u_1} [DecidableEq α] (n : ℕ) : ∅.sym (n + 1) = ∅

theorem Finset.replicate_mem_sym {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] (ha : a ∈ s) (n : ℕ) : Sym.replicate n a ∈ s.sym n

theorem Finset.Nonempty.sym {α : Type u_1} {s : Finset α} [DecidableEq α] (h : s.Nonempty) (n : ℕ) : (s.sym n).Nonempty

@[simp]

theorem Finset.sym_singleton {α : Type u_1} [DecidableEq α] (a : α) (n : ℕ) : {a}.sym n = {Sym.replicate n a}

theorem Finset.eq_empty_of_sym_eq_empty {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} (h : s.sym n = ∅) : s = ∅

@[simp]

theorem Finset.sym_eq_empty {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} : s.sym n = ∅ ↔ n ≠ 0 ∧ s = ∅

@[simp]

theorem Finset.sym_nonempty {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} : (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty

@[simp]

theorem Finset.sym_univ {α : Type u_1} [DecidableEq α] [Fintype α] (n : ℕ) : univ.sym n = univ

@[simp]

theorem Finset.sym_mono {α : Type u_1} {s t : Finset α} [DecidableEq α] (h : s ⊆ t) (n : ℕ) : s.sym n ⊆ t.sym n

@[simp]

theorem Finset.sym_inter {α : Type u_1} [DecidableEq α] (s t : Finset α) (n : ℕ) : (s ∩ t).sym n = s.sym n ∩ t.sym n

@[simp]

theorem Finset.sym_union {α : Type u_1} [DecidableEq α] (s t : Finset α) (n : ℕ) : s.sym n ∪ t.sym n ⊆ (s ∪ t).sym n

theorem Finset.sym_fill_mem {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} (a : α) {i : Fin (n + 1)} {m : Sym α (n - ↑i)} (h : m ∈ s.sym (n - ↑i)) : Sym.fill a i m ∈ (insert a s).sym n

theorem Finset.sym_filterNe_mem {α : Type u_1} {s : Finset α} [DecidableEq α] {n : ℕ} {m : Sym α n} (a : α) (h : m ∈ s.sym n) : (Sym.filterNe a m).snd ∈ (s.erase a).sym (n - ↑(Sym.filterNe a m).fst)

def Finset.symInsertEquiv {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) : ↥((insert a s).sym n) ≃ (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))

If a does not belong to the finset s, then the nth symmetric power of {a} ∪ s is in 1-1 correspondence with the disjoint union of the n - ith symmetric powers of s, for 0 ≤ i ≤ n.

@[simp]

theorem Finset.symInsertEquiv_apply_snd_coe {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : ↥((insert a s).sym n)) : ↑((symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd

@[simp]

theorem Finset.symInsertEquiv_apply_fst {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : ↥((insert a s).sym n)) : ((symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst

@[simp]

theorem Finset.symInsertEquiv_symm_apply_coe {α : Type u_1} {s : Finset α} {a : α} [DecidableEq α] {n : ℕ} (h : a ∉ s) (m : (i : Fin (n + 1)) × ↥(s.sym (n - ↑i))) : ↑((symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd

theorem Finset.val_prod_eq_prod_count_pow {α : Type u_1} [DecidableEq α] [CommMonoid α] {n : ℕ} {k : Sym α n} {s : Finset α} (hk : k ∈ s.sym n) : (↑k).prod = ∏ d ∈ s, d ^ Multiset.count d ↑k

theorem Finset.val_sum_eq_sum_count_nsmul {α : Type u_1} [DecidableEq α] [AddCommMonoid α] {n : ℕ} {k : Sym α n} {s : Finset α} (hk : k ∈ s.sym n) : (↑k).sum = ∑ d ∈ s, Multiset.count d ↑k • d