Equivalence between Multiset and ℕ-valued finitely supported functions

This defines Finsupp.toMultiset the equivalence between α →₀ ℕ and Multiset α, along with Multiset.toFinsupp the reverse equivalence and Finsupp.orderIsoMultiset (the equivalence promoted to an order isomorphism).

def Finsupp.toMultiset {α : Type u_1} : (α →₀ ℕ) →+ Multiset α

Given f : α →₀ ℕ, f.toMultiset is the multiset with multiplicities given by the values of f on the elements of α. We define this function as an AddMonoidHom.

Under the additional assumption of [DecidableEq α], this is available as Multiset.toFinsupp : Multiset α ≃+ (α →₀ ℕ); the two declarations are separate as this assumption is only needed for one direction.

Equations

• Finsupp.toMultiset = { toFun := fun (f : α →₀ ℕ) => f.sum fun (a : α) (n : ℕ) => n • {a}, map_zero' := ⋯, map_add' := ⋯ }

theorem Finsupp.toMultiset_zero {α : Type u_1} : Finsupp.toMultiset 0 = 0

theorem Finsupp.toMultiset_add {α : Type u_1} (m : α →₀ ℕ) (n : α →₀ ℕ) : Finsupp.toMultiset (m + n) = Finsupp.toMultiset m + Finsupp.toMultiset n

theorem Finsupp.toMultiset_apply {α : Type u_1} (f : α →₀ ℕ) : Finsupp.toMultiset f = f.sum fun (a : α) (n : ℕ) => n • {a}

@[simp]

theorem Finsupp.toMultiset_single {α : Type u_1} (a : α) (n : ℕ) : Finsupp.toMultiset (Finsupp.single a n) = n • {a}

theorem Finsupp.toMultiset_sum {α : Type u_1} {ι : Type u_3} {f : ι → α →₀ ℕ} (s : Finset ι) : Finsupp.toMultiset (∑ i ∈ s, f i) = ∑ i ∈ s, Finsupp.toMultiset (f i)

theorem Finsupp.toMultiset_sum_single {ι : Type u_3} (s : Finset ι) (n : ℕ) : Finsupp.toMultiset (∑ i ∈ s, Finsupp.single i n) = n • s.val

@[simp]

theorem Finsupp.card_toMultiset {α : Type u_1} (f : α →₀ ℕ) : Multiset.card (Finsupp.toMultiset f) = f.sum fun (x : α) => id

theorem Finsupp.toMultiset_map {α : Type u_1} {β : Type u_2} (f : α →₀ ℕ) (g : α → β) : Multiset.map g (Finsupp.toMultiset f) = Finsupp.toMultiset (Finsupp.mapDomain g f)

@[simp]

theorem Finsupp.prod_toMultiset {α : Type u_1} [CommMonoid α] (f : α →₀ ℕ) : (Finsupp.toMultiset f).prod = f.prod fun (a : α) (n : ℕ) => a ^ n

@[simp]

theorem Finsupp.sum_toMultiset {α : Type u_1} [AddCommMonoid α] (f : α →₀ ℕ) : (Finsupp.toMultiset f).sum = f.sum fun (a : α) (n : ℕ) => n • a

@[simp]

theorem Finsupp.toFinset_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) : (Finsupp.toMultiset f).toFinset = f.support

@[simp]

theorem Finsupp.count_toMultiset {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (a : α) : Multiset.count a (Finsupp.toMultiset f) = f a

theorem Finsupp.toMultiset_sup {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) : Finsupp.toMultiset (f ⊔ g) = Finsupp.toMultiset f ∪ Finsupp.toMultiset g

theorem Finsupp.toMultiset_inf {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) (g : α →₀ ℕ) : Finsupp.toMultiset (f ⊓ g) = Finsupp.toMultiset f ∩ Finsupp.toMultiset g

@[simp]

theorem Finsupp.mem_toMultiset {α : Type u_1} (f : α →₀ ℕ) (i : α) : i ∈ Finsupp.toMultiset f ↔ i ∈ f.support

def Multiset.toFinsupp {α : Type u_1} [DecidableEq α] : Multiset α ≃+ (α →₀ ℕ)

Given a multiset s, s.toFinsupp returns the finitely supported function on ℕ given by the multiplicities of the elements of s.

Equations

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

@[simp]

theorem Multiset.toFinsupp_symm_apply {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) : Multiset.toFinsupp.symm f = Finsupp.toMultiset f

@[simp]

theorem Multiset.toFinsupp_support {α : Type u_1} [DecidableEq α] (s : Multiset α) : (Multiset.toFinsupp s).support = s.toFinset

@[simp]

theorem Multiset.toFinsupp_apply {α : Type u_1} [DecidableEq α] (s : Multiset α) (a : α) : (Multiset.toFinsupp s) a = Multiset.count a s

theorem Multiset.toFinsupp_zero {α : Type u_1} [DecidableEq α] : Multiset.toFinsupp 0 = 0

theorem Multiset.toFinsupp_add {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.toFinsupp (s + t) = Multiset.toFinsupp s + Multiset.toFinsupp t

@[simp]

theorem Multiset.toFinsupp_singleton {α : Type u_1} [DecidableEq α] (a : α) : Multiset.toFinsupp {a} = Finsupp.single a 1

@[simp]

theorem Multiset.toFinsupp_toMultiset {α : Type u_1} [DecidableEq α] (s : Multiset α) : Finsupp.toMultiset (Multiset.toFinsupp s) = s

theorem Multiset.toFinsupp_eq_iff {α : Type u_1} [DecidableEq α] {s : Multiset α} {f : α →₀ ℕ} : Multiset.toFinsupp s = f ↔ s = Finsupp.toMultiset f

theorem Multiset.toFinsupp_union {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.toFinsupp (s ∪ t) = Multiset.toFinsupp s ⊔ Multiset.toFinsupp t

theorem Multiset.toFinsupp_inter {α : Type u_1} [DecidableEq α] (s : Multiset α) (t : Multiset α) : Multiset.toFinsupp (s ∩ t) = Multiset.toFinsupp s ⊓ Multiset.toFinsupp t

@[simp]

theorem Multiset.toFinsupp_sum_eq {α : Type u_1} [DecidableEq α] (s : Multiset α) : ((Multiset.toFinsupp s).sum fun (x : α) => id) = Multiset.card s

@[simp]

theorem Finsupp.toMultiset_toFinsupp {α : Type u_1} [DecidableEq α] (f : α →₀ ℕ) : Multiset.toFinsupp (Finsupp.toMultiset f) = f

theorem Finsupp.toMultiset_eq_iff {α : Type u_1} [DecidableEq α] {f : α →₀ ℕ} {s : Multiset α} : Finsupp.toMultiset f = s ↔ f = Multiset.toFinsupp s

As an order isomorphism

def Finsupp.orderIsoMultiset {ι : Type u_3} [DecidableEq ι] : (ι →₀ ℕ) ≃o Multiset ι

Finsupp.toMultiset as an order isomorphism.

Equations

• Finsupp.orderIsoMultiset = { toEquiv := Multiset.toFinsupp.symm.toEquiv, map_rel_iff' := ⋯ }

@[simp]

theorem Finsupp.coe_orderIsoMultiset {ι : Type u_3} [DecidableEq ι] : ⇑Finsupp.orderIsoMultiset = ⇑Finsupp.toMultiset

@[simp]

theorem Finsupp.coe_orderIsoMultiset_symm {ι : Type u_3} [DecidableEq ι] : ⇑Finsupp.orderIsoMultiset.symm = ⇑Multiset.toFinsupp

theorem Finsupp.toMultiset_strictMono {ι : Type u_3} : StrictMono ⇑Finsupp.toMultiset

theorem Finsupp.sum_id_lt_of_lt {ι : Type u_3} (m : ι →₀ ℕ) (n : ι →₀ ℕ) (h : m < n) : (m.sum fun (x : ι) => id) < n.sum fun (x : ι) => id

theorem Finsupp.lt_wf (ι : Type u_3) : WellFounded LT.lt

The order on ι →₀ ℕ is well-founded.

instance Finsupp.instWellFoundedRelationNat (ι : Type u_3) : WellFoundedRelation (ι →₀ ℕ)

Equations

• Finsupp.instWellFoundedRelationNat ι = { rel := fun (x1 x2 : ι →₀ ℕ) => x1 < x2, wf := ⋯ }

theorem Multiset.toFinsupp_strictMono {ι : Type u_3} [DecidableEq ι] : StrictMono ⇑Multiset.toFinsupp

def Sym.equivNatSum (α : Type u_1) [DecidableEq α] (n : ℕ) : Sym α n ≃ { P : α →₀ ℕ // (P.sum fun (x : α) => id) = n }

The nth symmetric power of a type α is naturally equivalent to the subtype of finitely-supported maps α →₀ ℕ with total mass n.

See also Sym.equivNatSumOfFintype when α is finite.

Equations

• Sym.equivNatSum α n = Multiset.toFinsupp.subtypeEquiv ⋯

@[simp]

theorem Sym.coe_equivNatSum_apply_apply (α : Type u_1) [DecidableEq α] (n : ℕ) (s : Sym α n) (a : α) : ↑((Sym.equivNatSum α n) s) a = Multiset.count a ↑s

@[simp]

theorem Sym.coe_equivNatSum_symm_apply (α : Type u_1) [DecidableEq α] (n : ℕ) (P : { P : α →₀ ℕ // (P.sum fun (x : α) => id) = n }) : ↑((Sym.equivNatSum α n).symm P) = Finsupp.toMultiset ↑P

noncomputable def Sym.equivNatSumOfFintype (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] : Sym α n ≃ { P : α → ℕ // ∑ i : α, P i = n }

The nth symmetric power of a finite type α is naturally equivalent to the subtype of maps α → ℕ with total mass n.

See also Sym.equivNatSum when α is not necessarily finite.

Equations

• Sym.equivNatSumOfFintype α n = (Sym.equivNatSum α n).trans (Finsupp.equivFunOnFinite.subtypeEquiv ⋯)

@[simp]

theorem Sym.coe_equivNatSumOfFintype_apply_apply (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] (s : Sym α n) (a : α) : ↑((Sym.equivNatSumOfFintype α n) s) a = Multiset.count a ↑s

@[simp]

theorem Sym.coe_equivNatSumOfFintype_symm_apply (α : Type u_1) [DecidableEq α] (n : ℕ) [Fintype α] (P : { P : α → ℕ // ∑ i : α, P i = n }) : ↑((Sym.equivNatSumOfFintype α n).symm P) = ∑ a : α, ↑P a • {a}