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.

@[simp]

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

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 α.

Equations

• Finset.sym2 s = { val := Multiset.sym2 s.val, nodup := (_ : Multiset.Nodup (Multiset.sym2 s.val)) }

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

@[simp]

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

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

Equations

• Sym2.instFintype = { elems := Finset.sym2 Finset.univ, complete := (_ : ∀ (x : Sym2 α), x ∈ Finset.sym2 Finset.univ) }

@[simp]

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

@[simp]

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

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 α) : Finset.sym2 (Multiset.toFinset m) = Multiset.toFinset (Multiset.sym2 m)

@[simp]

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

@[simp]

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

@[simp]

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

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

Alias of the reverse direction of Finset.sym2_nonempty.

@[simp]

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

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

Finset stars and bars for the case n = 2.

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

theorem Finset.isDiag_mk_of_mem_diag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a ∈ Finset.diag s) : Sym2.IsDiag (Sym2.mk a)

theorem Finset.not_isDiag_mk_of_mem_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a ∈ Finset.offDiag s) : ¬Sym2.IsDiag (Sym2.mk a)

@[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 ∈ Finset.sym2 s ↔ a ∈ s

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

instance Finset.instDecidableEqSym {α : Type u_1} [DecidableEq α] {n : ℕ} : DecidableEq (Sym α n)

Equations

• Finset.instDecidableEqSym = Subtype.instDecidableEqSubtype

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.

Equations

• Finset.sym s 0 = {∅}
• Finset.sym s (Nat.succ n) = Finset.sup s fun (a : α) => Finset.image (Sym.cons a) (Finset.sym s n)

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

@[simp]

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

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

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

@[simp]

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

@[simp]

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

@[simp]

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

def Finset.symInsertEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : ℕ} (h : a ∉ s) : { x : Sym α n // x ∈ Finset.sym (insert a s) n } ≃ (i : Fin (n + 1)) × { x : Sym α (n - ↑i) // x ∈ Finset.sym s (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.

Equations

• One or more equations did not get rendered due to their size.