data.sym.basic

Symmetric powers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

This file defines symmetric powers of a type. The nth symmetric power consists of homogeneous n-tuples modulo permutations by the symmetric group.

The special case of 2-tuples is called the symmetric square, which is addressed in more detail in data.sym.sym2.

TODO: This was created as supporting material for sym2; it needs a fleshed-out interface.

Tags #

symmetric powers

def sym (α : Type u_1) (n : ) :
Type u_1

The nth symmetric power is n-tuples up to permutation. We define it as a subtype of multiset since these are well developed in the library. We also give a definition sym.sym' in terms of vectors, and we show these are equivalent in sym.sym_equiv_sym'.

Equations
Instances for sym
@[protected, instance]
def sym.has_coe (α : Type u_1) (n : ) :
has_coe (sym α n) (multiset α)
Equations
@[reducible]
def vector.perm.is_setoid (α : Type u_1) (n : ) :
setoid (vector α n)

This is the list.perm setoid lifted to vector.

Equations
theorem sym.coe_injective {α : Type u_1} {n : } :
@[simp, norm_cast]
theorem sym.coe_inj {α : Type u_1} {n : } {s₁ s₂ : sym α n} :
s₁ = s₂ s₁ = s₂
@[simp]
theorem sym.mk_coe {α : Type u_1} {n : } (m : multiset α) (h : = n) :
(sym.mk m h) = m
@[reducible]
def sym.mk {α : Type u_1} {n : } (m : multiset α) (h : = n) :
sym α n

Construct an element of the nth symmetric power from a multiset of cardinality n.

def sym.nil {α : Type u_1} :
sym α 0

The unique element in sym α 0.

Equations
@[simp]
theorem sym.coe_nil {α : Type u_1} :
def sym.cons {α : Type u_1} {n : } (a : α) (s : sym α n) :
sym α n.succ

Inserts an element into the term of sym α n, increasing the length by one.

Equations
@[simp]
theorem sym.cons_inj_right {α : Type u_1} {n : } (a : α) (s s' : sym α n) :
a ::ₛ s = a ::ₛ s' s = s'
@[simp]
theorem sym.cons_inj_left {α : Type u_1} {n : } (a a' : α) (s : sym α n) :
a ::ₛ s = a' ::ₛ s a = a'
theorem sym.cons_swap {α : Type u_1} {n : } (a b : α) (s : sym α n) :
a ::ₛ b ::ₛ s = b ::ₛ a ::ₛ s
theorem sym.coe_cons {α : Type u_1} {n : } (s : sym α n) (a : α) :
(a ::ₛ s) = a ::ₘ s
@[protected, instance]
def sym.has_lift {α : Type u_1} {n : } :
has_lift (vector α n) (sym α n)

This is the quotient map that takes a list of n elements as an n-tuple and produces an nth symmetric power.

Equations
@[simp]
theorem sym.of_vector_nil {α : Type u_1} :
@[simp]
theorem sym.of_vector_cons {α : Type u_1} {n : } (a : α) (v : n) :
(a ::ᵥ v) = a ::ₛ v
@[protected, instance]
def sym.has_mem {α : Type u_1} {n : } :
(sym α n)

α ∈ s means that a appears as one of the factors in s.

Equations
@[protected, instance]
def sym.decidable_mem {α : Type u_1} {n : } [decidable_eq α] (a : α) (s : sym α n) :
Equations
@[simp]
theorem sym.mem_mk {α : Type u_1} {n : } (a : α) (s : multiset α) (h : = n) :
a h a s
@[simp]
theorem sym.mem_cons {α : Type u_1} {n : } {s : sym α n} {a b : α} :
a b ::ₛ s a = b a s
@[simp]
theorem sym.mem_coe {α : Type u_1} {n : } {s : sym α n} {a : α} :
a s a s
theorem sym.mem_cons_of_mem {α : Type u_1} {n : } {s : sym α n} {a b : α} (h : a s) :
a b ::ₛ s
@[simp]
theorem sym.mem_cons_self {α : Type u_1} {n : } (a : α) (s : sym α n) :
a a ::ₛ s
theorem sym.cons_of_coe_eq {α : Type u_1} {n : } (a : α) (v : n) :
a ::ₛ v = (a ::ᵥ v)
theorem sym.sound {α : Type u_1} {n : } {a b : n} (h : a.val ~ b.val) :
def sym.erase {α : Type u_1} {n : } [decidable_eq α] (s : sym α (n + 1)) (a : α) (h : a s) :
sym α n

erase s a h is the sym that subtracts 1 from the multiplicity of a if a is present in the sym.

Equations
@[simp]
theorem sym.erase_mk {α : Type u_1} {n : } [decidable_eq α] (m : multiset α) (hc : = n + 1) (a : α) (h : a m) :
(sym.mk m hc).erase a h = sym.mk (m.erase a) _
@[simp]
theorem sym.coe_erase {α : Type u_1} {n : } [decidable_eq α] {s : sym α n.succ} {a : α} (h : a s) :
(s.erase a h) = s.erase a
@[simp]
theorem sym.cons_erase {α : Type u_1} {n : } [decidable_eq α] {s : sym α n.succ} {a : α} (h : a s) :
a ::ₛ s.erase a h = s
@[simp]
theorem sym.erase_cons_head {α : Type u_1} {n : } [decidable_eq α] (s : sym α n) (a : α) (h : a a ::ₛ s := _) :
(a ::ₛ s).erase a h = s
def sym.sym' (α : Type u_1) (n : ) :
Type u_1

Another definition of the nth symmetric power, using vectors modulo permutations. (See sym.)

Equations
• n =
Instances for sym.sym'
def sym.cons' {α : Type u_1} {n : } :
α n n.succ

This is cons but for the alternative sym' definition.

Equations
def sym.sym_equiv_sym' {α : Type u_1} {n : } :
sym α n n

Multisets of cardinality n are equivalent to length-n vectors up to permutations.

Equations
theorem sym.cons_equiv_eq_equiv_cons (α : Type u_1) (n : ) (a : α) (s : sym α n) :
@[protected, instance]
def sym.has_zero {α : Type u_1} :
has_zero (sym α 0)
Equations
@[protected, instance]
def sym.has_emptyc {α : Type u_1} :
Equations
theorem sym.eq_nil_of_card_zero {α : Type u_1} (s : sym α 0) :
@[protected, instance]
def sym.unique_zero {α : Type u_1} :
unique (sym α 0)
Equations
def sym.replicate {α : Type u_1} (n : ) (a : α) :
sym α n

replicate n a is the sym containing only a with multiplicity n.

Equations
theorem sym.replicate_succ {α : Type u_1} {a : α} {n : } :
= a ::ₛ
theorem sym.coe_replicate {α : Type u_1} {n : } {a : α} :
a) =
@[simp]
theorem sym.mem_replicate {α : Type u_1} {n : } {a b : α} :
b n 0 b = a
theorem sym.eq_replicate_iff {α : Type u_1} {n : } {s : sym α n} {a : α} :
s = (b : α), b s b = a
theorem sym.exists_mem {α : Type u_1} {n : } (s : sym α n.succ) :
(a : α), a s
theorem sym.exists_eq_cons_of_succ {α : Type u_1} {n : } (s : sym α n.succ) :
(a : α) (s' : sym α n), s = a ::ₛ s'
theorem sym.eq_replicate {α : Type u_1} {a : α} {n : } {s : sym α n} :
s = (b : α), b s b = a
theorem sym.eq_replicate_of_subsingleton {α : Type u_1} [subsingleton α] (a : α) {n : } (s : sym α n) :
s =
@[protected, instance]
def sym.subsingleton {α : Type u_1} [subsingleton α] (n : ) :
@[protected, instance]
def sym.inhabited_sym {α : Type u_1} [inhabited α] (n : ) :
inhabited (sym α n)
Equations
@[protected, instance]
def sym.inhabited_sym' {α : Type u_1} [inhabited α] (n : ) :
Equations
@[protected, instance]
def sym.is_empty {α : Type u_1} (n : ) [is_empty α] :
@[protected, instance]
def sym.unique {α : Type u_1} (n : ) [unique α] :
unique (sym α n)
Equations
theorem sym.replicate_right_inj {α : Type u_1} {a b : α} {n : } (h : n 0) :
= a = b
theorem sym.replicate_right_injective {α : Type u_1} {n : } (h : n 0) :
@[protected, instance]
def sym.nontrivial {α : Type u_1} (n : ) [nontrivial α] :
nontrivial (sym α (n + 1))
def sym.map {α : Type u_1} {β : Type u_2} {n : } (f : α β) (x : sym α n) :
sym β n

A function α → β induces a function sym α n → sym β n by applying it to every element of the underlying n-tuple.

Equations
@[simp]
theorem sym.mem_map {α : Type u_1} {β : Type u_2} {n : } {f : α β} {b : β} {l : sym α n} :
b l (a : α), a l f a = b
@[simp]
theorem sym.map_id' {α : Type u_1} {n : } (s : sym α n) :
sym.map (λ (x : α), x) s = s

Note: sym.map_id is not simp-normal, as simp ends up unfolding id with sym.map_congr

theorem sym.map_id {α : Type u_1} {n : } (s : sym α n) :
= s
@[simp]
theorem sym.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (g : β γ) (f : α β) (s : sym α n) :
(sym.map f s) = sym.map (g f) s
@[simp]
theorem sym.map_zero {α : Type u_1} {β : Type u_2} (f : α β) :
0 = 0
@[simp]
theorem sym.map_cons {α : Type u_1} {β : Type u_2} {n : } (f : α β) (a : α) (s : sym α n) :
(a ::ₛ s) = f a ::ₛ s
theorem sym.map_congr {α : Type u_1} {β : Type u_2} {n : } {f g : α β} {s : sym α n} (h : (x : α), x s f x = g x) :
s = s
@[simp]
theorem sym.map_mk {α : Type u_1} {β : Type u_2} {n : } {f : α β} {m : multiset α} {hc : = n} :
(sym.mk m hc) = sym.mk m) _
@[simp]
theorem sym.coe_map {α : Type u_1} {β : Type u_2} {n : } (s : sym α n) (f : α β) :
(sym.map f s) =
theorem sym.map_injective {α : Type u_1} {β : Type u_2} {f : α β} (hf : function.injective f) (n : ) :
def sym.equiv_congr {α : Type u_1} {β : Type u_2} {n : } (e : α β) :
sym α n sym β n

Mapping an equivalence α ≃ β using sym.map gives an equivalence between sym α n and sym β n.

Equations
@[simp]
theorem sym.equiv_congr_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : sym α n) :
x = x
@[simp]
theorem sym.equiv_congr_symm_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : sym β n) :
def sym.attach {α : Type u_1} {n : } (s : sym α n) :
sym {x // x s} n

"Attach" a proof that a ∈ s to each element a in s to produce an element of the symmetric power on {x // x ∈ s}.

Equations
@[simp]
theorem sym.attach_mk {α : Type u_1} {n : } {m : multiset α} {hc : = n} :
(sym.mk m hc).attach = _
@[simp]
theorem sym.coe_attach {α : Type u_1} {n : } (s : sym α n) :
theorem sym.attach_map_coe {α : Type u_1} {n : } (s : sym α n) :
= s
@[simp]
theorem sym.mem_attach {α : Type u_1} {n : } (s : sym α n) (x : {x // x s}) :
@[simp]
theorem sym.attach_nil {α : Type u_1} :
@[simp]
theorem sym.attach_cons {α : Type u_1} {n : } (x : α) (s : sym α n) :
(x ::ₛ s).attach = x, _⟩ ::ₛ sym.map (λ (x_1 : {x // x s}), x_1, _⟩) s.attach
@[protected]
def sym.cast {α : Type u_1} {n m : } (h : n = m) :
sym α n sym α m

Change the length of a sym using an equality. The simp-normal form is for the cast to be pushed outward.

Equations
@[simp]
theorem sym.cast_rfl {α : Type u_1} {n : } {s : sym α n} :
s = s
@[simp]
theorem sym.cast_cast {α : Type u_1} {n n' : } {s : sym α n} {n'' : } (h : n = n') (h' : n' = n'') :
@[simp]
theorem sym.coe_cast {α : Type u_1} {n m : } {s : sym α n} (h : n = m) :
@[simp]
theorem sym.mem_cast {α : Type u_1} {n m : } {s : sym α n} {a : α} (h : n = m) :
a (sym.cast h) s a s
def sym.append {α : Type u_1} {n n' : } (s : sym α n) (s' : sym α n') :
sym α (n + n')

Append a pair of sym terms.

Equations
@[simp]
theorem sym.append_inj_right {α : Type u_1} {n n' : } (s : sym α n) {t t' : sym α n'} :
s.append t = s.append t' t = t'
@[simp]
theorem sym.append_inj_left {α : Type u_1} {n n' : } {s s' : sym α n} (t : sym α n') :
s.append t = s'.append t s = s'
theorem sym.append_comm {α : Type u_1} {n' : } (s s' : sym α n') :
s.append s' = (sym.cast _) (s'.append s)
@[simp, norm_cast]
theorem sym.coe_append {α : Type u_1} {n n' : } (s : sym α n) (s' : sym α n') :
(s.append s') = s + s'
theorem sym.mem_append_iff {α : Type u_1} {n m : } {s : sym α n} {a : α} {s' : sym α m} :
a s.append s' a s a s'
def sym.fill {α : Type u_1} {n : } (a : α) (i : fin (n + 1)) (m : sym α (n - i)) :
sym α n

Fill a term m : sym α (n - i) with i copies of a to obtain a term of sym α n. This is a convenience wrapper for m.append (replicate i a) that adjusts the term using sym.cast.

Equations
theorem sym.coe_fill {α : Type u_1} {n : } {a : α} {i : fin (n + 1)} {m : sym α (n - i)} :
(sym.fill a i m) = m + a)
theorem sym.mem_fill_iff {α : Type u_1} {n : } {a b : α} {i : fin (n + 1)} {s : sym α (n - i)} :
a i s i 0 a = b a s
def sym.filter_ne {α : Type u_1} {n : } [decidable_eq α] (a : α) (m : sym α n) :
Σ (i : fin (n + 1)), sym α (n - i)

Remove every a from a given sym α n. Yields the number of copies i and a term of sym α (n - i).

Equations
theorem sym.sigma_sub_ext {α : Type u_1} {n : } {m₁ m₂ : Σ (i : fin (n + 1)), sym α (n - i)} (h : (m₁.snd) = (m₂.snd)) :
m₁ = m₂
theorem sym.fill_filter_ne {α : Type u_1} {n : } [decidable_eq α] (a : α) (m : sym α n) :
m).fst m).snd = m
theorem sym.filter_ne_fill {α : Type u_1} {n : } [decidable_eq α] (a : α) (m : Σ (i : fin (n + 1)), sym α (n - i)) (h : a m.snd) :
(sym.fill a m.fst m.snd) = m

Combinatorial equivalences #

def sym_option_succ_equiv.encode {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n.succ) :
sym (option α) n sym α n.succ

Function from the symmetric product over option splitting on whether or not it contains a none.

Equations
@[simp]
theorem sym_option_succ_equiv.encode_of_none_mem {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n.succ) (h : option.none s) :
@[simp]
theorem sym_option_succ_equiv.encode_of_not_none_mem {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n.succ) (h : option.none s) :
= sum.inr (sym.map (λ (o : {x // x s}), s.attach)
@[simp]
def sym_option_succ_equiv.decode {α : Type u_1} {n : } :
sym (option α) n sym α n.succ sym (option α) n.succ

Inverse of sym_option_succ_equiv.decode.

Equations
@[simp]
theorem sym_option_succ_equiv.decode_encode {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n.succ) :
@[simp]
theorem sym_option_succ_equiv.encode_decode {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n sym α n.succ) :
@[simp]
theorem sym_option_succ_equiv_apply {α : Type u_1} {n : } [decidable_eq α] (s : sym (option α) n.succ) :
@[simp]
theorem sym_option_succ_equiv_symm_apply {α : Type u_1} {n : } [decidable_eq α] (ᾰ : sym (option α) n sym α n.succ) :
def sym_option_succ_equiv {α : Type u_1} {n : } [decidable_eq α] :
sym (option α) n.succ sym (option α) n sym α n.succ

The symmetric product over option is a disjoint union over simpler symmetric products.

Equations