mathlib documentation

data.sym.basic

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

TODO: This was created as supporting material for 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

sym α n = {s // ⇑multiset.card s = n}

def vector.perm.is_setoid (α : Type u) (n : ℕ) :

setoid (vector α n)

This is the list.perm setoid lifted to vector.

See note [reducible non-instances].

Equations

vector.perm.is_setoid α n = {r := λ (a b : vector α n), a.val ~ b.val, iseqv := _}

def sym.of_vector {α : Type u} {n : ℕ} (x : 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

sym.of_vector x = ⟨↑(x.val), _⟩

@[protected, instance]

def sym.has_lift {α : Type u} {n : ℕ} :

has_lift (vector α n) (sym α n)

Equations

sym.has_lift = {lift := sym.of_vector n}

def sym.nil {α : Type u} :

sym α 0

The unique element in sym α 0.

Equations

sym.nil = ⟨0, _⟩

def sym.cons {α : Type u} {n : ℕ} :

α → sym α n → sym α n.succ

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

Equations

a::⟨s, h⟩ = ⟨a ::ₘ s, _⟩

@[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

sym.mem a s = (a ∈ s.val)

@[protected, instance]

def sym.has_mem {α : Type u} {n : ℕ} :

has_mem α (sym α n)

Equations

sym.has_mem = {mem := sym.mem n}

@[protected, instance]

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

decidable (a ∈ s)

Equations

sym.decidable_mem a s = subtype.cases_on s (λ (s_val : multiset α) (s_property : ⇑multiset.card s_val = n), id (multiset.decidable_mem a 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} (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 : vector α n) :

a::↑v = ↑(a::ᵥv)

theorem sym.sound {α : Type u} {n : ℕ} {a b : vector α 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

sym.sym' α n = quotient (vector.perm.is_setoid α n)

def sym.cons' {α : Type u} {n : ℕ} :

α → sym.sym' α n → sym.sym' α n.succ

This is cons but for the alternative sym' definition.

Equations

sym.cons' = λ (a : α), quotient.map (vector.cons a) _

def sym.sym_equiv_sym' {α : Type u} {n : ℕ} :

sym α n ≃ sym.sym' α n

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

Equations

sym.sym_equiv_sym' = equiv.subtype_quotient_equiv_quotient_subtype (λ (l : list α), l.length = n) (λ (s : multiset α), ⇑multiset.card s = n) sym.sym_equiv_sym'._proof_1 sym.sym_equiv_sym'._proof_2

theorem sym.cons_equiv_eq_equiv_cons (α : Type u) (n : ℕ) (a : α) (s : sym α n) :

a::⇑sym.sym_equiv_sym' s = ⇑sym.sym_equiv_sym' (a::s)

@[protected, instance]

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

inhabited (sym α n)

Equations

sym.inhabited_sym n = {default := ⟨multiset.repeat (default α) n, _⟩}

@[protected, instance]

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

inhabited (sym.sym' α n)

Equations

sym.inhabited_sym' n = {default := quotient.mk' (vector.repeat (default α) n)}