The free monoid as the unitization of the free semigroup

FreeMonoid.equivWithOneFreeSemigroup sends the image of FreeSemigroup.toFreeMonoid to the WithOne coercion, and a homomorphism out of the free semigroup extends along it to the free monoid (FreeMonoid.mapWithOne), with the empty word sent to 1.

theorem FreeMonoid.equivWithOneFreeSemigroup_toFreeMonoid {α : Type u_1} (u : FreeSemigroup α) : equivWithOneFreeSemigroup (FreeSemigroup.toFreeMonoid u) = ↑u

@[simp]

theorem FreeSemigroup.toList_toFreeMonoid_ne_nil {α : Type u_1} (u : FreeSemigroup α) : FreeMonoid.toList (toFreeMonoid u) ≠ []

def FreeMonoid.mapWithOne {α : Type u_1} {T : Type u_2} [Mul T] (η : FreeSemigroup α →ₙ* T) : FreeMonoid α →* WithOne T

The extension of a homomorphism out of the free semigroup to the free monoid, with the empty word sent to 1.

Equations

• FreeMonoid.mapWithOne η = (WithOne.mapMulHom η).comp FreeMonoid.equivWithOneFreeSemigroup.toMonoidHom

@[simp]

theorem FreeMonoid.mapWithOne_toFreeMonoid {α : Type u_1} (u : FreeSemigroup α) {T : Type u_2} [Mul T] (η : FreeSemigroup α →ₙ* T) : (mapWithOne η) (FreeSemigroup.toFreeMonoid u) = ↑(η u)

theorem FreeMonoid.mapWithOne_ofList_cons {α : Type u_1} {T : Type u_2} [Mul T] (η : FreeSemigroup α →ₙ* T) (c : α) (l : List α) : (mapWithOne η) (ofList (c :: l)) = ↑(η { head := c, tail := l })