data.sym

# Symmetric powers

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

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

## Tags

symmetric powers

def sym  :
Type uType u

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
def vector.perm.is_setoid (α : Type u) (n : ) :
setoid (vector α n)

This is the list.perm setoid lifted to vector.

Equations
def sym.of_vector {α : Type u} {n : } :
nsym α n

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

Equations
@[instance]
def sym.has_lift {α : Type u} {n : } :
has_lift (vector α n) (sym α n)

Equations
def sym.nil {α : Type u} :
sym α 0

The unique element in sym α 0.

Equations
def sym.cons {α : Type u} {n : } :
α → sym α nsym α 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} {n : } (a : α) (s s' : sym α n) :
a :: s = a :: s' s = s'

@[simp]
theorem sym.cons_inj_left {α : Type u} {n : } (a a' : α) (s : sym α n) :
a :: s = a' :: s a = a'

theorem sym.cons_swap {α : Type u} {n : } (a b : α) (s : sym α n) :
a :: b :: s = b :: a :: s

def sym.mem {α : Type u} {n : } :
α → sym α n → Prop

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

Equations
@[instance]
def sym.has_mem {α : Type u} {n : } :
(sym α n)

Equations
@[instance]
def sym.decidable_mem {α : Type u} {n : } [decidable_eq α] (a : α) (s : sym α n) :

Equations
• = subtype.cases_on s (λ (s_val : multiset α) (s_property : s_val.card = n), id s_val))
@[simp]
theorem sym.mem_cons {α : Type u} {n : } {a b : α} {s : sym α n} :
a b :: s a = b a s

theorem sym.mem_cons_of_mem {α : Type u} {n : } {a b : α} {s : sym α n} :
a sa b :: s

@[simp]
theorem sym.mem_cons_self {α : Type u} {n : } (a : α) (s : sym α n) :
a a :: s

theorem sym.cons_of_coe_eq {α : Type u} {n : } (a : α) (v : n) :
a :: v = (a::ᵥv)

theorem sym.sound {α : Type u} {n : } {a b : n} :
a.val ~ b.vala = b

def sym.sym'  :
Type uType u

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

Equations
• n =
def sym.cons' {α : Type u} {n : } :
α → n n.succ

This is cons but for the alternative sym' definition.

Equations
def sym.sym_equiv_sym' {α : Type u} {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) (n : ) (a : α) (s : sym α n) :

@[instance]
def sym.inhabited_sym {α : Type u} [inhabited α] (n : ) :
inhabited (sym α n)

Equations
@[instance]
def sym.inhabited_sym' {α : Type u} [inhabited α] (n : ) :

Equations