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 u) (n : ) :
Type 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 : } (x : 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
@[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 : } (a : α) (s : 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
@[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} (h : a s) :
a 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} (h : a.val ~ b.val) :
def sym.sym' (α : Type u) (n : ) :
Type 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