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

def Sym.toMultiset {α : Type u_1} {n : ℕ} (s : Sym α n) : Multiset α

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

instance Sym.hasCoe (α : Type u_1) (n : ℕ) : CoeOut (Sym α n) (Multiset α)

instance instDecidableEqSym {α : Type u_1} {n : ℕ} [DecidableEq α] : DecidableEq (Sym α n)

@[reducible, inline]

abbrev List.Vector.Perm.isSetoid (α : Type u_1) (n : ℕ) : Setoid (Vector α n)

This is the List.Perm setoid lifted to Vector.

See note [reducible non-instances].

instance instDecidableRelVectorEquivOfDecidableEq {α : Type u_1} {n : ℕ} [DecidableEq α] : DecidableRel fun (x1 x2 : List.Vector α n) => x1 ≈ x2

theorem Sym.coe_injective {α : Type u_1} {n : ℕ} : Function.Injective toMultiset

@[simp]

theorem Sym.coe_inj {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n} : ↑s₁ = ↑s₂ ↔ s₁ = s₂

theorem Sym.ext {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n} (h : ↑s₁ = ↑s₂) : s₁ = s₂

theorem Sym.ext_iff {α : Type u_1} {n : ℕ} {s₁ s₂ : Sym α n} : s₁ = s₂ ↔ ↑s₁ = ↑s₂

@[simp]

theorem Sym.val_eq_coe {α : Type u_1} {n : ℕ} (s : Sym α n) : ↑s = ↑s

@[reducible, match_pattern, inline]

abbrev Sym.mk {α : Type u_1} {n : ℕ} (m : Multiset α) (h : m.card = n) : Sym α n

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

@[match_pattern]

def Sym.nil {α : Type u_1} : Sym α 0

The unique element in Sym α 0.

@[simp]

theorem Sym.coe_nil {α : Type u_1} : ↑nil = 0

@[match_pattern]

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

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

def Sym.«term_::ₛ_» : Lean.TrailingParserDescr

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

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

def Sym.ofVector {α : Type u_1} {n : ℕ} : List.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.

instance Sym.instCoeVector {α : Type u_1} {n : ℕ} : Coe (List.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.

@[simp]

theorem Sym.ofVector_nil {α : Type u_1} : ofVector List.Vector.nil = nil

@[simp]

theorem Sym.ofVector_cons {α : Type u_1} {n : ℕ} (a : α) (v : List.Vector α n) : ofVector (a ::ᵥ v) = a ::ₛ ofVector v

@[simp]

theorem Sym.card_coe {α : Type u_1} {n : ℕ} {s : Sym α n} : (↑s).card = n

instance Sym.instMembership {α : Type u_1} {n : ℕ} : Membership α (Sym α n)

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

instance Sym.decidableMem {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (s : Sym α n) : Decidable (a ∈ s)

@[simp]

theorem Sym.coe_mk {α : Type u_1} {n : ℕ} (s : Multiset α) (h : s.card = n) : ↑(mk s h) = s

@[simp]

theorem Sym.mem_mk {α : Type u_1} {n : ℕ} (a : α) (s : Multiset α) (h : s.card = n) : a ∈ mk s h ↔ a ∈ s

theorem Sym.forall {α : Type u_1} {n : ℕ} {p : Sym α n → Prop} : (∀ (s : Sym α n), p s) ↔ ∀ (s : Multiset α) (hs : s.card = n), p (mk s hs)

theorem Sym.exists {α : Type u_1} {n : ℕ} {p : Sym α n → Prop} : (∃ (s : Sym α n), p s) ↔ ∃ (s : Multiset α) (hs : s.card = n), p (mk s hs)

@[simp]

theorem Sym.notMem_nil {α : Type u_1} (a : α) : a ∉ nil

@[deprecated Sym.notMem_nil (since := "2025-05-23")]

theorem Sym.not_mem_nil {α : Type u_1} (a : α) : a ∉ nil

Alias of Sym.notMem_nil.

@[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 : List.Vector α n) : a ::ₛ ofVector v = ofVector (a ::ᵥ v)

theorem Sym.sound {α : Type u_1} {n : ℕ} {a b : List.Vector α n} (h : (↑a).Perm ↑b) : ofVector a = ofVector b

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

@[simp]

theorem Sym.erase_mk {α : Type u_1} {n : ℕ} [DecidableEq α] (m : Multiset α) (hc : m.card = n + 1) (a : α) (h : a ∈ m) : (mk m hc).erase a h = mk (m.erase a) ⋯

@[simp]

theorem Sym.coe_erase {α : Type u_1} {n : ℕ} [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) : ↑(s.erase a h) = (↑s).erase a

@[simp]

theorem Sym.cons_erase {α : Type u_1} {n : ℕ} [DecidableEq α] {s : Sym α n.succ} {a : α} (h : a ∈ s) : a ::ₛ s.erase a h = s

@[simp]

theorem Sym.erase_cons_head {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym α n) (a : α) (h : a ∈ a ::ₛ s := ⋯) : (a ::ₛ s).erase a h = s

def Sym.Sym' (α : Type u_3) (n : ℕ) : Type u_3

Another definition of the nth symmetric power, using vectors modulo permutations. (See Sym.)

def Sym.cons' {α : Type u_3} {n : ℕ} : α → Sym' α n → Sym' α n.succ

This is cons but for the alternative Sym' definition.

def Sym.«term_::_» : Lean.TrailingParserDescr

This is cons but for the alternative Sym' definition.

def Sym.symEquivSym' {α : Type u_3} {n : ℕ} : Sym α n ≃ Sym' α n

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

theorem Sym.cons_equiv_eq_equiv_cons (α : Type u_3) (n : ℕ) (a : α) (s : Sym α n) : cons' a (symEquivSym' s) = symEquivSym' (a ::ₛ s)

instance Sym.instZeroSym {α : Type u_1} : Zero (Sym α 0)

@[simp]

theorem Sym.toMultiset_zero {α : Type u_1} : ↑0 = 0

instance Sym.instEmptyCollectionOfNatNat {α : Type u_1} : EmptyCollection (Sym α 0)

theorem Sym.eq_nil_of_card_zero {α : Type u_1} (s : Sym α 0) : s = nil

instance Sym.uniqueZero {α : Type u_1} : Unique (Sym α 0)

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

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

theorem Sym.replicate_succ {α : Type u_1} {a : α} {n : ℕ} : replicate n.succ a = a ::ₛ replicate n a

theorem Sym.coe_replicate {α : Type u_1} {n : ℕ} {a : α} : ↑(replicate n a) = Multiset.replicate n a

theorem Sym.val_replicate {α : Type u_1} {n : ℕ} {a : α} : ↑(replicate n a) = Multiset.replicate n a

@[simp]

theorem Sym.mem_replicate {α : Type u_1} {n : ℕ} {a b : α} : b ∈ replicate n a ↔ n ≠ 0 ∧ b = a

theorem Sym.eq_replicate_iff {α : Type u_1} {n : ℕ} {s : Sym α n} {a : α} : s = replicate n a ↔ ∀ b ∈ s, b = a

theorem Sym.exists_mem {α : Type u_1} {n : ℕ} (s : Sym α n.succ) : ∃ (a : α), a ∈ s

theorem Sym.exists_cons_of_mem {α : Type u_1} {n : ℕ} {s : Sym α (n + 1)} {a : α} (h : a ∈ s) : ∃ (t : Sym α n), s = a ::ₛ t

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 = replicate n a ↔ ∀ b ∈ s, b = a

theorem Sym.eq_replicate_of_subsingleton {α : Type u_1} [Subsingleton α] (a : α) {n : ℕ} (s : Sym α n) : s = replicate n a

instance Sym.instSubsingleton {α : Type u_1} [Subsingleton α] (n : ℕ) : Subsingleton (Sym α n)

instance Sym.inhabitedSym {α : Type u_1} [Inhabited α] (n : ℕ) : Inhabited (Sym α n)

instance Sym.inhabitedSym' {α : Type u_1} [Inhabited α] (n : ℕ) : Inhabited (Sym' α n)

instance Sym.instIsEmptySucc {α : Type u_1} (n : ℕ) [IsEmpty α] : IsEmpty (Sym α n.succ)

instance Sym.instUnique {α : Type u_1} (n : ℕ) [Unique α] : Unique (Sym α n)

theorem Sym.replicate_right_inj {α : Type u_1} {a b : α} {n : ℕ} (h : n ≠ 0) : replicate n a = replicate n b ↔ a = b

theorem Sym.replicate_right_injective {α : Type u_1} {n : ℕ} (h : n ≠ 0) : Function.Injective (replicate n)

instance Sym.instNontrivialHAddNatOfNat {α : 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.

@[simp]

theorem Sym.mem_map {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {b : β} {l : Sym α n} : b ∈ map f l ↔ ∃ a ∈ l, f a = b

@[simp]

theorem Sym.map_id' {α : Type u_3} {n : ℕ} (s : Sym α n) : 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_3} {n : ℕ} (s : Sym α n) : map id s = s

@[simp]

theorem Sym.map_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} {n : ℕ} (g : β → γ) (f : α → β) (s : Sym α n) : map g (map f s) = map (g ∘ f) s

@[simp]

theorem Sym.map_zero {α : Type u_1} {β : Type u_2} (f : α → β) : map f 0 = 0

@[simp]

theorem Sym.map_cons {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : α) (s : Sym α n) : map f (a ::ₛ s) = f a ::ₛ map f s

theorem Sym.map_congr {α : Type u_1} {β : Type u_2} {n : ℕ} {f g : α → β} {s : Sym α n} (h : ∀ x ∈ s, f x = g x) : map f s = map g s

@[simp]

theorem Sym.map_mk {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → β} {m : Multiset α} {hc : m.card = n} : map f (mk m hc) = mk (Multiset.map f m) ⋯

@[simp]

theorem Sym.coe_map {α : Type u_1} {β : Type u_2} {n : ℕ} (s : Sym α n) (f : α → β) : ↑(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 (map f)

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.

@[simp]

theorem Sym.equivCongr_symm_apply {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : Sym β n) : (equivCongr e).symm x = map (⇑e.symm) x

@[simp]

theorem Sym.equivCongr_apply {α : Type u_1} {β : Type u_2} {n : ℕ} (e : α ≃ β) (x : Sym α n) : (equivCongr e) x = map (⇑e) 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}.

@[simp]

theorem Sym.attach_mk {α : Type u_1} {n : ℕ} {m : Multiset α} {hc : m.card = n} : (mk m hc).attach = 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) : map Subtype.val s.attach = s

@[simp]

theorem Sym.mem_attach {α : Type u_1} {n : ℕ} (s : Sym α n) (x : { x : α // x ∈ s }) : x ∈ s.attach

@[simp]

theorem Sym.attach_nil {α : Type u_1} : nil.attach = nil

@[simp]

theorem Sym.attach_cons {α : Type u_1} {n : ℕ} (x : α) (s : Sym α n) : (x ::ₛ s).attach = ⟨x, ⋯⟩ ::ₛ map (fun (x_1 : { x : α // x ∈ s }) => ⟨↑x_1, ⋯⟩) s.attach

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.

@[simp]

theorem Sym.cast_rfl {α : Type u_1} {n : ℕ} {s : Sym α n} : (Sym.cast ⋯) 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.

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

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.oneEquiv {α : Type u_1} : α ≃ Sym α 1

a ↦ {a} as an equivalence between α and Sym α 1.

@[simp]

theorem Sym.oneEquiv_apply {α : Type u_1} (a : α) : oneEquiv a = ⟨{a}, ⋯⟩

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.

theorem Sym.coe_fill {α : Type u_1} {n : ℕ} {a : α} {i : Fin (n + 1)} {m : Sym α (n - ↑i)} : ↑(fill a i m) = ↑m + ↑(replicate (↑i) a)

theorem Sym.mem_fill_iff {α : Type u_1} {n : ℕ} {a b : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)} : a ∈ fill b i s ↔ ↑i ≠ 0 ∧ a = b ∨ a ∈ s

def Sym.filterNe {α : Type u_1} {n : ℕ} [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).

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_filterNe {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (m : Sym α n) : fill a (filterNe a m).fst (filterNe a m).snd = m

theorem Sym.filter_ne_fill {α : Type u_1} {n : ℕ} [DecidableEq α] (a : α) (m : (i : Fin (n + 1)) × Sym α (n - ↑i)) (h : a ∉ m.snd) : filterNe a (fill a m.fst m.snd) = m

theorem Sym.count_coe_fill_self_of_notMem {α : Type u_1} {n : ℕ} [DecidableEq α] {a : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)} (hx : a ∉ s) : Multiset.count a ↑(fill a i s) = ↑i

@[deprecated Sym.count_coe_fill_self_of_notMem (since := "2025-05-23")]

theorem Sym.count_coe_fill_self_of_not_mem {α : Type u_1} {n : ℕ} [DecidableEq α] {a : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)} (hx : a ∉ s) : Multiset.count a ↑(fill a i s) = ↑i

Alias of Sym.count_coe_fill_self_of_notMem.

theorem Sym.count_coe_fill_of_ne {α : Type u_1} {n : ℕ} [DecidableEq α] {a x : α} {i : Fin (n + 1)} {s : Sym α (n - ↑i)} (hx : x ≠ a) : Multiset.count x ↑(fill a i s) = Multiset.count x ↑s

Combinatorial equivalences

def SymOptionSuccEquiv.encode {α : Type u_1} {n : ℕ} [DecidableEq α] (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.

@[simp]

theorem SymOptionSuccEquiv.encode_of_none_mem {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∈ s) : encode s = Sum.inl (s.erase none h)

@[simp]

theorem SymOptionSuccEquiv.encode_of_none_notMem {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∉ s) : encode s = Sum.inr (Sym.map (fun (o : { x : Option α // x ∈ s }) => (↑o).get ⋯) s.attach)

@[deprecated SymOptionSuccEquiv.encode_of_none_notMem (since := "2025-05-23")]

theorem SymOptionSuccEquiv.encode_of_not_none_mem {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym (Option α) n.succ) (h : none ∉ s) : encode s = Sum.inr (Sym.map (fun (o : { x : Option α // x ∈ s }) => (↑o).get ⋯) s.attach)

Alias of SymOptionSuccEquiv.encode_of_none_notMem.

def SymOptionSuccEquiv.decode {α : Type u_1} {n : ℕ} : Sym (Option α) n ⊕ Sym α n.succ → Sym (Option α) n.succ

Inverse of Sym_option_succ_equiv.decode.

@[simp]

theorem SymOptionSuccEquiv.decode_inl {α : Type u_1} {n : ℕ} (s : Sym (Option α) n) : decode (Sum.inl s) = none ::ₛ s

@[simp]

theorem SymOptionSuccEquiv.decode_inr {α : Type u_1} {n : ℕ} (s : Sym α n.succ) : decode (Sum.inr s) = Sym.map (⇑Function.Embedding.some) s

@[simp]

theorem SymOptionSuccEquiv.decode_encode {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym (Option α) n.succ) : decode (encode s) = s

@[simp]

theorem SymOptionSuccEquiv.encode_decode {α : Type u_1} {n : ℕ} [DecidableEq α] (s : Sym (Option α) n ⊕ Sym α n.succ) : encode (decode s) = s

def symOptionSuccEquiv {α : Type u_1} {n : ℕ} [DecidableEq α] : Sym (Option α) n.succ ≃ Sym (Option α) n ⊕ Sym α n.succ

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