mathlib3 documentation

data.sym.basic

Symmetric powers #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.sym_equiv_sym'.

Equations

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

Instances for sym

@[protected, instance]

def sym.has_coe (α : Type u_1) (n : ℕ) :

has_coe (sym α n) (multiset α)

Equations

sym.has_coe α n = coe_subtype

@[reducible]

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

setoid (vector α n)

This is the list.perm setoid lifted to vector.

See note [reducible non-instances].

Equations

vector.perm.is_setoid α n = setoid.comap subtype.val (list.is_setoid α)

theorem sym.coe_injective {α : Type u_1} {n : ℕ} :

function.injective coe

@[simp, norm_cast]

theorem sym.coe_inj {α : Type u_1} {n : ℕ} {s₁ s₂ : sym α n} :

↑s₁ = ↑s₂ ↔ s₁ = s₂

@[simp]

theorem sym.mk_coe {α : Type u_1} {n : ℕ} (m : multiset α) (h : ⇑multiset.card m = n) :

↑(sym.mk m h) = m

@[reducible]

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

def sym.nil {α : Type u_1} :

sym α 0

The unique element in sym α 0.

Equations

sym.nil = ⟨0, _⟩

@[simp]

theorem sym.coe_nil {α : Type u_1} :

def sym.cons {α : Type u_1} {n : ℕ} (a : α) (s : sym α n) :

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

Equations

a ::ₛ s = ⟨a ::ₘ s.val, _⟩

@[simp]

theorem sym.cons_inj_right {α : Type u_1} {n : ℕ} (a : α) (s 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

@[protected, instance]

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

has_lift (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.has_lift = {lift := λ (x : vector α n), ⟨↑(x.val), _⟩}

@[simp]

theorem sym.of_vector_nil {α : Type u_1} :

↑vector.nil = sym.nil

@[simp]

theorem sym.of_vector_cons {α : Type u_1} {n : ℕ} (a : α) (v : vector α n) :

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

@[protected, instance]

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

has_mem α (sym α n)

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

Equations

sym.has_mem = {mem := λ (a : α) (s : sym α n), a ∈ s.val}

@[protected, instance]

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

decidable (a ∈ s)

Equations

sym.decidable_mem a s = multiset.decidable_mem a s.val

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

@[simp]

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) :

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

theorem sym.sound {α : Type u_1} {n : ℕ} {a b : vector α n} (h : a.val ~ b.val) :

def sym.erase {α : Type u_1} {n : ℕ} [decidable_eq α] (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

s.erase a h = ⟨s.val.erase a, _⟩

@[simp]

theorem sym.erase_mk {α : Type u_1} {n : ℕ} [decidable_eq α] (m : multiset α) (hc : ⇑multiset.card m = n + 1) (a : α) (h : a ∈ m) :

(sym.mk m hc).erase a h = sym.mk (m.erase a) _

@[simp]

theorem sym.coe_erase {α : Type u_1} {n : ℕ} [decidable_eq α] {s : sym α n.succ} {a : α} (h : a ∈ s) :

↑(s.erase a h) = ↑s.erase a

@[simp]

theorem sym.cons_erase {α : Type u_1} {n : ℕ} [decidable_eq α] {s : sym α n.succ} {a : α} (h : a ∈ s) :

a ::ₛ s.erase a h = s

@[simp]

theorem sym.erase_cons_head {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym α n) (a : α) (h : a ∈ a ::ₛ s := _) :

(a ::ₛ s).erase 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

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

Instances for sym.sym'

def sym.cons' {α : Type u_1} {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_1} {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_1) (n : ℕ) (a : α) (s : sym α n) :

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

@[protected, instance]

def sym.has_zero {α : Type u_1} :

has_zero (sym α 0)

Equations

sym.has_zero = {zero := ⟨0, _⟩}

@[protected, instance]

def sym.has_emptyc {α : Type u_1} :

has_emptyc (sym α 0)

Equations

sym.has_emptyc = {emptyc := 0}

theorem sym.eq_nil_of_card_zero {α : Type u_1} (s : sym α 0) :

@[protected, instance]

def sym.unique_zero {α : Type u_1} :

unique (sym α 0)

Equations

sym.unique_zero = {to_inhabited := {default := sym.nil α}, uniq := _}

def sym.replicate {α : Type u_1} (n : ℕ) (a : α) :

sym α n

replicate n a is the sym containing only a with multiplicity n.

Equations

sym.replicate n a = ⟨multiset.replicate n a, _⟩

theorem sym.replicate_succ {α : Type u_1} {a : α} {n : ℕ} :

sym.replicate n.succ a = a ::ₛ sym.replicate n a

theorem sym.coe_replicate {α : Type u_1} {n : ℕ} {a : α} :

↑(sym.replicate n a) = multiset.replicate 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 ∈ s → b = a

theorem sym.exists_mem {α : Type u_1} {n : ℕ} (s : sym α n.succ) :

∃ (a : α), a ∈ s

theorem sym.exists_eq_cons_of_succ {α : Type u_1} {n : ℕ} (s : sym α n.succ) :

∃ (a : α) (s' : sym α n), s = a ::ₛ s'

theorem sym.eq_replicate {α : Type u_1} {a : α} {n : ℕ} {s : sym α n} :

s = sym.replicate n a ↔ ∀ (b : α), b ∈ s → b = a

theorem sym.eq_replicate_of_subsingleton {α : Type u_1} [subsingleton α] (a : α) {n : ℕ} (s : sym α n) :

s = sym.replicate n a

@[protected, instance]

def sym.subsingleton {α : Type u_1} [subsingleton α] (n : ℕ) :

subsingleton (sym α n)

@[protected, instance]

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

inhabited (sym α n)

Equations

sym.inhabited_sym n = {default := sym.replicate n inhabited.default}

@[protected, instance]

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

inhabited (sym.sym' α n)

Equations

sym.inhabited_sym' n = {default := quotient.mk' (vector.replicate n inhabited.default)}

@[protected, instance]

def sym.is_empty {α : Type u_1} (n : ℕ) [is_empty α] :

is_empty (sym α n.succ)

@[protected, instance]

def sym.unique {α : Type u_1} (n : ℕ) [unique α] :

unique (sym α n)

Equations

sym.unique n = unique.mk' (sym α n)

theorem sym.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) :

sym.replicate n a = sym.replicate n b ↔ a = b

theorem sym.replicate_right_injective {α : Type u_1} {n : ℕ} (h : n ≠ 0) :

function.injective (sym.replicate n)

@[protected, instance]

def sym.nontrivial {α : Type u_1} (n : ℕ) [nontrivial α] :

nontrivial (sym α (n + 1))

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 by applying it to every element of the underlying n-tuple.

Equations

sym.map f x = ⟨multiset.map f x.val, _⟩

@[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 (λ (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_1} {β : Type u_2} (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 ∈ s → f 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) _

@[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 : ℕ) :

function.injective (sym.map f)

def sym.equiv_congr {α : 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

sym.equiv_congr e = {to_fun := sym.map ⇑e, inv_fun := sym.map ⇑(e.symm), left_inv := _, right_inv := _}

@[simp]

theorem sym.equiv_congr_apply {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : sym α n) :

⇑(sym.equiv_congr e) x = sym.map ⇑e x

@[simp]

theorem sym.equiv_congr_symm_apply {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : sym β n) :

⇑((sym.equiv_congr e).symm) x = sym.map ⇑(e.symm) x

def sym.attach {α : Type u_1} {n : ℕ} (s : sym α n) :

sym {x // x ∈ s} n

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

Equations

s.attach = ⟨s.val.attach, _⟩

@[simp]

theorem sym.attach_mk {α : Type u_1} {n : ℕ} {m : multiset α} {hc : ⇑multiset.card m = n} :

(sym.mk m hc).attach = sym.mk m.attach _

@[simp]

theorem sym.coe_attach {α : Type u_1} {n : ℕ} (s : sym α n) :

↑(s.attach) = ↑s.attach

theorem sym.attach_map_coe {α : Type u_1} {n : ℕ} (s : sym α n) :

sym.map coe s.attach = 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.nil.attach = sym.nil

@[simp]

theorem sym.attach_cons {α : Type u_1} {n : ℕ} (x : α) (s : sym α n) :

(x ::ₛ s).attach = ⟨x, _⟩ ::ₛ sym.map (λ (x_1 : {x // x ∈ s}), ⟨↑x_1, _⟩) s.attach

@[protected]

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

sym.cast h = {to_fun := λ (s : sym α n), ⟨s.val, _⟩, inv_fun := λ (s : sym α m), ⟨s.val, _⟩, left_inv := _, right_inv := _}

@[simp]

theorem sym.cast_rfl {α : Type u_1} {n : ℕ} {s : sym α n} :

⇑(sym.cast rfl) 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 _) 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

s.append s' = ⟨s.val + s'.val, _⟩

@[simp]

theorem sym.append_inj_right {α : Type u_1} {n n' : ℕ} (s : sym α n) {t t' : sym α n'} :

s.append t = s.append t' ↔ t = t'

@[simp]

theorem sym.append_inj_left {α : Type u_1} {n n' : ℕ} {s s' : sym α n} (t : sym α n') :

s.append t = s'.append t ↔ s = s'

theorem sym.append_comm {α : Type u_1} {n' : ℕ} (s s' : sym α n') :

s.append s' = ⇑(sym.cast _) (s'.append s)

@[simp, norm_cast]

theorem sym.coe_append {α : Type u_1} {n n' : ℕ} (s : sym α n) (s' : sym α n') :

↑(s.append s') = ↑s + ↑s'

theorem sym.mem_append_iff {α : Type u_1} {n m : ℕ} {s : sym α n} {a : α} {s' : sym α m} :

a ∈ s.append 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

sym.fill a i m = ⇑(sym.cast _) (m.append (sym.replicate ↑i a))

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.filter_ne {α : Type u_1} {n : ℕ} [decidable_eq α] (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

sym.filter_ne a m = ⟨⟨multiset.count a m.val, _⟩, ⟨multiset.filter (ne a) m.val, _⟩⟩

theorem sym.sigma_sub_ext {α : Type u_1} {n : ℕ} {m₁ m₂ : Σ (i : fin (n + 1)), sym α (n - ↑i)} (h : ↑(m₁.snd) = ↑(m₂.snd)) :

m₁ = m₂

theorem sym.fill_filter_ne {α : Type u_1} {n : ℕ} [decidable_eq α] (a : α) (m : sym α n) :

sym.fill a (sym.filter_ne a m).fst (sym.filter_ne a m).snd = m

theorem sym.filter_ne_fill {α : Type u_1} {n : ℕ} [decidable_eq α] (a : α) (m : Σ (i : fin (n + 1)), sym α (n - ↑i)) (h : a ∉ m.snd) :

sym.filter_ne a (sym.fill a m.fst m.snd) = m

Combinatorial equivalences #

def sym_option_succ_equiv.encode {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n.succ) :

sym (option α) n ⊕ sym α n.succ

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

Equations

sym_option_succ_equiv.encode s = dite (option.none ∈ s) (λ (h : option.none ∈ s), sum.inl (s.erase option.none h)) (λ (h : option.none ∉ s), sum.inr (sym.map (λ (o : {x // x ∈ s}), option.get _) s.attach))

@[simp]

theorem sym_option_succ_equiv.encode_of_none_mem {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n.succ) (h : option.none ∈ s) :

sym_option_succ_equiv.encode s = sum.inl (s.erase option.none h)

@[simp]

theorem sym_option_succ_equiv.encode_of_not_none_mem {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n.succ) (h : option.none ∉ s) :

sym_option_succ_equiv.encode s = sum.inr (sym.map (λ (o : {x // x ∈ s}), option.get _) s.attach)

@[simp]

def sym_option_succ_equiv.decode {α : Type u_1} {n : ℕ} :

sym (option α) n ⊕ sym α n.succ → sym (option α) n.succ

Inverse of sym_option_succ_equiv.decode.

Equations

@[simp]

theorem sym_option_succ_equiv.decode_encode {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n.succ) :

sym_option_succ_equiv.decode (sym_option_succ_equiv.encode s) = s

@[simp]

theorem sym_option_succ_equiv.encode_decode {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n ⊕ sym α n.succ) :

sym_option_succ_equiv.encode (sym_option_succ_equiv.decode s) = s

@[simp]

theorem sym_option_succ_equiv_apply {α : Type u_1} {n : ℕ} [decidable_eq α] (s : sym (option α) n.succ) :

⇑sym_option_succ_equiv s = sym_option_succ_equiv.encode s

@[simp]

theorem sym_option_succ_equiv_symm_apply {α : Type u_1} {n : ℕ} [decidable_eq α] (ᾰ : sym (option α) n ⊕ sym α n.succ) :

⇑(sym_option_succ_equiv.symm) ᾰ = sym_option_succ_equiv.decode ᾰ

def sym_option_succ_equiv {α : Type u_1} {n : ℕ} [decidable_eq α] :

sym (option α) n.succ ≃ sym (option α) n ⊕ sym α n.succ

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

Equations

sym_option_succ_equiv = {to_fun := sym_option_succ_equiv.encode (λ (a b : α), _inst_1 a b), inv_fun := sym_option_succ_equiv.decode n, left_inv := _, right_inv := _}