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 α // Multiset.card s = n }

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

The canonical 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

• Sym.hasCoe α n = { coe := Sym.toMultiset }

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

Equations

• instDecidableEqSym = Subtype.instDecidableEqSubtype

@[reducible]

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

• Vector.Perm.isSetoid α n = Setoid.comap Subtype.val (List.isSetoid α)

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

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

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 := ⋯ }

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

• a ::ₛ s = { val := a ::ₘ ↑s, property := ⋯ }

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

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

Equations

• Sym.«term_::ₛ_» = Lean.ParserDescr.trailingNode `Sym.term_::ₛ_ 67 68 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " ::ₛ ") (Lean.ParserDescr.cat `term 67))

@[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 α 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.ofVector x = { val := ↑↑x, property := ⋯ }

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

• Sym.instCoeVectorSym = { coe := fun (x : Vector α n) => Sym.ofVector x }

@[simp]

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

@[simp]

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

@[simp]

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

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

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

Equations

• Sym.instMembershipSym = { mem := fun (a : α) (s : Sym α n) => a ∈ ↑s }

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

Equations

• Sym.decidableMem a s = Multiset.decidableMem a ↑s

@[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.not_mem_nil {α : Type u_1} (a : α) : a ∉ Sym.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 : Vector α n) : a ::ₛ Sym.ofVector v = Sym.ofVector (a ::ᵥ v)

theorem Sym.sound {α : Type u_1} {n : ℕ} {a : Vector α n} {b : Vector α n} (h : List.Perm ↑a ↑b) : Sym.ofVector a = Sym.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.

Equations

• Sym.erase s a h = { val := Multiset.erase (↑s) a, property := ⋯ }

@[simp]

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

@[simp]

theorem Sym.coe_erase {α : Type u_1} {n : ℕ} [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 : ℕ} [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 : ℕ} [DecidableEq α] (s : Sym α n) (a : α) (h : optParam (a ∈ a ::ₛ s) ⋯) : Sym.erase (a ::ₛ s) 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.)

Equations

• Sym.Sym' α n = Quotient (Vector.Perm.isSetoid α n)

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

This is cons but for the alternative Sym' definition.

Equations

• Sym.cons' a = Quotient.map (Vector.cons a) ⋯

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

This is cons but for the alternative Sym' definition.

Equations

• Sym.«term_::_» = Lean.ParserDescr.trailingNode `Sym.term_::_ 1022 0 (Lean.ParserDescr.binary `andthen (Lean.ParserDescr.symbol " :: ") (Lean.ParserDescr.cat `term 0))

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

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

Equations

• Sym.symEquivSym' = Equiv.subtypeQuotientEquivQuotientSubtype (fun (l : List α) => List.length l = n) (fun (s : Multiset α) => Multiset.card s = n) ⋯ ⋯

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

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

Equations

• Sym.instZeroSym = { zero := { val := 0, property := ⋯ } }

instance Sym.instEmptyCollectionSymOfNatNatInstOfNatNat {α : Type u_1} : EmptyCollection (Sym α 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 := ⋯ }

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 = { val := Multiset.replicate n a, property := ⋯ }

theorem Sym.replicate_succ {α : Type u_1} {a : α} {n : ℕ} : Sym.replicate (Nat.succ n) 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 ∈ s, b = a

theorem Sym.exists_mem {α : Type u_1} {n : ℕ} (s : Sym α (Nat.succ n)) : ∃ (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 α (Nat.succ n)) : ∃ (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 ∈ s, b = a

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

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

Equations

• ⋯ = ⋯

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

Equations

• Sym.inhabitedSym n = { default := Sym.replicate n default }

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

Equations

• Sym.inhabitedSym' n = { default := Quotient.mk' (Vector.replicate n default) }

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

Equations

• ⋯ = ⋯

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

Equations

• Sym.instUniqueSym 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)

instance Sym.instNontrivialSymHAddNatInstHAddInstAddNatOfNat {α : Type u_1} (n : ℕ) [Nontrivial α] : Nontrivial (Sym α (n + 1))

Equations

• ⋯ = ⋯

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 = { val := Multiset.map f ↑x, property := ⋯ }

@[simp]

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

@[simp]

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

@[simp]

theorem Sym.map_map {α : Type u_3} {β : Type u_4} {γ : Type u_5} {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 ∈ 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)

@[simp]

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

@[simp]

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

• Sym.equivCongr e = { toFun := Sym.map ⇑e, invFun := Sym.map ⇑e.symm, left_inv := ⋯, right_inv := ⋯ }

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

• Sym.attach s = { val := Multiset.attach ↑s, property := ⋯ }

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

@[simp]

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

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 }) : x ∈ Sym.attach 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 := ⋯ } ::ₛ Sym.map (fun (x_1 : { x : α // x ∈ s }) => { val := ↑x_1, property := ⋯ }) (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

• Sym.cast h = { toFun := fun (s : Sym α n) => { val := ↑s, property := ⋯ }, invFun := fun (s : Sym α m) => { val := ↑s, property := ⋯ }, left_inv := ⋯, right_inv := ⋯ }

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

Equations

• Sym.append s s' = { val := ↑s + ↑s', property := ⋯ }

@[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 ⋯) (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

• Sym.fill a i m = (Sym.cast ⋯) (Sym.append m (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.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).

Equations

• Sym.filterNe a m = { fst := { val := Multiset.count a ↑m, isLt := ⋯ }, snd := { val := Multiset.filter (fun (x : α) => a ≠ x) ↑m, property := ⋯ } }

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 : ℕ} [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 : ℕ} [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

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 ↑(Sym.fill a i s) = ↑i

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 ↑(Sym.fill a i s) = Multiset.count x ↑s

Combinatorial equivalences

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

• SymOptionSuccEquiv.encode s = if h : none ∈ s then Sum.inl (Sym.erase s none h) else Sum.inr (Sym.map (fun (o : { x : Option α // x ∈ s }) => Option.get ↑o ⋯) (Sym.attach s))

@[simp]

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

@[simp]

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

• SymOptionSuccEquiv.decode x = match x with | Sum.inl s => none ::ₛ s | Sum.inr s => Sym.map (⇑Function.Embedding.some) s

@[simp]

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

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

@[simp]

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

@[simp]

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

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

• symOptionSuccEquiv = { toFun := SymOptionSuccEquiv.encode, invFun := SymOptionSuccEquiv.decode, left_inv := ⋯, right_inv := ⋯ }