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
.- A
Fintype (Sym2 α)
instance that does not requireDecidableEq α
.
TODO #
Finset.sym
forms a Galois connection between Finset α
and Finset (Sym α n)
. Similar for
Finset.sym2
.
theorem
Finset.sym2_cons
{α : Type u_1}
(a : α)
(s : Finset α)
(ha : a ∉ s)
:
(Finset.cons a s ha).sym2 = (Finset.map (Sym2.mkEmbedding a) (Finset.cons a s ha)).disjUnion s.sym2 ⋯
theorem
Finset.sym2_insert
{α : Type u_1}
[DecidableEq α]
(a : α)
(s : Finset α)
:
(insert a s).sym2 = Finset.image (fun (b : α) => s(a, b)) (insert a s) ∪ s.sym2
theorem
Finset.sym2_map
{α : Type u_1}
{β : Type u_2}
(f : α ↪ β)
(s : Finset α)
:
(Finset.map f s).sym2 = Finset.map f.sym2Map s.sym2
theorem
Finset.sym2_image
{α : Type u_1}
{β : Type u_2}
[DecidableEq β]
(f : α → β)
(s : Finset α)
:
(Finset.image f s).sym2 = Finset.image (Sym2.map f) s.sym2
theorem
Finset.sym2_toFinset
{α : Type u_1}
[DecidableEq α]
(m : Multiset α)
:
m.toFinset.sym2 = m.sym2.toFinset
@[simp]
Alias of the reverse direction of Finset.sym2_nonempty
.
theorem
Finset.sym2_eq_image
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
:
s.sym2 = Finset.image Sym2.mk (s ×ˢ s)
theorem
Finset.isDiag_mk_of_mem_diag
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
{a : α × α}
(h : a ∈ s.diag)
:
(Sym2.mk a).IsDiag
theorem
Finset.not_isDiag_mk_of_mem_offDiag
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
{a : α × α}
(h : a ∈ s.offDiag)
:
theorem
Finset.image_diag_union_image_offDiag
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
:
Finset.image Sym2.mk s.diag ∪ Finset.image Sym2.mk s.offDiag = s.sym2
Equations
- Finset.instDecidableEqSym = inferInstanceAs (DecidableEq { s : Multiset α // Multiset.card s = n })
@[simp]
theorem
Finset.sym_succ
{α : Type u_1}
{s : Finset α}
[DecidableEq α]
{n : ℕ}
:
s.sym (n + 1) = s.sup fun (a : α) => Finset.image (Sym.cons a) (s.sym n)
@[simp]
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 = ∅)
:
@[simp]
@[simp]
theorem
Finset.sym_univ
{α : Type u_1}
[DecidableEq α]
[Fintype α]
(n : ℕ)
:
Finset.univ.sym n = Finset.univ
@[simp]
theorem
Finset.sym_mono
{α : Type u_1}
{s t : Finset α}
[DecidableEq α]
(h : s ⊆ t)
(n : ℕ)
:
s.sym n ⊆ t.sym n
@[simp]
@[simp]
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)
:
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
.
Equations
- One or more equations did not get rendered due to their size.
Instances For
@[simp]
theorem
Finset.symInsertEquiv_apply_fst
{α : Type u_1}
{s : Finset α}
{a : α}
[DecidableEq α]
{n : ℕ}
(h : a ∉ s)
(m : { x : Sym α n // x ∈ (insert a s).sym n })
:
((Finset.symInsertEquiv h) m).fst = (Sym.filterNe a ↑m).fst
@[simp]
theorem
Finset.symInsertEquiv_apply_snd_coe
{α : Type u_1}
{s : Finset α}
{a : α}
[DecidableEq α]
{n : ℕ}
(h : a ∉ s)
(m : { x : Sym α n // x ∈ (insert a s).sym n })
:
↑((Finset.symInsertEquiv h) m).snd = (Sym.filterNe a ↑m).snd
@[simp]
theorem
Finset.symInsertEquiv_symm_apply_coe
{α : Type u_1}
{s : Finset α}
{a : α}
[DecidableEq α]
{n : ℕ}
(h : a ∉ s)
(m : (i : Fin (n + 1)) × { x : Sym α (n - ↑i) // x ∈ s.sym (n - ↑i) })
:
↑((Finset.symInsertEquiv h).symm m) = Sym.fill a m.fst ↑m.snd