Relation between the free semigroup and the free monoid

We provide some constructions relating the free semigroup and the free monoid on the same type.

Main definitions

• FreeSemigroup.toFreeMonoid: the natural embedding of the free semigroup into the free monoid.
• FreeMonoid.equivWithOneFreeSemigroup: the free monoid is isomorphic to the free semigroup with a 1 added.

def FreeSemigroup.toFreeMonoid {α : Type u_1} : FreeSemigroup α →ₙ* FreeMonoid α

The natural embedding of the free semigroup into the free monoid. This is injective (FreeSemigroup.toFreeMonoid_injective), and its image consists of all non-1 elements of the free monoid (FreeSemigroup.eq_one_or_toFreeMonoid).

Equations

• FreeSemigroup.toFreeMonoid = FreeSemigroup.lift FreeMonoid.of

def FreeAddSemigroup.toFreeAddMonoid {α : Type u_1} : FreeAddSemigroup α →ₙ+ FreeAddMonoid α

The natural embedding of the free additive semigroup into the free additive monoid. This is injective (FreeAddSemigroup.toFreeAddMonoid_injective), and its image consists of all non-0 elements of the free additive monoid (FreeAddSemigroup.eq_zero_or_toFreeAddMonoid).

Equations

• FreeAddSemigroup.toFreeAddMonoid = FreeAddSemigroup.lift FreeAddMonoid.of

@[simp]

theorem FreeSemigroup.toFreeMonoid_of {α : Type u_1} (x : α) : toFreeMonoid (of x) = FreeMonoid.of x

@[simp]

theorem FreeAddSemigroup.toFreeAddMonoid_of {α : Type u_1} (x : α) : toFreeAddMonoid (of x) = FreeAddMonoid.of x

theorem FreeSemigroup.toFreeMonoid_mk_eq_cons {α : Type u_1} (x : α) (xs : List α) : toFreeMonoid { head := x, tail := xs } = FreeMonoid.ofList (x :: xs)

theorem FreeAddSemigroup.toFreeAddMonoid_mk_eq_cons {α : Type u_1} (x : α) (xs : List α) : toFreeAddMonoid { head := x, tail := xs } = FreeAddMonoid.ofList (x :: xs)

theorem FreeSemigroup.toFreeMonoid_injective {α : Type u_1} : Function.Injective ⇑toFreeMonoid

theorem FreeAddSemigroup.toFreeAddMonoid_injective {α : Type u_1} : Function.Injective ⇑toFreeAddMonoid

@[simp]

theorem FreeSemigroup.toFreeMonoid_ne_one {α : Type u_1} (x : FreeSemigroup α) : toFreeMonoid x ≠ 1

@[simp]

theorem FreeAddSemigroup.toFreeAddMonoid_ne_zero {α : Type u_1} (x : FreeAddSemigroup α) : toFreeAddMonoid x ≠ 0

theorem FreeSemigroup.eq_one_or_toFreeMonoid {α : Type u_1} (x : FreeMonoid α) : x = 1 ∨ ∃ (y : FreeSemigroup α), toFreeMonoid y = x

theorem FreeAddSemigroup.eq_zero_or_toFreeAddMonoid {α : Type u_1} (x : FreeAddMonoid α) : x = 0 ∨ ∃ (y : FreeAddSemigroup α), toFreeAddMonoid y = x

@[simp]

theorem FreeSemigroup.range_toFreeMonoid {α : Type u_1} : Set.range ⇑toFreeMonoid = {1}ᶜ

@[simp]

theorem FreeAddSemigroup.range_toFreeAddMonoid {α : Type u_1} : Set.range ⇑toFreeAddMonoid = {0}ᶜ

def FreeMonoid.equivWithOneFreeSemigroup {α : Type u_1} : FreeMonoid α ≃* WithOne (FreeSemigroup α)

The free monoid on α is isomorphic to the free semigroup on α with a 1 added.

Equations

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

def FreeAddMonoid.equivWithZeroFreeAddSemigroup {α : Type u_1} : FreeAddMonoid α ≃+ WithZero (FreeAddSemigroup α)

The free additive monoid on α is isomorphic to the free additive semigroup on α with a 0 added.

Equations

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

@[simp]

theorem FreeMonoid.equivWithOneFreeSemigroup_symm_apply {α : Type u_1} (a : WithOne (FreeSemigroup α)) : equivWithOneFreeSemigroup.symm a = (WithOne.lift FreeSemigroup.toFreeMonoid) a

@[simp]

theorem FreeAddMonoid.equivWithZeroFreeAddSemigroup_apply {α : Type u_1} (a : FreeAddMonoid α) : equivWithZeroFreeAddSemigroup a = (lift fun (x : α) => ↑(FreeAddSemigroup.of x)) a

@[simp]

theorem FreeAddMonoid.equivWithZeroFreeAddSemigroup_symm_apply {α : Type u_1} (a : WithZero (FreeAddSemigroup α)) : equivWithZeroFreeAddSemigroup.symm a = (WithZero.lift FreeAddSemigroup.toFreeAddMonoid) a

@[simp]

theorem FreeMonoid.equivWithOneFreeSemigroup_apply {α : Type u_1} (a : FreeMonoid α) : equivWithOneFreeSemigroup a = (lift fun (x : α) => ↑(FreeSemigroup.of x)) a