Mathlib.Algebra.FreeMonoid.Basic

FreeMonoid definition

(α)

Full source

/--
If `α` is a type, then `FreeMonoid α` is the free monoid generated by `α`.
This is a monoid equipped with a function `FreeMonoid.of : α → FreeMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeMonoid.of` and a unique monoid homomorphism
`FreeMonoid.lift f : FreeMonoid α →* M`.

A typical element of `FreeMonoid α` is a formal product of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x * y * y * x` is a
"typical" element of `FreeMonoid α`. In particular if `α` is empty
then `FreeMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeMonoid α` is isomorphic to `Multiplicative ℕ`.
If `α` has two or more terms then `FreeMonoid α` is not commutative.
One can think of `FreeMonoid α` as the type of lists of `α`, with multiplication
given by concatenation.
-/
@[to_additive
"
If `α` is a type, then `FreeAddMonoid α` is the free additive monoid generated by `α`.
This is a monoid equipped with a function `FreeAddMonoid.of : α → FreeAddMonoid α` which has
the following universal property: if `M` is any monoid, and `f : α → M` is any function,
then this function is the composite of `FreeAddMonoid.of` and a unique monoid homomorphism
`FreeAddMonoid.lift f : FreeAddMonoid α →+ M`.

A typical element of `FreeAddMonoid α` is a formal sum of elements of `α`.
For example if `x` and `y` are terms of type `α` then `x + y + y + x` is a
\"typical\" element of `FreeAddMonoid α`. In particular if `α` is empty
then `FreeAddMonoid α` is isomorphic to the trivial monoid, and if `α` has one term
then `FreeAddMonoid α` is isomorphic to `ℕ`.
If `α` has two or more terms then `FreeAddMonoid α` is not commutative.
One can think of `FreeAddMonoid α` as the type of lists of `α`, with addition
given by concatenation.
"]
def FreeMonoid (α) := List α

Free monoid over a type

Informal description

The free monoid over a type $\alpha$, denoted $\text{FreeMonoid}(\alpha)$, is the monoid whose elements are finite lists of elements of $\alpha$, with multiplication given by concatenation of lists. It is equipped with a canonical embedding $\text{FreeMonoid.of} : \alpha \to \text{FreeMonoid}(\alpha)$ that sends each element $x \in \alpha$ to the singleton list $[x]$. This construction satisfies the universal property: for any monoid $M$ and any function $f : \alpha \to M$, there exists a unique monoid homomorphism $\text{FreeMonoid.lift}(f) : \text{FreeMonoid}(\alpha) \to M$ such that $f = \text{FreeMonoid.lift}(f) \circ \text{FreeMonoid.of}$. When $\alpha$ is empty, $\text{FreeMonoid}(\alpha)$ is isomorphic to the trivial monoid. When $\alpha$ has one element, $\text{FreeMonoid}(\alpha)$ is isomorphic to the multiplicative monoid of natural numbers. For $\alpha$ with two or more elements, $\text{FreeMonoid}(\alpha)$ is non-commutative.

FreeMonoid.toList definition

: FreeMonoid α ≃ List α

Full source

/-- The identity equivalence between `FreeMonoid α` and `List α`. -/
@[to_additive "The identity equivalence between `FreeAddMonoid α` and `List α`."]
def toList : FreeMonoidFreeMonoid α ≃ List α := Equiv.refl _

Identity equivalence between free monoid and lists

Informal description

The equivalence `FreeMonoid.toList` is the identity bijection between the free monoid over an alphabet $\alpha$ (denoted $\text{FreeMonoid}(\alpha)$) and the type of lists over $\alpha$ (denoted $\text{List}(\alpha)$). This means it maps each element of the free monoid to itself viewed as a list, and vice versa, with the inverse operation being the same mapping in the opposite direction.

FreeMonoid.ofList definition

: List α ≃ FreeMonoid α

Full source

/-- The identity equivalence between `List α` and `FreeMonoid α`. -/
@[to_additive "The identity equivalence between `List α` and `FreeAddMonoid α`."]
def ofList : ListList α ≃ FreeMonoid α := Equiv.refl _

Identity equivalence between lists and free monoid

Informal description

The equivalence `FreeMonoid.ofList` is the identity bijection between the type of lists over an alphabet $\alpha$ (denoted $\text{List}(\alpha)$) and the free monoid over $\alpha$ (denoted $\text{FreeMonoid}(\alpha)$). This means it maps each list to itself viewed as an element of the free monoid, and vice versa, with the inverse operation being the same mapping in the opposite direction.

FreeMonoid.toList_symm theorem

: (@toList α).symm = ofList

Full source

@[to_additive (attr := simp)]
theorem toList_symm : (@toList α).symm = ofList := rfl

Inverse of Free Monoid to List Equivalence is List to Free Monoid Equivalence

Informal description

The inverse of the identity equivalence between the free monoid over $\alpha$ and the list type $\text{List}(\alpha)$ is equal to the identity equivalence in the opposite direction, i.e., $(\text{FreeMonoid.toList})^{-1} = \text{FreeMonoid.ofList}$.

FreeMonoid.ofList_symm theorem

: (@ofList α).symm = toList

Full source

@[to_additive (attr := simp)]
theorem ofList_symm : (@ofList α).symm = toList := rfl

Inverse of List-FreeMonoid Identity Equivalence

Informal description

The inverse of the identity equivalence between lists over $\alpha$ and the free monoid over $\alpha$ is equal to the identity equivalence in the opposite direction. That is, $(\text{FreeMonoid.ofList})^{-1} = \text{FreeMonoid.toList}$.

FreeMonoid.toList_ofList theorem

(l : List α) : toList (ofList l) = l

Full source

@[to_additive (attr := simp)]
theorem toList_ofList (l : List α) : toList (ofList l) = l := rfl

$\text{toList} \circ \text{ofList} = \text{id}$ for lists in the free monoid

Informal description

For any list $l$ of elements of type $\alpha$, the composition of the functions $\text{toList}$ and $\text{ofList}$ applied to $l$ returns $l$ itself, i.e., $\text{toList}(\text{ofList}(l)) = l$.

FreeMonoid.ofList_toList theorem

(xs : FreeMonoid α) : ofList (toList xs) = xs

Full source

@[to_additive (attr := simp)]
theorem ofList_toList (xs : FreeMonoid α) : ofList (toList xs) = xs := rfl

Identity Property of Free Monoid Embedding and Projection

Informal description

For any element $xs$ of the free monoid over $\alpha$, the composition of the embedding $\text{ofList}$ with the projection $\text{toList}$ yields the identity, i.e., $\text{ofList}(\text{toList}(xs)) = xs$.

FreeMonoid.toList_comp_ofList theorem

: @toList α ∘ ofList = id

Full source

@[to_additive (attr := simp)]
theorem toList_comp_ofList : @toList α ∘ ofList = id := rfl

Composition of Free Monoid Conversions Yields Identity on Lists

Informal description

The composition of the functions $\text{toList} : \text{FreeMonoid}(\alpha) \to \text{List}(\alpha)$ and $\text{ofList} : \text{List}(\alpha) \to \text{FreeMonoid}(\alpha)$ is equal to the identity function on $\text{List}(\alpha)$, i.e., $\text{toList} \circ \text{ofList} = \text{id}$.

FreeMonoid.ofList_comp_toList theorem

: @ofList α ∘ toList = id

Full source

@[to_additive (attr := simp)]
theorem ofList_comp_toList : @ofList α ∘ toList = id := rfl

Composition of $\text{ofList}$ and $\text{toList}$ is Identity on Free Monoid

Informal description

The composition of the functions $\text{ofList}$ and $\text{toList}$ is the identity function on the free monoid over $\alpha$, i.e., $\text{ofList} \circ \text{toList} = \text{id}$.

FreeMonoid.instCancelMonoid instance

: CancelMonoid (FreeMonoid α)

Full source

@[to_additive]
instance : CancelMonoid (FreeMonoid α) where
  one := ofList []
  mul x y := ofList (toList x ++ toList y)
  mul_one := List.append_nil
  one_mul := List.nil_append
  mul_assoc := List.append_assoc
  mul_left_cancel _ _ _ := List.append_cancel_left
  mul_right_cancel _ _ _ := List.append_cancel_right

The Free Monoid is Cancellative

Informal description

The free monoid $\text{FreeMonoid}(\alpha)$ over any alphabet $\alpha$ is a cancellative monoid. That is, for any elements $x, y, z \in \text{FreeMonoid}(\alpha)$, if $x \cdot y = x \cdot z$ or $y \cdot x = z \cdot x$, then $y = z$.

FreeMonoid.instInhabited instance

: Inhabited (FreeMonoid α)

Full source

@[to_additive]
instance : Inhabited (FreeMonoid α) := ⟨1⟩

The Free Monoid is Inhabited

Informal description

The free monoid $\text{FreeMonoid}(\alpha)$ over any type $\alpha$ is inhabited, meaning it contains at least one element (the empty list).

FreeMonoid.instUniqueOfIsEmpty instance

[IsEmpty α] : Unique (FreeMonoid α)

Full source

@[to_additive]
instance [IsEmpty α] : Unique (FreeMonoid α) := inferInstanceAs <| Unique (List α)

Uniqueness of the Free Monoid over an Empty Alphabet

Informal description

For any empty type $\alpha$, the free monoid $\text{FreeMonoid}(\alpha)$ has exactly one element (the empty list).

FreeMonoid.toList_one theorem

: toList (1 : FreeMonoid α) = []

Full source

@[to_additive (attr := simp)]
theorem toList_one : toList (1 : FreeMonoid α) = [] := rfl

Identity Element Maps to Empty List in Free Monoid

Informal description

The equivalence `FreeMonoid.toList` maps the multiplicative identity element $1$ of the free monoid over $\alpha$ to the empty list, i.e., $\text{toList}(1) = []$.

FreeMonoid.ofList_nil theorem

: ofList ([] : List α) = 1

Full source

@[to_additive (attr := simp)]
theorem ofList_nil : ofList ([] : List α) = 1 := rfl

Empty List Maps to Identity in Free Monoid

Informal description

The embedding `ofList` maps the empty list `[]` to the identity element `1` of the free monoid $\text{FreeMonoid}(\alpha)$.

FreeMonoid.toList_nil theorem

: toList ([] : FreeMonoid α) = []

Full source

@[to_additive (attr := simp)]
theorem toList_nil : toList ([] : FreeMonoid α) = [] := rfl

Empty element maps to empty list under `FreeMonoid.toList`

Informal description

The equivalence `FreeMonoid.toList` maps the empty element of the free monoid over $\alpha$ to the empty list, i.e., $\text{toList}(1_{\text{FreeMonoid}(\alpha)}) = []$.

FreeMonoid.toList_cons theorem

(x : α) (xs : FreeMonoid α) : toList (x :: xs) = x :: toList xs

Full source

@[to_additive (attr := simp)]
theorem toList_cons (x : α) (xs : FreeMonoid α) : toList (x :: xs) = x :: toList xs := rfl

List Representation of Free Monoid Concatenation

Informal description

For any element $x$ in $\alpha$ and any element $xs$ in the free monoid $\text{FreeMonoid}(\alpha)$, the list representation of the concatenation $x :: xs$ is equal to the list obtained by prepending $x$ to the list representation of $xs$. That is, $\text{toList}(x :: xs) = x :: \text{toList}(xs)$.

FreeMonoid.toList_mul theorem

(xs ys : FreeMonoid α) : toList (xs * ys) = toList xs ++ toList ys

Full source

@[to_additive (attr := simp)]
theorem toList_mul (xs ys : FreeMonoid α) : toList (xs * ys) = toList xs ++ toList ys := rfl

List Representation Preserves Free Monoid Multiplication

Informal description

For any elements $xs$ and $ys$ in the free monoid $\text{FreeMonoid}(\alpha)$, the list representation of their product $xs * ys$ is equal to the concatenation of their individual list representations. That is, $\text{toList}(xs * ys) = \text{toList}(xs) \mathbin{+\!\!+} \text{toList}(ys)$.

FreeMonoid.ofList_append theorem

(xs ys : List α) : ofList (xs ++ ys) = ofList xs * ofList ys

Full source

@[to_additive (attr := simp)]
theorem ofList_append (xs ys : List α) : ofList (xs ++ ys) = ofList xs * ofList ys := rfl

Embedding Preserves List Concatenation in Free Monoid

Informal description

For any two lists $xs$ and $ys$ over an alphabet $\alpha$, the embedding of their concatenation $xs ++ ys$ into the free monoid $\text{FreeMonoid}(\alpha)$ is equal to the product of their individual embeddings, i.e., $\text{ofList}(xs ++ ys) = \text{ofList}(xs) * \text{ofList}(ys)$.

FreeMonoid.toList_prod theorem

(xs : List (FreeMonoid α)) : toList xs.prod = (xs.map toList).flatten

Full source

@[to_additive (attr := simp)]
theorem toList_prod (xs : List (FreeMonoid α)) : toList xs.prod = (xs.map toList).flatten := by
  induction xs <;> simp [*, List.flatten]

Product-to-List Flattening in Free Monoid

Informal description

For any list $xs$ of elements in the free monoid $\text{FreeMonoid}(\alpha)$, the list representation of the product of $xs$ is equal to the concatenation (flattening) of the list representations of its elements. That is, if $xs = [w_1, \dots, w_n]$ where each $w_i \in \text{FreeMonoid}(\alpha)$, then $\text{toList}(\prod_{i=1}^n w_i) = \text{concat}_{i=1}^n \text{toList}(w_i)$.

FreeMonoid.ofList_flatten theorem

(xs : List (List α)) : ofList xs.flatten = (xs.map ofList).prod

Full source

@[to_additive (attr := simp)]
theorem ofList_flatten (xs : List (List α)) : ofList xs.flatten = (xs.map ofList).prod :=
  toList.injective <| by simp

Free Monoid Embedding Preserves List Flattening: $\text{ofList}(\text{flatten}(xs)) = \prod \text{ofList}(xs)$

Informal description

For any list of lists $xs$ over an alphabet $\alpha$, the embedding of the concatenated list $\text{flatten}(xs)$ into the free monoid $\text{FreeMonoid}(\alpha)$ is equal to the product of the embeddings of each individual list in $xs$. That is, $\text{ofList}(\text{flatten}(xs)) = \prod_{l \in xs} \text{ofList}(l)$.

FreeMonoid.of definition

(x : α) : FreeMonoid α

Full source

/-- Embeds an element of `α` into `FreeMonoid α` as a singleton list. -/
@[to_additive "Embeds an element of `α` into `FreeAddMonoid α` as a singleton list."]
def of (x : α) : FreeMonoid α := ofList [x]

Embedding into the free monoid

Informal description

The function $\text{FreeMonoid.of} : \alpha \to \text{FreeMonoid}(\alpha)$ embeds an element $x \in \alpha$ into the free monoid over $\alpha$ as the singleton list $[x]$.

FreeMonoid.toList_of theorem

(x : α) : toList (of x) = [x]

Full source

@[to_additive (attr := simp)]
theorem toList_of (x : α) : toList (of x) = [x] := rfl

List Representation of Free Monoid Embedding: $\text{toList}(\text{of}(x)) = [x]$

Informal description

For any element $x$ of type $\alpha$, the list representation of the free monoid element $\text{FreeMonoid.of}(x)$ is the singleton list $[x]$.

FreeMonoid.ofList_singleton theorem

(x : α) : ofList [x] = of x

Full source

@[to_additive]
theorem ofList_singleton (x : α) : ofList [x] = of x := rfl

Equivalence of Singleton List and Free Monoid Embedding

Informal description

For any element $x$ of type $\alpha$, the equivalence `ofList` maps the singleton list $[x]$ to the free monoid element $\text{FreeMonoid.of}(x)$.

FreeMonoid.ofList_cons theorem

(x : α) (xs : List α) : ofList (x :: xs) = of x * ofList xs

Full source

@[to_additive (attr := simp)]
theorem ofList_cons (x : α) (xs : List α) : ofList (x :: xs) = of x * ofList xs := rfl

Equivalence of List Cons and Free Monoid Multiplication

Informal description

For any element $x$ in $\alpha$ and any list $xs$ of elements in $\alpha$, the equivalence $\text{ofList}$ maps the cons operation $x :: xs$ to the product of the singleton list $[x]$ and $\text{ofList}(xs)$ in the free monoid $\text{FreeMonoid}(\alpha)$. That is, \[ \text{ofList}(x :: xs) = \text{of}(x) \cdot \text{ofList}(xs). \]

FreeMonoid.toList_of_mul theorem

(x : α) (xs : FreeMonoid α) : toList (of x * xs) = x :: toList xs

Full source

@[to_additive]
theorem toList_of_mul (x : α) (xs : FreeMonoid α) : toList (of x * xs) = x :: toList xs := rfl

List Representation of Free Monoid Multiplication: $\text{toList}([x] \cdot xs) = x :: \text{toList}(xs)$

Informal description

For any element $x \in \alpha$ and any element $xs$ of the free monoid over $\alpha$, the list representation of the product $\text{of}(x) \cdot xs$ is equal to the list obtained by prepending $x$ to the list representation of $xs$. In other words, the equivalence $\text{toList} : \text{FreeMonoid}(\alpha) \simeq \text{List}(\alpha)$ satisfies $\text{toList}([x] \cdot xs) = x :: \text{toList}(xs)$.

FreeMonoid.of_injective theorem

: Function.Injective (@of α)

Full source

@[to_additive]
theorem of_injective : Function.Injective (@of α) := List.singleton_injective

Injectivity of the Free Monoid Embedding

Informal description

The canonical embedding $\text{FreeMonoid.of} : \alpha \to \text{FreeMonoid}(\alpha)$, which maps each element $x \in \alpha$ to the singleton list $[x]$, is injective. That is, for any $x, y \in \alpha$, if $[x] = [y]$, then $x = y$.

FreeMonoid.length definition

(a : FreeMonoid α) : ℕ

Full source

/-- The length of a free monoid element: 1.length = 0 and (a * b).length = a.length + b.length -/
@[to_additive "The length of an additive free monoid element: 1.length = 0 and (a + b).length =
  a.length + b.length"]
def length (a : FreeMonoid α) : ℕ := a.toList.length

Length in free monoid

Informal description

The length of an element $a$ in the free monoid over $\alpha$ is defined as the length of the corresponding list under the canonical equivalence between $\text{FreeMonoid}(\alpha)$ and $\text{List}(\alpha)$. Specifically: - The length of the identity element (empty list) is $0$ - The length of a product $a * b$ is the sum of the lengths of $a$ and $b$

FreeMonoid.length_one theorem

: length (1 : FreeMonoid α) = 0

Full source

@[to_additive (attr := simp)]
theorem length_one : length (1 : FreeMonoid α) = 0 := rfl

Length of Identity in Free Monoid is Zero

Informal description

The length of the identity element $1$ in the free monoid over $\alpha$ is $0$.

FreeMonoid.length_eq_zero theorem

: length a = 0 ↔ a = 1

Full source

@[to_additive (attr := simp)]
theorem length_eq_zero : lengthlength a = 0 ↔ a = 1 := List.length_eq_zero_iff

Zero Length Characterization in Free Monoid: $\text{length}(a) = 0 \leftrightarrow a = 1$

Informal description

For any element $a$ of the free monoid over an alphabet $\alpha$, the length of $a$ is zero if and only if $a$ is the identity element (empty list) of the monoid.

FreeMonoid.length_of theorem

(m : α) : length (of m) = 1

Full source

@[to_additive (attr := simp)]
theorem length_of (m : α) : length (of m) = 1 := rfl

Length of singleton in free monoid is one

Informal description

For any element $m$ in the alphabet $\alpha$, the length of the free monoid element $\text{FreeMonoid.of}(m)$ is equal to $1$.

FreeMonoid.length_eq_one theorem

: length a = 1 ↔ ∃ m, a = FreeMonoid.of m

Full source

@[to_additive FreeAddMonoid.length_eq_one]
theorem length_eq_one : lengthlength a = 1 ↔ ∃ m, a = FreeMonoid.of m :=
  List.length_eq_one_iff

Characterization of Length-One Elements in Free Monoid: $\text{length}(a) = 1 \leftrightarrow \exists m, a = [m]$

Informal description

For any element $a$ in the free monoid over $\alpha$, the length of $a$ is equal to 1 if and only if there exists an element $m \in \alpha$ such that $a$ is the singleton list $[m]$, i.e., $a = \text{FreeMonoid.of}(m)$.

FreeMonoid.length_eq_two theorem

{v : FreeMonoid α} : v.length = 2 ↔ ∃ c d, v = FreeMonoid.of c * FreeMonoid.of d

Full source

@[to_additive]
theorem length_eq_two {v : FreeMonoid α} :
    v.length = 2 ↔ ∃ c d, v = FreeMonoid.of c * FreeMonoid.of d := List.length_eq_two

Characterization of Length 2 Elements in Free Monoid: $\text{length}(v) = 2 \leftrightarrow \exists c d, v = [c, d]$

Informal description

For any element $v$ in the free monoid over $\alpha$, the length of $v$ is equal to 2 if and only if there exist elements $c, d \in \alpha$ such that $v$ is equal to the product of the singleton lists $[c]$ and $[d]$, i.e., $v = [c] * [d] = [c, d]$.

FreeMonoid.length_eq_three theorem

{v : FreeMonoid α} : v.length = 3 ↔ ∃ (a b c : α), v = of a * of b * of c

Full source

@[to_additive]
theorem length_eq_three {v : FreeMonoid α} : v.length = 3 ↔ ∃ (a b c : α), v = of a * of b * of c :=
  List.length_eq_three

Characterization of Length-3 Elements in Free Monoid: $\text{length}(v) = 3 \leftrightarrow \exists a b c, v = [a] \cdot [b] \cdot [c]$

Informal description

For any element $v$ in the free monoid over $\alpha$, the length of $v$ is equal to 3 if and only if there exist elements $a, b, c \in \alpha$ such that $v$ can be expressed as the product of the singleton embeddings of $a$, $b$, and $c$, i.e., $v = [a] \cdot [b] \cdot [c]$.

FreeMonoid.length_mul theorem

(a b : FreeMonoid α) : (a * b).length = a.length + b.length

Full source

@[to_additive (attr := simp)]
theorem length_mul (a b : FreeMonoid α) : (a * b).length = a.length + b.length :=
  List.length_append

Length is Additive under Free Monoid Multiplication

Informal description

For any elements $a$ and $b$ in the free monoid over an alphabet $\alpha$, the length of their product $a \cdot b$ is equal to the sum of their lengths, i.e., $\text{length}(a \cdot b) = \text{length}(a) + \text{length}(b)$.

FreeMonoid.of_ne_one theorem

(a : α) : of a ≠ 1

Full source

@[to_additive (attr := simp)]
theorem of_ne_one (a : α) : ofof a ≠ 1 := by
  intro h
  have := congrArg FreeMonoid.length h
  simp only [length_of, length_one, Nat.succ_ne_self] at this

Non-identity of singleton embedding in free monoid

Informal description

For any element $a$ of type $\alpha$, the embedding $\text{FreeMonoid.of}(a)$ into the free monoid over $\alpha$ is not equal to the identity element $1$ of the monoid.

FreeMonoid.one_ne_of theorem

(a : α) : 1 ≠ of a

Full source

@[to_additive (attr := simp)]
theorem one_ne_of (a : α) : 1 ≠ of a := of_ne_one _ |>.symm

Identity Element is Not a Singleton in Free Monoid

Informal description

For any element $a$ of type $\alpha$, the identity element $1$ of the free monoid $\text{FreeMonoid}(\alpha)$ is not equal to the singleton embedding $\text{FreeMonoid.of}(a) = [a]$.

FreeMonoid.mem definition

(a : FreeMonoid α) (m : α)

Full source

/-- Membership in a free monoid element -/
@[to_additive "Membership in a free monoid element"]
def mem (a : FreeMonoid α) (m : α) := m ∈ toList a

Membership in free monoid elements

Informal description

The membership relation `m ∈ a` for an element `m` of type `α` in a free monoid element `a : FreeMonoid α` is defined as membership in the underlying list representation of `a`.

FreeMonoid.instMembership instance

: Membership α (FreeMonoid α)

Full source

@[to_additive]
instance : Membership α (FreeMonoid α) := ⟨mem⟩

Membership Relation in the Free Monoid

Informal description

For any type $\alpha$, the free monoid $\text{FreeMonoid}(\alpha)$ has a membership relation where an element $m \in \alpha$ is considered to belong to a free monoid element $a \in \text{FreeMonoid}(\alpha)$ if $m$ appears in the underlying list representation of $a$.

FreeMonoid.not_mem_one theorem

: ¬m ∈ (1 : FreeMonoid α)

Full source

@[to_additive]
theorem not_mem_one : ¬ m ∈ (1 : FreeMonoid α) := List.not_mem_nil

Non-membership in the identity of the free monoid: $m \notin 1$

Informal description

For any element $m$ of type $\alpha$, $m$ does not belong to the identity element $1$ of the free monoid $\text{FreeMonoid}(\alpha)$. Here, $1$ represents the empty list.

FreeMonoid.mem_of theorem

{n : α} : m ∈ of n ↔ m = n

Full source

@[to_additive (attr := simp)]
theorem mem_of {n : α} : m ∈ of nm ∈ of n ↔ m = n := List.mem_singleton

Membership in Singleton Free Monoid: $m \in [n] \leftrightarrow m = n$

Informal description

For any elements $m$ and $n$ of type $\alpha$, the element $m$ belongs to the singleton list $[n]$ (represented as $\text{FreeMonoid.of}(n)$) if and only if $m = n$.

FreeMonoid.mem_of_self theorem

: m ∈ of m

Full source

@[to_additive]
theorem mem_of_self : m ∈ of m := List.mem_singleton_self _

Self-membership in the free monoid embedding: $m \in [m]$

Informal description

For any element $m$ of type $\alpha$, the singleton list $[m]$ (represented as $\text{FreeMonoid.of}(m)$) contains $m$ as an element. In other words, $m \in [m]$.

FreeMonoid.mem_mul theorem

{a b : FreeMonoid α} : m ∈ (a * b) ↔ m ∈ a ∨ m ∈ b

Full source

@[to_additive (attr := simp)]
theorem mem_mul {a b : FreeMonoid α} : m ∈ (a * b)m ∈ (a * b) ↔ m ∈ a ∨ m ∈ b := List.mem_append

Membership in Product of Free Monoid Elements: $m \in a \cdot b \leftrightarrow m \in a \lor m \in b$

Informal description

For any element $m$ in the alphabet $\alpha$ and any two elements $a, b$ of the free monoid $\text{FreeMonoid}(\alpha)$, the element $m$ belongs to the product $a \cdot b$ if and only if $m$ belongs to $a$ or $m$ belongs to $b$.

FreeMonoid.recOn definition

{C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) : C xs

Full source

/-- Recursor for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of `[]` and `x :: xs`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator)
  "Recursor for `FreeAddMonoid` using `0` and
  FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
-- Porting note: change from `List.recOn` to `List.rec` since only the latter is computable
def recOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
    (ih : ∀ x xs, C xs → C (of x * xs)) : C xs := List.rec h0 ih xs

Recursor for free monoid

Informal description

The recursor for the free monoid $\text{FreeMonoid}(\alpha)$, defined by induction on the list structure. For any predicate $C$ on $\text{FreeMonoid}(\alpha)$, to prove $C(xs)$ for all $xs \in \text{FreeMonoid}(\alpha)$, it suffices to: 1. Prove the base case $C(1)$ (where $1$ is the empty list), and 2. For any $x \in \alpha$ and $xs \in \text{FreeMonoid}(\alpha)$, show that $C(xs)$ implies $C(\text{FreeMonoid.of}(x) \cdot xs)$ (where $\cdot$ is list concatenation). This is equivalent to the standard list recursor but expressed in terms of the monoid operations.

FreeMonoid.recOn_one theorem

{C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) : @recOn α C 1 h0 ih = h0

Full source

@[to_additive (attr := simp)]
theorem recOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) :
    @recOn α C 1 h0 ih = h0 := rfl

Recursor Identity for Empty List in Free Monoid

Informal description

For any predicate $C$ on the free monoid $\text{FreeMonoid}(\alpha)$, the recursor $\text{recOn}$ applied to the identity element $1$ (the empty list) with base case proof $h_0 : C(1)$ and inductive step $\text{ih}$ satisfies $\text{recOn}(1, h_0, \text{ih}) = h_0$.

FreeMonoid.recOn_of_mul theorem

 {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C xs → C (of x * xs)) :
  @recOn α C (of x * xs) h0 ih = ih x xs (recOn xs h0 ih)

Full source

@[to_additive (attr := simp)]
theorem recOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
    (ih : ∀ x xs, C xs → C (of x * xs)) : @recOn α C (of x * xs) h0 ih = ih x xs (recOn xs h0 ih) :=
  rfl

Recursion Step for Free Monoid Multiplication

Informal description

Let $\alpha$ be a type and $C : \text{FreeMonoid}(\alpha) \to \text{Sort}^*$ be a predicate on the free monoid over $\alpha$. For any $x \in \alpha$ and $xs \in \text{FreeMonoid}(\alpha)$, given a base case proof $h_0 : C(1)$ and an inductive step function $ih : \forall y\ ys, C(ys) \to C(\text{FreeMonoid.of}(y) \cdot ys)$, the recursive computation on $\text{FreeMonoid.of}(x) \cdot xs$ satisfies: \[ \text{recOn}\ (\text{FreeMonoid.of}(x) \cdot xs)\ h_0\ ih = ih\ x\ xs\ (\text{recOn}\ xs\ h_0\ ih) \]

FreeMonoid.inductionOn theorem

 {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1) (of : ∀ (x : α), C (FreeMonoid.of x))
  (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) : C z

Full source

/-- An induction principle on free monoids, with cases for `1`, `FreeMonoid.of` and `*`. -/
@[to_additive (attr := elab_as_elim, induction_eliminator)
"An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`."]
protected theorem inductionOn {C : FreeMonoid α → Prop} (z : FreeMonoid α) (one : C 1)
    (of : ∀ (x : α), C (FreeMonoid.of x)) (mul : ∀ (x y : FreeMonoid α), C x → C y → C (x * y)) :
  C z := List.rec one (fun _ _ ih => mul [_] _ (of _) ih) z

Induction Principle for Free Monoids

Informal description

Let $C$ be a predicate on the free monoid $\text{FreeMonoid}(\alpha)$. To prove that $C(z)$ holds for all $z \in \text{FreeMonoid}(\alpha)$, it suffices to show: 1. Base case: $C(1)$ holds (where $1$ is the empty list). 2. Singleton case: For any $x \in \alpha$, $C([x])$ holds (where $[x]$ is the singleton list). 3. Multiplication case: For any $x, y \in \text{FreeMonoid}(\alpha)$, if $C(x)$ and $C(y)$ hold, then $C(x \cdot y)$ holds (where $\cdot$ is list concatenation).

FreeMonoid.inductionOn' theorem

 {p : FreeMonoid α → Prop} (a : FreeMonoid α) (one : p (1 : FreeMonoid α)) (mul_of : ∀ b a, p a → p (of b * a)) : p a

Full source

/-- An induction principle for free monoids which mirrors induction on lists, with cases analogous
to the empty list and cons -/
@[to_additive (attr := elab_as_elim) "An induction principle for free monoids which mirrors
induction on lists, with cases analogous to the empty list and cons"]
protected theorem inductionOn' {p : FreeMonoid α → Prop} (a : FreeMonoid α)
    (one : p (1 : FreeMonoid α)) (mul_of : ∀ b a, p a → p (of b * a)) : p a :=
  List.rec one (fun _ _ tail_ih => mul_of _ _ tail_ih) a

Induction Principle for Free Monoids via Singleton Multiplication

Informal description

Let $\alpha$ be a type, and let $p : \text{FreeMonoid}(\alpha) \to \text{Prop}$ be a predicate on the free monoid over $\alpha$. For any element $a \in \text{FreeMonoid}(\alpha)$, if: 1. $p$ holds for the identity element $1$, and 2. For any $b \in \alpha$ and any $a' \in \text{FreeMonoid}(\alpha)$, if $p(a')$ holds, then $p(\text{FreeMonoid.of}(b) \cdot a')$ also holds, then $p(a)$ holds.

FreeMonoid.casesOn definition

{C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) : C xs

Full source

/-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
`[]` and `x :: xs`. -/
@[to_additive (attr := elab_as_elim, cases_eliminator)
  "A version of `List.casesOn` for `FreeAddMonoid` using `0` and
  `FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`."]
def casesOn {C : FreeMonoid α → Sort*} (xs : FreeMonoid α) (h0 : C 1)
    (ih : ∀ x xs, C (of x * xs)) : C xs := List.casesOn xs h0 ih

Case analysis for the free monoid

Informal description

Given a type `α`, the function `FreeMonoid.casesOn` is a case analysis principle for the free monoid over `α`. For any property `C` depending on elements of the free monoid, to prove `C` holds for all `xs : FreeMonoid α`, it suffices to: 1. Show `C` holds for the identity element `1` (the empty list), and 2. For any `x : α` and `xs : FreeMonoid α`, show that `C` holds for the product `of x * xs` (the list `x :: xs`). This is equivalent to the standard list case analysis but phrased in terms of the free monoid operations.

FreeMonoid.casesOn_one theorem

{C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) : @casesOn α C 1 h0 ih = h0

Full source

@[to_additive (attr := simp)]
theorem casesOn_one {C : FreeMonoid α → Sort*} (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) :
    @casesOn α C 1 h0 ih = h0 := rfl

Case Analysis on Identity in Free Monoid Yields Base Case

Informal description

For any property $C$ defined on the free monoid $\text{FreeMonoid}(\alpha)$, if $h_0$ is a proof that $C$ holds for the identity element $1$ (the empty list), and $ih$ is a proof that for any $x \in \alpha$ and $xs \in \text{FreeMonoid}(\alpha)$, $C$ holds for the product $\text{FreeMonoid.of}(x) \cdot xs$ (the list $x :: xs$), then applying the case analysis principle $\text{FreeMonoid.casesOn}$ to $1$ with these arguments yields $h_0$.

FreeMonoid.casesOn_of_mul theorem

 {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1) (ih : ∀ x xs, C (of x * xs)) :
  @casesOn α C (of x * xs) h0 ih = ih x xs

Full source

@[to_additive (attr := simp)]
theorem casesOn_of_mul {C : FreeMonoid α → Sort*} (x : α) (xs : FreeMonoid α) (h0 : C 1)
    (ih : ∀ x xs, C (of x * xs)) : @casesOn α C (of x * xs) h0 ih = ih x xs := rfl

Case Analysis Reduction for Free Monoid Multiplication

Informal description

For any property $C$ depending on elements of the free monoid $\text{FreeMonoid}(\alpha)$, given an element $x \in \alpha$ and $xs \in \text{FreeMonoid}(\alpha)$, the case analysis of the product $\text{FreeMonoid.of}(x) \cdot xs$ under $C$ reduces to applying the inductive hypothesis $ih$ to $x$ and $xs$. That is, evaluating $C$ on $\text{FreeMonoid.of}(x) \cdot xs$ via $\text{casesOn}$ with base case $h_0$ and inductive step $ih$ yields exactly $ih(x, xs)$.

FreeMonoid.hom_eq theorem

⦃f g : FreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g

Full source

@[to_additive (attr := ext)]
theorem hom_eq ⦃f g : FreeMonoidFreeMonoid α →* M⦄ (h : ∀ x, f (of x) = g (of x)) : f = g :=
  MonoidHom.ext fun l ↦ recOn l (f.map_one.trans g.map_one.symm)
    (fun x xs hxs ↦ by simp only [h, hxs, MonoidHom.map_mul])

Uniqueness of Monoid Homomorphisms from Free Monoid via Generators

Informal description

Let $M$ be a monoid and let $f, g \colon \text{FreeMonoid}(\alpha) \to M$ be monoid homomorphisms. If $f([x]) = g([x])$ for every $x \in \alpha$, then $f = g$.

FreeMonoid.prodAux definition

{M} [Monoid M] : List M → M

Full source

/-- A variant of `List.prod` that has `[x].prod = x` true definitionally.
The purpose is to make `FreeMonoid.lift_eval_of` true by `rfl`. -/
@[to_additive "A variant of `List.sum` that has `[x].sum = x` true definitionally.
The purpose is to make `FreeAddMonoid.lift_eval_of` true by `rfl`."]
def prodAux {M} [Monoid M] : List M → M
  | [] => 1
  | (x :: xs) => List.foldl (· * ·) x xs

Monoid product of a list (auxiliary definition)

Informal description

Given a monoid $M$, the function `FreeMonoid.prodAux` maps a list of elements in $M$ to their product, defined recursively as follows: - The empty list maps to the identity element $1$. - For a non-empty list `x :: xs`, the product is computed by left-folding the multiplication operation over the list starting with `x`. This definition ensures that the product of a singleton list `[x]` is exactly `x` (true definitionally), which is used to make certain properties hold by reflexivity.

FreeMonoid.prodAux_eq theorem

: ∀ l : List M, FreeMonoid.prodAux l = l.prod

Full source

@[to_additive]
lemma prodAux_eq : ∀ l : List M, FreeMonoid.prodAux l = l.prod
  | [] => rfl
  | (_ :: xs) => by simp [prodAux, List.prod_eq_foldl]

Equality of Auxiliary Product and List Product in Free Monoid

Informal description

For any list $l$ of elements in a monoid $M$, the auxiliary product function `FreeMonoid.prodAux` applied to $l$ is equal to the product of the elements in $l$ computed via `List.prod`, i.e., $\text{FreeMonoid.prodAux}(l) = \text{List.prod}(l)$.

FreeMonoid.lift definition

: (α → M) ≃ (FreeMonoid α →* M)

Full source

/-- Equivalence between maps `α → M` and monoid homomorphisms `FreeMonoid α →* M`. -/
@[to_additive "Equivalence between maps `α → A` and additive monoid homomorphisms
`FreeAddMonoid α →+ A`."]
def lift : (α → M) ≃ (FreeMonoid α →* M) where
  toFun f :=
  { toFun := fun l ↦ prodAux ((toList l).map f)
    map_one' := rfl
    map_mul' := fun _ _ ↦ by simp only [prodAux_eq, toList_mul, List.map_append, List.prod_append] }
  invFun f x := f (of x)
  left_inv _ := rfl
  right_inv _ := hom_eq fun _ ↦ rfl

Universal property of the free monoid

Informal description

The equivalence $\text{FreeMonoid.lift}$ establishes a natural bijection between functions $\alpha \to M$ and monoid homomorphisms $\text{FreeMonoid}(\alpha) \to^* M$. Specifically: 1. Given a function $f \colon \alpha \to M$, the corresponding monoid homomorphism $\text{FreeMonoid.lift}(f) \colon \text{FreeMonoid}(\alpha) \to^* M$ maps a list $[x_1, \dots, x_n]$ to the product $f(x_1) \cdots f(x_n)$ in $M$. 2. Conversely, given a monoid homomorphism $g \colon \text{FreeMonoid}(\alpha) \to^* M$, the corresponding function $\text{FreeMonoid.lift}^{-1}(g) \colon \alpha \to M$ is obtained by precomposing $g$ with the embedding $\text{FreeMonoid.of} \colon \alpha \to \text{FreeMonoid}(\alpha)$. This equivalence satisfies the universal property of the free monoid: for any monoid $M$, the map $\text{FreeMonoid.lift}$ provides a natural isomorphism between the functors $\alpha \to M$ and $\text{FreeMonoid}(\alpha) \to^* M$.

FreeMonoid.lift_ofList theorem

(f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod

Full source

@[to_additive (attr := simp)]
theorem lift_ofList (f : α → M) (l : List α) : lift f (ofList l) = (l.map f).prod :=
  prodAux_eq _

Universal Property of Free Monoid: $\text{lift}(f)(\text{ofList}(l)) = \prod_{x \in l} f(x)$

Informal description

For any function $f \colon \alpha \to M$ and any list $l$ of elements in $\alpha$, the monoid homomorphism $\text{lift}(f)$ applied to the free monoid element corresponding to $l$ equals the product of the elements obtained by applying $f$ to each element of $l$, i.e., \[ \text{lift}(f)(\text{ofList}(l)) = \prod_{x \in l} f(x). \]

FreeMonoid.lift_symm_apply theorem

(f : FreeMonoid α →* M) : lift.symm f = f ∘ of

Full source

@[to_additive (attr := simp)]
theorem lift_symm_apply (f : FreeMonoidFreeMonoid α →* M) : lift.symm f = f ∘ of := rfl

Inverse of the Free Monoid Lifting Map is Composition with Embedding

Informal description

For any monoid homomorphism $f \colon \text{FreeMonoid}(\alpha) \to^* M$, the inverse of the universal lifting map $\text{FreeMonoid.lift}^{-1}(f)$ is equal to the composition of $f$ with the embedding $\text{FreeMonoid.of} \colon \alpha \to \text{FreeMonoid}(\alpha)$. In other words, $\text{FreeMonoid.lift}^{-1}(f) = f \circ \text{FreeMonoid.of}$.

FreeMonoid.lift_apply theorem

(f : α → M) (l : FreeMonoid α) : lift f l = ((toList l).map f).prod

Full source

@[to_additive]
theorem lift_apply (f : α → M) (l : FreeMonoid α) : lift f l = ((toList l).map f).prod :=
  prodAux_eq _

Evaluation of the Free Monoid Lift Homomorphism

Informal description

For any function $f \colon \alpha \to M$ and any element $l$ of the free monoid $\text{FreeMonoid}(\alpha)$, the monoid homomorphism $\text{lift}(f)$ evaluated at $l$ is equal to the product of the list obtained by applying $f$ to each element of the list representation of $l$, i.e., \[ \text{lift}(f)(l) = \prod_{x \in \text{toList}(l)} f(x). \]

FreeMonoid.lift_comp_of theorem

(f : α → M) : lift f ∘ of = f

Full source

@[to_additive]
theorem lift_comp_of (f : α → M) : liftlift f ∘ of = f := rfl

Composition of Free Monoid Lift with Embedding Equals Original Function

Informal description

For any function $f \colon \alpha \to M$ from a type $\alpha$ to a monoid $M$, the composition of the monoid homomorphism $\text{FreeMonoid.lift}(f) \colon \text{FreeMonoid}(\alpha) \to M$ with the embedding $\text{FreeMonoid.of} \colon \alpha \to \text{FreeMonoid}(\alpha)$ equals $f$. That is, $\text{FreeMonoid.lift}(f) \circ \text{FreeMonoid.of} = f$.

FreeMonoid.lift_eval_of theorem

(f : α → M) (x : α) : lift f (of x) = f x

Full source

@[to_additive (attr := simp)]
theorem lift_eval_of (f : α → M) (x : α) : lift f (of x) = f x := rfl

Evaluation of Lifted Function on Singleton in Free Monoid

Informal description

For any function $f \colon \alpha \to M$ and any element $x \in \alpha$, the monoid homomorphism $\text{FreeMonoid.lift}(f)$ evaluated at the singleton list $[x]$ (i.e., $\text{FreeMonoid.of}(x)$) equals $f(x)$.

FreeMonoid.lift_restrict theorem

(f : FreeMonoid α →* M) : lift (f ∘ of) = f

Full source

@[to_additive (attr := simp)]
theorem lift_restrict (f : FreeMonoidFreeMonoid α →* M) : lift (f ∘ of) = f := lift.apply_symm_apply f

Lifting Restriction Property of the Free Monoid

Informal description

For any monoid homomorphism $f \colon \text{FreeMonoid}(\alpha) \to^* M$, the homomorphism obtained by lifting the composition of $f$ with the embedding $\text{FreeMonoid.of} \colon \alpha \to \text{FreeMonoid}(\alpha)$ is equal to $f$ itself. That is, $\text{lift}(f \circ \text{of}) = f$.

FreeMonoid.comp_lift theorem

(g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f)

Full source

@[to_additive]
theorem comp_lift (g : M →* N) (f : α → M) : g.comp (lift f) = lift (g ∘ f) := by
  ext
  simp

Compatibility of Monoid Homomorphism Composition with Free Monoid Lifting

Informal description

For any monoid homomorphism $g \colon M \to^* N$ and any function $f \colon \alpha \to M$, the composition of $g$ with the monoid homomorphism $\text{lift}(f) \colon \text{FreeMonoid}(\alpha) \to^* M$ is equal to the monoid homomorphism obtained by lifting the composition $g \circ f \colon \alpha \to N$ to $\text{FreeMonoid}(\alpha) \to^* N$. That is, $g \circ \text{lift}(f) = \text{lift}(g \circ f)$.

FreeMonoid.hom_map_lift theorem

(g : M →* N) (f : α → M) (x : FreeMonoid α) : g (lift f x) = lift (g ∘ f) x

Full source

@[to_additive]
theorem hom_map_lift (g : M →* N) (f : α → M) (x : FreeMonoid α) : g (lift f x) = lift (g ∘ f) x :=
  DFunLike.ext_iff.1 (comp_lift g f) x

Naturality of Free Monoid Lifting with Respect to Monoid Homomorphisms

Informal description

For any monoid homomorphism $g \colon M \to^* N$, any function $f \colon \alpha \to M$, and any element $x \in \text{FreeMonoid}(\alpha)$, the homomorphism $g$ applied to the lift of $f$ evaluated at $x$ equals the lift of the composition $g \circ f$ evaluated at $x$. That is, \[ g(\text{lift}(f)(x)) = \text{lift}(g \circ f)(x). \]

FreeMonoid.mkMulAction definition

(f : α → β → β) : MulAction (FreeMonoid α) β

Full source

/-- Define a multiplicative action of `FreeMonoid α` on `β`. -/
@[to_additive "Define an additive action of `FreeAddMonoid α` on `β`."]
def mkMulAction (f : α → β → β) : MulAction (FreeMonoid α) β where
  smul l b := l.toList.foldr f b
  one_smul _ := rfl
  mul_smul _ _ _ := List.foldr_append

Multiplicative Action Induced by Folding

Informal description

Given a function $ f : \alpha \to \beta \to \beta $, this defines a multiplicative action of the free monoid $\text{FreeMonoid}(\alpha)$ on $\beta$, where the action of a word $ l \in \text{FreeMonoid}(\alpha) $ on an element $ b \in \beta $ is given by folding $ f $ over the list representation of $ l $ starting from $ b $. Specifically, for a word $ l = [x_1, \dots, x_n] $ and $ b \in \beta $, the action is defined as: \[ l \cdot b = f(x_1, f(x_2, \dots f(x_n, b) \dots )) \] This action satisfies the multiplicative action axioms: 1. The empty word acts as the identity: $ 1 \cdot b = b $. 2. The action is compatible with concatenation: $ (l_1 \cdot l_2) \cdot b = l_1 \cdot (l_2 \cdot b) $.

FreeMonoid.smul_def theorem

 (f : α → β → β) (l : FreeMonoid α) (b : β) :
  haveI := mkMulAction f
  l • b = l.toList.foldr f b

Full source

@[to_additive]
theorem smul_def (f : α → β → β) (l : FreeMonoid α) (b : β) :
    haveI := mkMulAction f
    l • b = l.toList.foldr f b := rfl

Multiplicative Action as Right Fold in Free Monoid

Informal description

Given a function $f : \alpha \to \beta \to \beta$, a word $l \in \text{FreeMonoid}(\alpha)$, and an element $b \in \beta$, the multiplicative action of $l$ on $b$ is equal to the right fold of $f$ over the list representation of $l$ starting from $b$. That is: \[ l \cdot b = \text{foldr}(f, b, \text{toList}(l)) \]

FreeMonoid.ofList_smul theorem

 (f : α → β → β) (l : List α) (b : β) :
  haveI := mkMulAction f
  ofList l • b = l.foldr f b

Full source

@[to_additive]
theorem ofList_smul (f : α → β → β) (l : List α) (b : β) :
    haveI := mkMulAction f
    ofList l • b = l.foldr f b := rfl

Action of Free Monoid via List Folding

Informal description

Given a function $f \colon \alpha \to \beta \to \beta$ and a list $l \in \text{List}(\alpha)$, the action of the free monoid element corresponding to $l$ on $b \in \beta$ is equal to the right fold of $f$ over $l$ starting from $b$. That is, \[ \text{ofList}(l) \cdot b = \text{foldr}(f, b, l). \]

FreeMonoid.of_smul theorem

 (f : α → β → β) (x : α) (y : β) :
  (haveI := mkMulAction f
    of x • y) =
    f x y

Full source

@[to_additive (attr := simp)]
theorem of_smul (f : α → β → β) (x : α) (y : β) :
    (haveI := mkMulAction f
    of x • y) = f x y := rfl

Action of Singleton List in Free Monoid: $[x] \cdot y = f(x, y)$

Informal description

Given a function $f \colon \alpha \to \beta \to \beta$, the multiplicative action of the singleton list $[x] \in \text{FreeMonoid}(\alpha)$ on an element $y \in \beta$ is given by $f(x, y)$. That is, under the multiplicative action induced by $f$, we have $[x] \cdot y = f(x, y)$.

FreeMonoid.map definition

(f : α → β) : FreeMonoid α →* FreeMonoid β

Full source

/-- The unique monoid homomorphism `FreeMonoid α →* FreeMonoid β` that sends
each `of x` to `of (f x)`. -/
@[to_additive "The unique additive monoid homomorphism `FreeAddMonoid α →+ FreeAddMonoid β`
that sends each `of x` to `of (f x)`."]
def map (f : α → β) : FreeMonoidFreeMonoid α →* FreeMonoid β where
  toFun l := ofList <| l.toList.map f
  map_one' := rfl
  map_mul' _ _ := List.map_append

Induced homomorphism on free monoids by a function

Informal description

Given a function $ f \colon \alpha \to \beta $, the monoid homomorphism $ \text{FreeMonoid.map}(f) \colon \text{FreeMonoid}(\alpha) \to \text{FreeMonoid}(\beta) $ is the unique homomorphism that sends each generator $ \text{of}(x) $ (the singleton list $[x]$) to $ \text{of}(f(x)) $ (the singleton list $[f(x)]$). Explicitly, for any list $ [x_1, \dots, x_n] \in \text{FreeMonoid}(\alpha) $, we have: \[ \text{FreeMonoid.map}(f)([x_1, \dots, x_n]) = [f(x_1), \dots, f(x_n)]. \]

FreeMonoid.map_of theorem

(f : α → β) (x : α) : map f (of x) = of (f x)

Full source

@[to_additive (attr := simp)]
theorem map_of (f : α → β) (x : α) : map f (of x) = of (f x) := rfl

Image of Generator under Free Monoid Map: $\text{map}(f)([x]) = [f(x)]$

Informal description

Given a function $f \colon \alpha \to \beta$ and an element $x \in \alpha$, the monoid homomorphism $\text{FreeMonoid.map}(f)$ applied to the singleton list $[x]$ equals the singleton list $[f(x)]$, i.e., \[ \text{FreeMonoid.map}(f)([x]) = [f(x)]. \]

FreeMonoid.mem_map theorem

{m : β} : m ∈ map f a ↔ ∃ n ∈ a, f n = m

Full source

@[to_additive]
theorem mem_map {m : β} : m ∈ map f am ∈ map f a ↔ ∃ n ∈ a, f n = m := List.mem_map

Characterization of Membership in the Image of a Free Monoid Homomorphism

Informal description

For any element $m \in \beta$ and any element $a \in \text{FreeMonoid}(\alpha)$, $m$ is in the image of $a$ under the monoid homomorphism $\text{map}(f) : \text{FreeMonoid}(\alpha) \to \text{FreeMonoid}(\beta)$ if and only if there exists an element $n \in \alpha$ such that $n$ is in $a$ and $f(n) = m$.

FreeMonoid.map_map theorem

{α₁ : Type*} {g : α₁ → α} {x : FreeMonoid α₁} : map f (map g x) = map (f ∘ g) x

Full source

@[to_additive]
theorem map_map {α₁ : Type*} {g : α₁ → α} {x : FreeMonoid α₁} :
    map f (map g x) = map (f ∘ g) x := by
  unfold map
  simp only [MonoidHom.coe_mk, OneHom.coe_mk, toList_ofList, List.map_map]

Composition of Induced Homomorphisms on Free Monoids

Informal description

For any function $g \colon \alpha_1 \to \alpha$ and any element $x$ of the free monoid $\text{FreeMonoid}(\alpha_1)$, the composition of the monoid homomorphisms $\text{map}(f) \circ \text{map}(g)$ applied to $x$ is equal to the monoid homomorphism $\text{map}(f \circ g)$ applied to $x$. In other words, the following diagram commutes: \[ \text{map}(f) \circ \text{map}(g) = \text{map}(f \circ g). \]

FreeMonoid.toList_map theorem

(f : α → β) (xs : FreeMonoid α) : toList (map f xs) = xs.toList.map f

Full source

@[to_additive (attr := simp)]
theorem toList_map (f : α → β) (xs : FreeMonoid α) : toList (map f xs) = xs.toList.map f := rfl

Commutativity of $\text{toList}$ and $\text{map}$ for Free Monoids

Informal description

For any function $f \colon \alpha \to \beta$ and any element $xs$ of the free monoid $\text{FreeMonoid}(\alpha)$, the list representation of the mapped element $\text{map}(f)(xs)$ is equal to the pointwise application of $f$ to the list representation of $xs$. In other words, if $\text{toList} \colon \text{FreeMonoid}(\alpha) \to \text{List}(\alpha)$ is the canonical bijection between the free monoid and lists, then: \[ \text{toList}(\text{map}(f)(xs)) = \text{List.map}(f)(\text{toList}(xs)). \]

FreeMonoid.ofList_map theorem

(f : α → β) (xs : List α) : ofList (xs.map f) = map f (ofList xs)

Full source

@[to_additive]
theorem ofList_map (f : α → β) (xs : List α) : ofList (xs.map f) = map f (ofList xs) := rfl

Naturality of `ofList` with respect to `map`

Informal description

For any function $f \colon \alpha \to \beta$ and any list $xs$ of elements of $\alpha$, the equivalence `ofList` maps the list obtained by applying $f$ to each element of $xs$ to the same element as the monoid homomorphism `map f` applied to the equivalence `ofList` of $xs$. In other words, the following diagram commutes: \[ \text{ofList}(xs.\text{map}(f)) = \text{map}(f)(\text{ofList}(xs)). \]

FreeMonoid.lift_of_comp_eq_map theorem

(f : α → β) : (lift fun x ↦ of (f x)) = map f

Full source

@[to_additive]
theorem lift_of_comp_eq_map (f : α → β) : (lift fun x ↦ of (f x)) = map f := hom_eq fun _ ↦ rfl

Equality of Lifted Composition and Map for Free Monoids

Informal description

For any function $f \colon \alpha \to \beta$, the monoid homomorphism obtained by lifting the composition of $\text{FreeMonoid.of}$ with $f$ is equal to the homomorphism $\text{FreeMonoid.map}(f)$. In other words, the following diagram commutes: \[ \text{FreeMonoid.lift}(x \mapsto \text{FreeMonoid.of}(f(x))) = \text{FreeMonoid.map}(f). \]

FreeMonoid.map_comp theorem

(g : β → γ) (f : α → β) : map (g ∘ f) = (map g).comp (map f)

Full source

@[to_additive]
theorem map_comp (g : β → γ) (f : α → β) : map (g ∘ f) = (map g).comp (map f) := hom_eq fun _ ↦ rfl

Composition of Induced Homomorphisms on Free Monoids

Informal description

For any functions $f \colon \alpha \to \beta$ and $g \colon \beta \to \gamma$, the monoid homomorphism induced by the composition $g \circ f$ is equal to the composition of the monoid homomorphisms induced by $g$ and $f$ respectively. That is, \[ \text{map}(g \circ f) = \text{map}(g) \circ \text{map}(f). \]

FreeMonoid.map_id theorem

: map (@id α) = MonoidHom.id (FreeMonoid α)

Full source

@[to_additive (attr := simp)]
theorem map_id : map (@id α) = MonoidHom.id (FreeMonoid α) := hom_eq fun _ ↦ rfl

Identity Function Induces Identity Homomorphism on Free Monoid

Informal description

The monoid homomorphism induced by the identity function on $\alpha$ is equal to the identity homomorphism on the free monoid $\text{FreeMonoid}(\alpha)$. That is, \[ \text{map}(\text{id}) = \text{id}. \]

FreeMonoid.map_symm_apply_map_eq theorem

{x : FreeMonoid α} (e : α ≃ β) : (map ⇑e.symm) ((map ⇑e) x) = x

Full source

@[to_additive (attr := simp)]
theorem map_symm_apply_map_eq {x : FreeMonoid α} (e : α ≃ β) :
    (map ⇑e.symm) ((map ⇑e) x) = x := by simp [map_map]

Inverse Homomorphism Cancels Forward Homomorphism in Free Monoid

Informal description

For any element $x$ in the free monoid $\text{FreeMonoid}(\alpha)$ and any equivalence $e : \alpha \simeq \beta$, applying the monoid homomorphism induced by $e$ followed by the monoid homomorphism induced by its inverse $e^{-1}$ returns the original element $x$. That is, \[ \text{map}(e^{-1}) \circ \text{map}(e) (x) = x. \]

FreeMonoid.map_apply_map_symm_eq theorem

{x : FreeMonoid β} (e : α ≃ β) : (map ⇑e) ((map ⇑e.symm) x) = x

Full source

@[to_additive (attr := simp)]
theorem map_apply_map_symm_eq {x : FreeMonoid β} (e : α ≃ β) :
    (map ⇑e) ((map ⇑e.symm) x) = x := by simp [map_map]

Inverse Homomorphism Composition Yields Identity on Free Monoid

Informal description

For any element $x$ in the free monoid $\text{FreeMonoid}(\beta)$ and any equivalence $e : \alpha \simeq \beta$, the composition of the monoid homomorphisms induced by $e$ and its inverse $e^{-1}$ satisfies: \[ \text{map}(e) \circ \text{map}(e^{-1}) (x) = x. \]

FreeMonoid.uniqueUnits instance

: Unique (FreeMonoid α)ˣ

Full source

/-- The only invertible element of the free monoid is 1; this instance enables `units_eq_one`. -/
@[to_additive]
instance uniqueUnits : Unique (FreeMonoid α)ˣ where
  uniq u := Units.ext <| toList.injective <|
    have : toList u.val ++ toList u.inv = [] := DFunLike.congr_arg toList u.val_inv
    (List.append_eq_nil_iff.mp this).1

Triviality of Units in the Free Monoid

Informal description

The group of units of the free monoid $\text{FreeMonoid}(\alpha)$ is trivial, consisting only of the identity element (the empty list). In other words, the only invertible element in the free monoid is the multiplicative identity.

FreeMonoid.map_surjective theorem

{f : α → β} : Function.Surjective (map f) ↔ Function.Surjective f

Full source

@[to_additive (attr := simp)]
theorem map_surjective {f : α → β} : Function.SurjectiveFunction.Surjective (map f) ↔ Function.Surjective f := by
  constructor
  · intro fs d
    rcases fs (FreeMonoid.of d) with ⟨b, hb⟩
    induction' b using FreeMonoid.inductionOn' with head _ _
    · have H := congr_arg length hb
      simp only [length_one, length_of, Nat.zero_ne_one, map_one] at H
    simp only [map_mul, map_of] at hb
    use head
    have H := congr_arg length hb
    simp only [length_mul, length_of, add_eq_left, length_eq_zero] at H
    rw [H, mul_one] at hb
    exact FreeMonoid.of_injective hb
  intro fs d
  induction' d using FreeMonoid.inductionOn' with head tail ih
  · use 1
    rfl
  specialize fs head
  rcases fs with ⟨a, rfl⟩
  rcases ih with ⟨b, rfl⟩
  use FreeMonoid.of a * b
  rfl

Surjectivity of Induced Free Monoid Homomorphism $\text{FreeMonoid.map}(f)$ is Equivalent to Surjectivity of $f$

Informal description

For any function $f \colon \alpha \to \beta$, the induced monoid homomorphism $\text{FreeMonoid.map}(f) \colon \text{FreeMonoid}(\alpha) \to \text{FreeMonoid}(\beta)$ is surjective if and only if $f$ is surjective.

FreeMonoid.reverse definition

: FreeMonoid α → FreeMonoid α

Full source

/-- reverses the symbols in a free monoid element -/
@[to_additive "reverses the symbols in an additive free monoid element"]
def reverse : FreeMonoid α → FreeMonoid α := List.reverse

Reversal of a free monoid word

Informal description

The function that reverses the order of elements in a word (list) of the free monoid over an alphabet $\alpha$. That is, for a word $w = [x_1, x_2, \dots, x_n] \in \text{FreeMonoid}(\alpha)$, we have $\text{reverse}(w) = [x_n, \dots, x_2, x_1]$.

FreeMonoid.reverse_of theorem

(a : α) : reverse (of a) = of a

Full source

@[to_additive (attr := simp)]
theorem reverse_of (a : α) : reverse (of a) = of a := rfl

Reversal of Singleton Word in Free Monoid

Informal description

For any element $a$ in the alphabet $\alpha$, the reversal of the singleton word $[a]$ in the free monoid $\text{FreeMonoid}(\alpha)$ is equal to $[a]$ itself, i.e., $\text{reverse}(\text{of}(a)) = \text{of}(a)$.

FreeMonoid.reverse_mul theorem

{a b : FreeMonoid α} : reverse (a * b) = reverse b * reverse a

Full source

@[to_additive]
theorem reverse_mul {a b : FreeMonoid α} : reverse (a * b) = reverse b * reverse a :=
  List.reverse_append

Reverse of Product in Free Monoid Equals Reverse Product in Opposite Order

Informal description

For any two elements $a$ and $b$ in the free monoid over an alphabet $\alpha$, the reverse of their product equals the product of their reverses in the opposite order, i.e., $\text{reverse}(a \cdot b) = \text{reverse}(b) \cdot \text{reverse}(a)$.

FreeMonoid.reverse_reverse theorem

{a : FreeMonoid α} : reverse (reverse a) = a

Full source

@[to_additive (attr := simp)]
theorem reverse_reverse {a : FreeMonoid α} : reverse (reverse a) = a := by
  apply List.reverse_reverse

Double Reversal of a Free Monoid Word is the Identity

Informal description

For any word $a$ in the free monoid over an alphabet $\alpha$, reversing the word twice returns the original word, i.e., $\text{reverse}(\text{reverse}(a)) = a$.

FreeMonoid.length_reverse theorem

{a : FreeMonoid α} : a.reverse.length = a.length

Full source

@[to_additive (attr := simp)]
theorem length_reverse {a : FreeMonoid α} : a.reverse.length = a.length :=
  List.length_reverse

Length Preservation under Reversal in Free Monoid

Informal description

For any element $a$ in the free monoid over $\alpha$, the length of the reversed element $\text{reverse}(a)$ is equal to the length of $a$, i.e., $\text{length}(\text{reverse}(a)) = \text{length}(a)$.

FreeMonoid.freeMonoidCongr definition

(e : α ≃ β) : FreeMonoid α ≃* FreeMonoid β

Full source

/-- free monoids over isomorphic types are isomorphic -/
@[to_additive "if two types are isomorphic, the additive free monoids over those types are
isomorphic"]
def freeMonoidCongr (e : α ≃ β) :  FreeMonoidFreeMonoid α ≃* FreeMonoid β where
  toFun := FreeMonoid.map ⇑e
  invFun := FreeMonoid.map ⇑e.symm
  left_inv _ := map_symm_apply_map_eq e
  right_inv _ := map_apply_map_symm_eq e
  map_mul' := by simp [map_mul]

Isomorphism of free monoids induced by a bijection between alphabets

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, the function $\text{freeMonoidCongr}(e)$ is a multiplicative isomorphism between the free monoids $\text{FreeMonoid}(\alpha)$ and $\text{FreeMonoid}(\beta)$. This isomorphism is constructed by: 1. The forward map $\text{FreeMonoid.map}(e)$ which applies $e$ to each element of a list in $\text{FreeMonoid}(\alpha)$ 2. The inverse map $\text{FreeMonoid.map}(e^{-1})$ which applies $e^{-1}$ to each element of a list in $\text{FreeMonoid}(\beta)$ 3. The proof that these maps are mutual inverses 4. The proof that the forward map preserves multiplication Explicitly, for any list $[x_1,\ldots,x_n] \in \text{FreeMonoid}(\alpha)$, we have: \[ \text{freeMonoidCongr}(e)([x_1,\ldots,x_n]) = [e(x_1),\ldots,e(x_n)] \] and similarly for the inverse map.

FreeMonoid.freeMonoidCongr_of theorem

(e : α ≃ β) (a : α) : freeMonoidCongr e (of a) = of (e a)

Full source

@[to_additive (attr := simp)]
theorem freeMonoidCongr_of (e : α ≃ β) (a : α) : freeMonoidCongr e (of a) = of (e a) := rfl

Action of Free Monoid Isomorphism on Singletons

Informal description

Given a bijection $e : \alpha \simeq \beta$ between types $\alpha$ and $\beta$, and an element $a \in \alpha$, the multiplicative isomorphism $\text{freeMonoidCongr}(e)$ maps the singleton list $[a] \in \text{FreeMonoid}(\alpha)$ to the singleton list $[e(a)] \in \text{FreeMonoid}(\beta)$. In other words: \[ \text{freeMonoidCongr}(e)([a]) = [e(a)] \]

FreeMonoid.freeMonoidCongr_symm_of theorem

(e : α ≃ β) (b : β) : freeMonoidCongr e.symm (of b) = of (e.symm b)

Full source

@[to_additive (attr := simp)]
theorem freeMonoidCongr_symm_of (e : α ≃ β) (b : β) :
    freeMonoidCongr e.symm (of b) = of (e.symm b) := rfl

Action of Free Monoid Isomorphism on Singletons via Inverse Bijection

Informal description

Let $e : \alpha \simeq \beta$ be a bijection between types $\alpha$ and $\beta$, and let $b \in \beta$. Then the multiplicative isomorphism $\text{freeMonoidCongr}(e^{-1})$ between free monoids $\text{FreeMonoid}(\beta)$ and $\text{FreeMonoid}(\alpha)$ maps the singleton list $[b] \in \text{FreeMonoid}(\beta)$ to $[e^{-1}(b)] \in \text{FreeMonoid}(\alpha)$. In other words, for the inverse bijection $e^{-1} : \beta \simeq \alpha$, we have: \[ \text{freeMonoidCongr}(e^{-1})([b]) = [e^{-1}(b)] \]

Main definitions