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 cardinalityn
whose elements are ins
.Finset.sym2
: The symmetric square of a finset.s.sym2
is all the pairs whose elements are ins
.
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)
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)
@[simp]
theorem
Finset.mem_sym2_iff
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{m : Sym2 α}
:
m ∈ Finset.sym2 s ↔ ∀ (a : α), a ∈ m → a ∈ s
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
@[simp]
@[simp]
Alias of the reverse direction of Finset.sym2_nonempty
.
@[simp]
theorem
Finset.sym2_univ
{α : Type u_1}
[DecidableEq α]
[Fintype α]
:
Finset.sym2 Finset.univ = Finset.univ
@[simp]
theorem
Finset.sym2_singleton
{α : Type u_1}
[DecidableEq α]
(a : α)
:
Finset.sym2 {a} = {Sym2.diag a}
@[simp]
theorem
Finset.diag_mem_sym2_iff
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{a : α}
:
Sym2.diag a ∈ Finset.sym2 s ↔ a ∈ s
@[simp]
theorem
Finset.sym2_mono
{α : Type u_1}
[DecidableEq α]
{s : Finset α}
{t : Finset α}
(h : s ⊆ t)
:
Finset.sym2 s ⊆ Finset.sym2 t
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
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
@[simp]
@[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 : α), a ∈ m → a ∈ s
@[simp]
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 : Finset.Nonempty s)
(n : ℕ)
:
Finset.Nonempty (Finset.sym s n)
@[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 = ∅)
:
@[simp]
@[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
@[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_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
@[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
@[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
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 n
th symmetric power of {a} ∪ s
is
in 1-1 correspondence with the disjoint union of the n - i
th symmetric powers of s
,
for 0 ≤ i ≤ n
.