Documentation

Mathlib.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_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.symEquivSym'.

Equations
  • Sym α n = { s // Multiset.card s = n }
def toMultiset {α : Type u_1} {n : } (s : Sym α n) :

The canoncial map to Multiset α that forgets that s has length n

Equations
  • s = s
instance Sym.hasCoe (α : Type u_1) (n : ) :
CoeOut (Sym α n) (Multiset α)
Equations
def Vector.Perm.isSetoid (α : Type u_1) (n : ) :
Setoid (Vector α n)

This is the List.Perm setoid lifted to Vector.

See note [reducible non-instances].

Equations
theorem Sym.coe_injective {α : Type u_1} {n : } :
@[simp]
theorem Sym.coe_inj {α : Type u_1} {n : } {s₁ : Sym α n} {s₂ : Sym α n} :
s₁ = s₂ s₁ = s₂
theorem Sym.ext {α : Type u_1} {n : } {s₁ : Sym α n} {s₂ : Sym α n} (h : s₁ = s₂) :
s₁ = s₂
@[simp]
theorem Sym.val_eq_coe {α : Type u_1} {n : } (s : Sym α n) :
s = s
@[match_pattern, inline]
abbrev Sym.mk {α : Type u_1} {n : } (m : Multiset α) (h : Multiset.card m = n) :
Sym α n

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

Equations
  • Sym.mk m h = { val := m, property := h }
@[match_pattern]
def Sym.nil {α : Type u_1} :
Sym α 0

The unique element in Sym α 0.

Equations
  • Sym.nil = { val := 0, property := (_ : Multiset.card 0 = 0) }
@[simp]
theorem Sym.coe_nil {α : Type u_1} :
Sym.nil = 0
@[match_pattern]
def Sym.cons {α : Type u_1} {n : } (a : α) (s : Sym α n) :
Sym α (Nat.succ n)

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

Equations

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 : Sym α n) (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
def Sym.ofVector {α : Type u_1} {n : } :
Vector α 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
  • Sym.ofVector x = { val := x, property := (_ : Multiset.card x = n) }
instance Sym.instCoeVectorSym {α : Type u_1} {n : } :
Coe (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} :
Sym.ofVector Vector.nil = Sym.nil
@[simp]
theorem Sym.of_vector_cons {α : Type u_1} {n : } (a : α) (v : Vector α n) :
instance Sym.instMembershipSym {α : Type u_1} {n : } :
Membership α (Sym α n)

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

Equations
  • Sym.instMembershipSym = { mem := fun a s => a s }
instance Sym.decidableMem {α : Type u_1} {n : } [inst : DecidableEq α] (a : α) (s : Sym α n) :
Equations
@[simp]
theorem Sym.mem_mk {α : Type u_1} {n : } (a : α) (s : Multiset α) (h : Multiset.card s = n) :
a Sym.mk s 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
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 : Vector α n) :
theorem Sym.sound {α : Type u_1} {n : } {a : Vector α n} {b : Vector α n} (h : a ~ b) :
def Sym.erase {α : Type u_1} {n : } [inst : DecidableEq α] (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 : } [inst : DecidableEq α] (m : Multiset α) (hc : Multiset.card m = n + 1) (a : α) (h : a m) :
Sym.erase (Sym.mk m hc) a h = Sym.mk (Multiset.erase m a) (_ : Multiset.card (Multiset.erase m a) = n)
@[simp]
theorem Sym.coe_erase {α : Type u_1} {n : } [inst : DecidableEq α] {s : Sym α (Nat.succ n)} {a : α} (h : a s) :
↑(Sym.erase s a h) = Multiset.erase (s) a
@[simp]
theorem Sym.cons_erase {α : Type u_1} {n : } [inst : DecidableEq α] {s : Sym α (Nat.succ n)} {a : α} (h : a s) :
a ::ₛ Sym.erase s a h = s
@[simp]
theorem Sym.erase_cons_head {α : Type u_1} {n : } [inst : DecidableEq α] (s : Sym α n) (a : α) (h : optParam (a a ::ₛ s) (_ : a a ::ₛ s)) :
Sym.erase (a ::ₛ s) 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
def Sym.cons' {α : Type u_1} {n : } :
αSym.Sym' α nSym.Sym' α (Nat.succ n)

This is cons but for the alternative Sym' definition.

Equations

This is cons but for the alternative Sym' definition.

Equations
def Sym.symEquivSym' {α : Type u_1} {n : } :
Sym α n Sym.Sym' α n

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

Equations
  • One or more equations did not get rendered due to their size.
theorem Sym.cons_equiv_eq_equiv_cons (α : Type u_1) (n : ) (a : α) (s : Sym α n) :
Sym.cons' a (Sym.symEquivSym' s) = Sym.symEquivSym' (a ::ₛ s)
instance Sym.instZeroSymOfNatNatInstOfNatNat {α : Type u_1} :
Zero (Sym α 0)
Equations
  • Sym.instZeroSymOfNatNatInstOfNatNat = { zero := { val := 0, property := (_ : Multiset.card 0 = Multiset.card 0) } }
Equations
  • Sym.instEmptyCollectionSymOfNatNatInstOfNatNat = { emptyCollection := 0 }
theorem Sym.eq_nil_of_card_zero {α : Type u_1} (s : Sym α 0) :
s = Sym.nil
instance Sym.uniqueZero {α : Type u_1} :
Unique (Sym α 0)
Equations
  • Sym.uniqueZero = { toInhabited := { default := Sym.nil }, uniq := (_ : ∀ (s : Sym α 0), s = Sym.nil) }
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 : } :
theorem Sym.coe_replicate {α : Type u_1} {n : } {a : α} :
@[simp]
theorem Sym.mem_replicate {α : Type u_1} {n : } {a : α} {b : α} :
b Sym.replicate n a n 0 b = a
theorem Sym.eq_replicate_iff {α : Type u_1} {n : } {s : Sym α n} {a : α} :
s = Sym.replicate n a ∀ (b : α), b sb = a
theorem Sym.exists_mem {α : Type u_1} {n : } (s : Sym α (Nat.succ n)) :
a, a s
theorem Sym.exists_eq_cons_of_succ {α : Type u_1} {n : } (s : Sym α (Nat.succ n)) :
a s', s = a ::ₛ s'
theorem Sym.eq_replicate {α : Type u_1} {a : α} {n : } {s : Sym α n} :
s = Sym.replicate n a ∀ (b : α), b sb = a
theorem Sym.eq_replicate_of_subsingleton {α : Type u_1} [inst : Subsingleton α] (a : α) {n : } (s : Sym α n) :
instance Sym.inhabitedSym {α : Type u_1} [inst : Inhabited α] (n : ) :
Inhabited (Sym α n)
Equations
instance Sym.inhabitedSym' {α : Type u_1} [inst : Inhabited α] (n : ) :
Equations
instance Sym.instUniqueSym {α : Type u_1} (n : ) [inst : Unique α] :
Unique (Sym α n)
Equations
theorem Sym.replicate_right_inj {α : Type u_1} {a : α} {b : α} {n : } (h : n 0) :
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→ 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 Sym.map f l a, a l f a = b
@[simp]
theorem Sym.map_id' {α : Type u_1} {n : } (s : Sym α n) :
Sym.map (fun 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) :
Sym.map id s = s
@[simp]
theorem Sym.map_map {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : } (g : βγ) (f : αβ) (s : Sym α n) :
Sym.map g (Sym.map f s) = Sym.map (g f) s
@[simp]
theorem Sym.map_zero {α : Type u_2} {β : Type u_1} (f : αβ) :
Sym.map f 0 = 0
@[simp]
theorem Sym.map_cons {α : Type u_1} {β : Type u_2} {n : } (f : αβ) (a : α) (s : Sym α n) :
Sym.map f (a ::ₛ s) = f a ::ₛ Sym.map f s
theorem Sym.map_congr {α : Type u_1} {β : Type u_2} {n : } {f : αβ} {g : αβ} {s : Sym α n} (h : ∀ (x : α), x sf x = g x) :
Sym.map f s = Sym.map g s
@[simp]
theorem Sym.map_mk {α : Type u_1} {β : Type u_2} {n : } {f : αβ} {m : Multiset α} {hc : Multiset.card m = n} :
Sym.map f (Sym.mk m hc) = Sym.mk (Multiset.map f m) (_ : Multiset.card (Multiset.map f m) = n)
@[simp]
theorem Sym.coe_map {α : Type u_1} {β : Type u_2} {n : } (s : Sym α n) (f : αβ) :
↑(Sym.map f s) = Multiset.map f s
theorem Sym.map_injective {α : Type u_1} {β : Type u_2} {f : αβ} (hf : Function.Injective f) (n : ) :
@[simp]
theorem Sym.equivCongr_symm_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : Sym β n) :
@[simp]
theorem Sym.equivCongr_apply {α : Type u_1} {β : Type u_2} {n : } (e : α β) (x : Sym α n) :
↑(Sym.equivCongr e) x = Sym.map (e) x
def Sym.equivCongr {α : 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
  • One or more equations did not get rendered due to their size.
def Sym.attach {α : Type u_1} {n : } (s : Sym α n) :
Sym { x // x s } n

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

Equations
@[simp]
theorem Sym.attach_mk {α : Type u_1} {n : } {m : Multiset α} {hc : Multiset.card m = n} :
Sym.attach (Sym.mk m hc) = Sym.mk (Multiset.attach m) (_ : Multiset.card (Multiset.attach m) = n)
@[simp]
theorem Sym.coe_attach {α : Type u_1} {n : } (s : Sym α n) :
theorem Sym.attach_map_coe {α : Type u_1} {n : } (s : Sym α n) :
Sym.map Subtype.val (Sym.attach s) = 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} :
Sym.attach Sym.nil = Sym.nil
@[simp]
theorem Sym.attach_cons {α : Type u_1} {n : } (x : α) (s : Sym α n) :
Sym.attach (x ::ₛ s) = { val := x, property := (_ : x x ::ₛ s) } ::ₛ Sym.map (fun x => { val := x, property := (_ : x x ::ₛ s) }) (Sym.attach s)
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
  • One or more equations did not get rendered due to their size.
@[simp]
theorem Sym.cast_rfl {α : Type u_1} {n : } {s : Sym α n} :
↑(Sym.cast (_ : n = n)) s = s
@[simp]
theorem Sym.cast_cast {α : Type u_1} {n : } {n' : } {s : Sym α n} {n'' : } (h : n = n') (h' : n' = n'') :
↑(Sym.cast h') (↑(Sym.cast h) s) = ↑(Sym.cast (_ : n = n'')) s
@[simp]
theorem Sym.coe_cast {α : Type u_1} {n : } {m : } {s : Sym α n} (h : n = m) :
↑(↑(Sym.cast h) s) = s
@[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
  • Sym.append s s' = { val := s + s', property := (_ : Multiset.card (s + s') = n + n') }
@[simp]
theorem Sym.append_inj_right {α : Type u_1} {n : } {n' : } (s : Sym α n) {t : Sym α n'} {t' : Sym α n'} :
Sym.append s t = Sym.append s t' t = t'
@[simp]
theorem Sym.append_inj_left {α : Type u_1} {n : } {n' : } {s : Sym α n} {s' : Sym α n} (t : Sym α n') :
Sym.append s t = Sym.append s' t s = s'
theorem Sym.append_comm {α : Type u_1} {n' : } (s : Sym α n') (s' : Sym α n') :
Sym.append s s' = ↑(Sym.cast (_ : n' + n' = n' + n')) (Sym.append s' s)
@[simp]
theorem Sym.coe_append {α : Type u_1} {n : } {n' : } (s : Sym α n) (s' : Sym α n') :
↑(Sym.append s s') = s + s'
theorem Sym.mem_append_iff {α : Type u_1} {n : } {m : } {s : Sym α n} {a : α} {s' : Sym α m} :
a Sym.append s 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 + ↑(Sym.replicate (i) a)
theorem Sym.mem_fill_iff {α : Type u_1} {n : } {a : α} {b : α} {i : Fin (n + 1)} {s : Sym α (n - i)} :
a Sym.fill b i s i 0 a = b a s
def Sym.filterNe {α : Type u_1} {n : } [inst : DecidableEq α] (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
  • One or more equations did not get rendered due to their size.
theorem Sym.sigma_sub_ext {α : Type u_1} {n : } {m₁ : (i : Fin (n + 1)) × Sym α (n - i)} {m₂ : (i : Fin (n + 1)) × Sym α (n - i)} (h : m₁.snd = m₂.snd) :
m₁ = m₂
theorem Sym.fill_filterNe {α : Type u_1} {n : } [inst : DecidableEq α] (a : α) (m : Sym α n) :
Sym.fill a (Sym.filterNe a m).fst (Sym.filterNe a m).snd = m
theorem Sym.filter_ne_fill {α : Type u_1} {n : } [inst : DecidableEq α] (a : α) (m : (i : Fin (n + 1)) × Sym α (n - i)) (h : ¬a m.snd) :
Sym.filterNe a (Sym.fill a m.fst m.snd) = m

Combinatorial equivalences #

def SymOptionSuccEquiv.encode {α : Type u_1} {n : } [inst : DecidableEq α] (s : Sym (Option α) (Nat.succ n)) :
Sym (Option α) n Sym α (Nat.succ n)

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

Equations
@[simp]
theorem SymOptionSuccEquiv.encode_of_none_mem {α : Type u_1} {n : } [inst : DecidableEq α] (s : Sym (Option α) (Nat.succ n)) (h : none s) :
@[simp]
theorem SymOptionSuccEquiv.encode_of_not_none_mem {α : Type u_1} {n : } [inst : DecidableEq α] (s : Sym (Option α) (Nat.succ n)) (h : ¬none s) :
def SymOptionSuccEquiv.decode {α : Type u_1} {n : } :
Sym (Option α) n Sym α (Nat.succ n)Sym (Option α) (Nat.succ n)

Inverse of Sym_option_succ_equiv.decode.

Equations
@[simp]
theorem SymOptionSuccEquiv.decode_inl {α : Type u_1} {n : } (s : Sym (Option α) n) :
@[simp]
theorem SymOptionSuccEquiv.decode_inr {α : Type u_1} {n : } (s : Sym α (Nat.succ n)) :
SymOptionSuccEquiv.decode (Sum.inr s) = Sym.map (Function.Embedding.some) s
def symOptionSuccEquiv {α : Type u_1} {n : } [inst : DecidableEq α] :
Sym (Option α) (Nat.succ n) Sym (Option α) n Sym α (Nat.succ n)

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

Equations
  • One or more equations did not get rendered due to their size.