List.count as a bundled homomorphism

In this file we define FreeMonoid.countP, FreeMonoid.count, FreeAddMonoid.countP, and FreeAddMonoid.count. These are List.countP and List.count bundled as multiplicative and additive homomorphisms from FreeMonoid and FreeAddMonoid.

We do not use to_additive because it can't map Multiplicative ℕ to ℕ.

TODO

There is lots of defeq abuse here of FreeAddMonoid α = List α, e.g. in statements like

theorem countP_apply (l : FreeAddMonoid α) : countP p l = List.countP p l := rfl

This needs cleaning up.

def FreeAddMonoid.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] : FreeAddMonoid α →+ ℕ

List.countP as a bundled additive monoid homomorphism.

Equations

• FreeAddMonoid.countP p = { toFun := List.countP fun (b : α) => decide (p b), map_zero' := ⋯, map_add' := ⋯ }

theorem FreeAddMonoid.countP_of {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : (FreeAddMonoid.countP p) (FreeAddMonoid.of x) = if p x = (true = true) then 1 else 0

theorem FreeAddMonoid.countP_apply {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : FreeAddMonoid α) : (FreeAddMonoid.countP p) l = List.countP (fun (b : α) => decide (p b)) l

def FreeAddMonoid.count {α : Type u_1} [DecidableEq α] (x : α) : FreeAddMonoid α →+ ℕ

List.count as a bundled additive monoid homomorphism.

Equations

• FreeAddMonoid.count x = FreeAddMonoid.countP fun (x_1 : α) => x_1 = x

theorem FreeAddMonoid.count_of {α : Type u_1} [DecidableEq α] (x y : α) : (FreeAddMonoid.count x) (FreeAddMonoid.of y) = Pi.single x 1 y

theorem FreeAddMonoid.count_apply {α : Type u_1} [DecidableEq α] (x : α) (l : FreeAddMonoid α) : (FreeAddMonoid.count x) l = List.count x l

def FreeMonoid.countP {α : Type u_1} (p : α → Prop) [DecidablePred p] : FreeMonoid α →* Multiplicative ℕ

List.countP as a bundled multiplicative monoid homomorphism.

Equations

• FreeMonoid.countP p = AddMonoidHom.toMultiplicative (FreeAddMonoid.countP p)

theorem FreeMonoid.countP_of' {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : (FreeMonoid.countP p) (FreeMonoid.of x) = if p x then Multiplicative.ofAdd 1 else Multiplicative.ofAdd 0

theorem FreeMonoid.countP_of {α : Type u_1} (p : α → Prop) [DecidablePred p] (x : α) : (FreeMonoid.countP p) (FreeMonoid.of x) = if p x then Multiplicative.ofAdd 1 else 1

theorem FreeMonoid.countP_apply {α : Type u_1} (p : α → Prop) [DecidablePred p] (l : FreeAddMonoid α) : (FreeMonoid.countP p) l = Multiplicative.ofAdd (List.countP (fun (b : α) => decide (p b)) l)

def FreeMonoid.count {α : Type u_1} [DecidableEq α] (x : α) : FreeMonoid α →* Multiplicative ℕ

List.count as a bundled additive monoid homomorphism.

Equations

• FreeMonoid.count x = FreeMonoid.countP fun (x_1 : α) => x_1 = x

theorem FreeMonoid.count_apply {α : Type u_1} [DecidableEq α] (x : α) (l : FreeAddMonoid α) : (FreeMonoid.count x) l = Multiplicative.ofAdd (List.count x l)

theorem FreeMonoid.count_of {α : Type u_1} [DecidableEq α] (x y : α) : (FreeMonoid.count x) (FreeMonoid.of y) = Pi.mulSingle x (Multiplicative.ofAdd 1) y