The destutter quotient monoid of a free monoid

For [DecidableEq α], List.destutter (· ≠ ·) collapses each maximal run of equal adjacent elements to one; the lists it fixes are exactly the List.IsChain (· ≠ ·) lists (no two adjacent elements equal). Under append-then-destutter these form a monoid, and List.destutter (· ≠ ·) is the quotient homomorphism out of the free monoid: {l // l.IsChain (· ≠ ·)} ≃* FreeMonoid α ⧸ ker.

Abstractly this is the monoid presented by idempotent generators ⟨α | a · a = a⟩: the defining relations destutterRel make each generator absorb its own repeat, the rewriting system a · a → a is confluent and terminating, and destutter (· ≠ ·) computes its normal forms — the stutter-free words. presentedMonoidEquiv packages this as a MulEquiv PresentedMonoid (destutterRel α) ≃* {l // l.IsChain (· ≠ ·)}, identifying the abstract presentation with the concrete normal-form model.

Main definitions

• Monoid {l : List α // l.IsChain (· ≠ ·)} — the destutter quotient monoid, with multiplication List.destutterConcat (from Core.Data.List.Destutter).
• FreeMonoid.destutterHom — the quotient map FreeMonoid α →* {l // l.IsChain (· ≠ ·)}.
• FreeMonoid.destutterRel — the presentation ⟨α | a · a = a⟩: each generator is idempotent.
• FreeMonoid.destutterQuotientEquiv — first isomorphism FreeMonoid α ⧸ ker ≃* {l // …}.
• FreeMonoid.presentedMonoidEquiv — the concrete model is the presented monoid PresentedMonoid (destutterRel α) ≃* {l // l.IsChain (· ≠ ·)}.
• FreeMonoid.destutterLift — the universal property: the destutter monoid is the free monoid on idempotent generators; any f : α → M with f a * f a = f a extends uniquely (destutterLift_unique) to a monoid hom l ↦ (l.map f).prod.

Implementation notes

The destutter-vs-++ congruence lemmas live in Core.Data.List.Destutter (candidates for Mathlib.Data.List.Destutter); this file adds the monoid/presentation layer (candidate for Mathlib.Algebra.FreeMonoid). The monoid multiplication is associative because destutter (· ≠ ·) is a ++-congruence (destutter_append_left/_right from that file); the presentation is identified with the concrete model by the normalization lemma conGen_destutterRel_destutter. Nothing here is specific to any application; the phonological Obligatory Contour Principle (Phonology.OCP) is one consumer, reading the presentation as autosegmental tier fusion.

The bundled quotient monoid

The multiplication List.destutterConcat (append then destutter) and its List-level laws live in Core.Data.List.Destutter; here they are bundled into the monoid structure.

@[implicit_reducible]

instance List.instMulSubtypeIsChainNe_linglib {α : Type u_1} [DecidableEq α] : Mul { l : List α // IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

Equations

• List.instMulSubtypeIsChainNe_linglib = { mul := fun (a b : { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }) => ⟨(↑a).destutterConcat ↑b, ⋯⟩ }

@[implicit_reducible]

instance List.instOneSubtypeIsChainNe_linglib {α : Type u_1} : One { l : List α // IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

Equations

• List.instOneSubtypeIsChainNe_linglib = { one := ⟨[], ⋯⟩ }

@[simp]

theorem List.coe_mul {α : Type u_1} [DecidableEq α] (a b : { l : List α // IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }) : ↑(a * b) = (↑a).destutterConcat ↑b

@[simp]

theorem List.coe_one {α : Type u_1} : ↑1 = []

@[implicit_reducible]

instance List.instMonoidSubtypeIsChainNe_linglib {α : Type u_1} [DecidableEq α] : Monoid { l : List α // IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

The destutter quotient monoid: destutterConcat multiplication, [] unit.

Equations

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

def FreeMonoid.destutterHom {α : Type u_1} [DecidableEq α] : FreeMonoid α →* { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

The destutter quotient map: send a free-monoid word to its destutter (· ≠ ·) normal form. List.destutter_append_destutter is its map_mul.

Equations

• FreeMonoid.destutterHom = { toFun := fun (l : FreeMonoid α) => ⟨List.destutter (fun (x1 x2 : α) => x1 ≠ x2) (FreeMonoid.toList l), ⋯⟩, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeMonoid.destutterHom_ofList {α : Type u_1} [DecidableEq α] (c : { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }) : destutterHom (ofList ↑c) = c

ofList of a stutter-free list is a right inverse of destutterHom: a chain is its own destutter normal form.

theorem FreeMonoid.destutterHom_surjective {α : Type u_1} [DecidableEq α] : Function.Surjective ⇑destutterHom

def FreeMonoid.destutterCon {α : Type u_1} [DecidableEq α] : Con (FreeMonoid α)

The destutter congruence on the free monoid: the kernel of destutterHom.

Equations

• FreeMonoid.destutterCon = Con.ker FreeMonoid.destutterHom

def FreeMonoid.destutterQuotientEquiv {α : Type u_1} [DecidableEq α] : destutterCon.Quotient ≃* { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

First isomorphism theorem for the destutter quotient: the abstract quotient FreeMonoid α ⧸ ker is the concrete stutter-free model {l // l.IsChain (· ≠ ·)}. Computable: ofList on chains is the right inverse.

Equations

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

The monoid presentation ⟨α | a · a = a⟩

def FreeMonoid.destutterRel (α : Type u_2) : FreeMonoid α → FreeMonoid α → Prop

The defining relations of the destutter monoid: every generator is idempotent (a · a = a). The presented monoid PresentedMonoid (destutterRel α) is ⟨α | a · a = a⟩.

Equations

• FreeMonoid.destutterRel α x y = ∃ (a : α), x = FreeMonoid.of a * FreeMonoid.of a ∧ y = FreeMonoid.of a

theorem FreeMonoid.destutterHom_destutterRel {α : Type u_1} [DecidableEq α] {x y : FreeMonoid α} (h : destutterRel α x y) : destutterHom x = destutterHom y

destutterHom collapses each defining relation: destutter [a, a] = [a].

theorem FreeMonoid.conGen_destutterRel_destutter {α : Type u_1} [DecidableEq α] (l : List α) : (conGen (destutterRel α)) (ofList l) (ofList (List.destutter (fun (x1 x2 : α) => x1 ≠ x2) l))

Normalization: every free-monoid word is congruent, modulo the idempotent-generator relations, to its destutter (· ≠ ·) normal form. The rewriting system a · a → a reduces each word to a stutter-free one.

theorem FreeMonoid.destutterCon_eq_conGen {α : Type u_1} [DecidableEq α] : destutterCon = conGen (destutterRel α)

The destutter congruence is the presentation ⟨α | a · a = a⟩: two words have the same destutter exactly when the idempotent-generator relations identify them.

def FreeMonoid.presentedMonoidEquiv {α : Type u_1} [DecidableEq α] : PresentedMonoid (destutterRel α) ≃* { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }

The concrete stutter-free model is the monoid presented by idempotent generators ⟨α | a · a = a⟩, with destutter (· ≠ ·) computing normal forms.

Equations

• FreeMonoid.presentedMonoidEquiv = (Con.congr ⋯).trans FreeMonoid.destutterQuotientEquiv

Universal property: the free monoid on idempotent generators

theorem FreeMonoid.destutter_map_prod {α : Type u_1} [DecidableEq α] {M : Type u_2} [Monoid M] (f : α → M) (hf : ∀ (a : α), f a * f a = f a) (xs : List α) : (List.map f (List.destutter (fun (x1 x2 : α) => x1 ≠ x2) xs)).prod = (List.map f xs).prod

(· .map f).prod is invariant under destutter (· ≠ ·) when each f a is idempotent: collapsing an adjacent run replaces f a * f a by f a. The engine of destutterLift, read off the normalization lemma conGen_destutterRel_destutter.

def FreeMonoid.destutterLift {α : Type u_1} [DecidableEq α] {M : Type u_2} [Monoid M] (f : α → M) (hf : ∀ (a : α), f a * f a = f a) : { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l } →* M

Universal property — the destutter monoid is the free monoid on idempotent generators: any f : α → M sending each generator to an idempotent element of M extends to the monoid hom l ↦ (l.map f).prod out of the stutter-free model. This realizes PresentedMonoid.lift's universal property for the presentation ⟨α | a · a = a⟩ (via presentedMonoidEquiv) in concrete computable form — the destutter-monoid analogue of FreeMonoid.lift.

Equations

• FreeMonoid.destutterLift f hf = { toFun := fun (l : { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l }) => (List.map f ↑l).prod, map_one' := ⋯, map_mul' := ⋯ }

@[simp]

theorem FreeMonoid.destutterLift_singleton {α : Type u_1} [DecidableEq α] {M : Type u_2} [Monoid M] (f : α → M) (hf : ∀ (a : α), f a * f a = f a) (a : α) : (destutterLift f hf) ⟨[a], ⋯⟩ = f a

theorem FreeMonoid.eq_prod_map_singleton {α : Type u_1} [DecidableEq α] {l : List α} (hl : List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l) : ⟨l, hl⟩ = (List.map (fun (a : α) => ⟨[a], ⋯⟩) l).prod

A stutter-free list is the product of its single-element generators (no fusion occurs, since it is already a chain): the generators generate.

theorem FreeMonoid.destutterLift_unique {α : Type u_1} [DecidableEq α] {M : Type u_2} [Monoid M] (f : α → M) (hf : ∀ (a : α), f a * f a = f a) (g : { l : List α // List.IsChain (fun (x1 x2 : α) => x1 ≠ x2) l } →* M) (hg : ∀ (a : α), g ⟨[a], ⋯⟩ = f a) : g = destutterLift f hf

Uniqueness for the universal property: any monoid hom agreeing with f on the single-autosegment generators is destutterLift f hf.