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.

theorem Finset.isDiag_mk'_of_mem_diag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a ∈ Finset.diag s) :

Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)

source

theorem Finset.not_isDiag_mk'_of_mem_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α × α} (h : a ∈ Finset.offDiag s) :

¬Sym2.IsDiag (Quotient.mk (Sym2.Rel.setoid α) a)

source

def Finset.sym2 {α : Type u_1} [DecidableEq α] (s : Finset α) :

Finset (Sym2 α)

Lifts a finset to Sym2 α. s.sym2 is the finset of all pairs with elements in s.

Instances For

source

@[simp]

theorem Finset.mem_sym2_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {m : Sym2 α} :

m ∈ Finset.sym2 s ↔ ∀ (a : α), a ∈ m → a ∈ s

source

theorem Finset.mk'_mem_sym2_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {b : α} :

Quotient.mk (Sym2.Rel.setoid α) (a, b) ∈ Finset.sym2 s ↔ a ∈ s ∧ b ∈ s

source

@[simp]

theorem Finset.sym2_empty {α : Type u_1} [DecidableEq α] :

Finset.sym2 ∅ = ∅

source

@[simp]

theorem Finset.sym2_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} :

Finset.sym2 s = ∅ ↔ s = ∅

source

@[simp]

theorem Finset.sym2_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} :

Finset.Nonempty (Finset.sym2 s) ↔ Finset.Nonempty s

source

theorem Finset.nonempty.sym2 {α : Type u_1} [DecidableEq α] {s : Finset α} :

Finset.Nonempty s → Finset.Nonempty (Finset.sym2 s)

Alias of the reverse direction of Finset.sym2_nonempty.

source

@[simp]

theorem Finset.sym2_univ {α : Type u_1} [DecidableEq α] [Fintype α] :

Finset.sym2 Finset.univ = Finset.univ

source

@[simp]

theorem Finset.sym2_singleton {α : Type u_1} [DecidableEq α] (a : α) :

Finset.sym2 {a} = {Sym2.diag a}

source

@[simp]

theorem Finset.diag_mem_sym2_mem_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :

(∀ (b : α), b ∈ Sym2.diag a → b ∈ s) ↔ a ∈ s

source

theorem Finset.diag_mem_sym2_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} :

Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s

source

@[simp]

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

Finset.sym2 s ⊆ Finset.sym2 t

source

theorem Finset.image_diag_union_image_offDiag {α : Type u_1} [DecidableEq α] {s : Finset α} :

Finset.image Quotient.mk' (Finset.diag s) ∪ Finset.image Quotient.mk' (Finset.offDiag s) = Finset.sym2 s

source

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

DecidableEq (Sym α n)

source

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)

Instances For

source

@[simp]

theorem Finset.sym_zero {α : Type u_1} [DecidableEq α] {s : Finset α} :

Finset.sym s 0 = {∅}

source

@[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)

source

@[simp]

theorem Finset.mem_sym_iff {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} :

m ∈ Finset.sym s n ↔ ∀ (a : α), a ∈ m → a ∈ s

source

@[simp]

theorem Finset.sym_empty {α : Type u_1} [DecidableEq α] (n : ℕ) :

Finset.sym ∅ (n + 1) = ∅

source

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

Sym.replicate n a ∈ Finset.sym s n

source

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

Finset.Nonempty (Finset.sym s n)

source

@[simp]

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

Finset.sym {a} n = {Sym.replicate n a}

source

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

s = ∅

source

@[simp]

theorem Finset.sym_eq_empty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} :

Finset.sym s n = ∅ ↔ n ≠ 0 ∧ s = ∅

source

@[simp]

theorem Finset.sym_nonempty {α : Type u_1} [DecidableEq α] {s : Finset α} {n : ℕ} {m : Sym α n} :

Finset.Nonempty (Finset.sym s n) ↔ n = 0 ∨ Finset.Nonempty s

source

@[simp]

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

Finset.sym Finset.univ n = Finset.univ

source

@[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

source

@[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

source

@[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

source

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

source

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)

source

@[simp]

theorem Finset.symInsertEquiv_apply_snd_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : ℕ} (h : ¬a ∈ s) (m : { x // x ∈ Finset.sym (insert a s) n }) :

↑(↑(Finset.symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd

source

@[simp]

theorem Finset.symInsertEquiv_apply_fst {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : ℕ} (h : ¬a ∈ s) (m : { x // x ∈ Finset.sym (insert a s) n }) :

(↑(Finset.symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst

source

@[simp]

theorem Finset.symInsertEquiv_symm_apply_coe {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : ℕ} (h : ¬a ∈ s) (m : (i : Fin (n + 1)) × { x // x ∈ Finset.sym s (n - ↑i) }) :

↑(↑(Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd

source

def Finset.symInsertEquiv {α : Type u_1} [DecidableEq α] {s : Finset α} {a : α} {n : ℕ} (h : ¬a ∈ s) :

{ x // x ∈ Finset.sym (insert a s) n } ≃ (i : Fin (n + 1)) × { x // 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.

Instances For