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
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'.
Multisets of cardinality n are equivalent to length-n vectors up to permutations.
Equations
- sym.sym_equiv_sym' α n = equiv.subtype_quotient_equiv_quotient_subtype (λ (l : list α), l.length = n) (λ (s : multiset α), s.card = n) _ _
@[instance]
Equations
- sym.inhabited_sym α n = {default := ⟨multiset.repeat (inhabited.default α) n, _⟩}
@[instance]
Equations
- sym.inhabited_sym' α n = {default := quotient.mk' (vector.repeat (inhabited.default α) n)}