Hom. from a (multiplicative) monoid to an (additive) monoid

Stream: new members

[Philippe Duchon]

Is there a way to pretend that a mapping from some (multiplicative) Monoid to an (additive) AddMonoid is a homomorphism of some kind?

The base case I have in mind is the length of words over some alphabet. I see that Mathlib has a length function from words to ℕ (which is really List.length in thin disguise), and theorems (both in the multiplicative and additive settings) that the length of a concatenation of two words is the sum of their lengths, but it seems that none is described as a homomorphism. At least it could/should be in the additive case?

In fact, what I would like to be able to do is define some alternative notions of length, where each letter could be defined to have a different "length". I can do this with FreeAddMonoid.lift, but if I try to use FreeMonoid.lift (because I would really like to write concatenation multiplicatively), Lean picks the multiplicative monoid on ℕ and that's not at all what I want.

I suppose this is a sign that I don't really understand the problems with instance synthesis (like, having an instance to make a Monoid from a FreeMonoid and vice versa would probably create loops in the instance resolution program, and I can imagine this would be pretty bad)

[Ruben Van de Velde]

Something something docs#Additive

[Yakov Pechersky]

docs#MonoidHom.toAdditive'

[Philippe Duchon]

Not sure how to use this in practice, but thanks for the pointers.

(Why are so many thing hidden in Mathlib.Algebra.Group, when there is no group in sight?)

[Yakov Pechersky]

import Mathlib

variable {X : Type*}

instance : Add (List X) := ⟨List.append⟩
instance : Zero (List X) := ⟨[]⟩
instance : AddZeroClass (List X) where
  zero_add _ := rfl
  add_zero := List.append_nil

def lengthHom : List X →+ ℕ where
  toFun := List.length
  map_zero' := List.length_nil
  map_add' _ _ := List.length_append

[Yakov Pechersky]

You could/should probably scope these

[Yakov Pechersky]

For free monoid, let's see...

[Yakov Pechersky]

import Mathlib

variable {X : Type*}

def lengthHom : FreeMonoid X →* Multiplicative ℕ :=
  AddMonoidHom.toMultiplicative' {
    toFun := FreeMonoid.length ∘ Additive.toMul
    map_zero' := by simp
    map_add' := by simp
  }

[Philippe Duchon]

Thanks! (Though, having something like Multiplicative ℕ is probably a bit confusing)

[Edward van de Meent]

this loogle query suggests that it is not an uncommon pattern