Wreath products of monoids and semigroup division

• SgDiv S T — semigroup division: S is a homomorphic image of a subsemigroup of T.
• WreathProduct A B X — the wreath product of monoids A and B relative to an action of B on a type X: pairs (f : X → A, b : B) with (p * q).func x = p.func (q.base • x) * q.func x and (p * q).base = p.base * q.base (the lemmas WreathProduct.mul_func / mul_base), with its Monoid and Finite instances. Its monoid is that of the transformation wreath product (A, A) ≀ (X, B).

References

• [Krohn, Rhodes, Algebraic Theory of Machines. I., Trans. AMS 1965]
• [Eilenberg, Automata, Languages, and Machines, Vol. B, 1976]

Semigroup division

def LeanPool.KrohnRhodes.SgDiv (S : Type u_1) (T : Type u_2) [Mul S] [Mul T] : Prop

Semigroup S divides T if S is a homomorphic image of a subsemigroup of T.

Equations

• LeanPool.KrohnRhodes.SgDiv S T = ∃ (U : Subsemigroup T) (φ : ↥U →ₙ* S), Function.Surjective ⇑φ

Wreath product construction

structure LeanPool.KrohnRhodes.WreathProduct (A : Type u) (B : Type v) (X : Type w) [Monoid A] [Monoid B] [MulAction B X] : Type (max (max u v) w)

The wreath product of monoids A and B relative to an action of B on a type X. Elements are pairs (f, b) where f : X → A and b : B.

Multiplication: (f₁, b₁) * (f₂, b₂) = (fun x => f₁ (b₂ • x) * f₂ x, b₁ * b₂)

• func : X → A

  The decoration function mapping each point of X to an element of A.

• base : B

  The bottom component from B.

theorem LeanPool.KrohnRhodes.WreathProduct.ext {A : Type u} {B : Type v} {X : Type w} {inst✝ : Monoid A} {inst✝¹ : Monoid B} {inst✝² : MulAction B X} {x y : WreathProduct A B X} (func : x.func = y.func) (base : x.base = y.base) : x = y

theorem LeanPool.KrohnRhodes.WreathProduct.ext_iff {A : Type u} {B : Type v} {X : Type w} {inst✝ : Monoid A} {inst✝¹ : Monoid B} {inst✝² : MulAction B X} {x y : WreathProduct A B X} : x = y ↔ x.func = y.func ∧ x.base = y.base

@[instance_reducible]

instance LeanPool.KrohnRhodes.WreathProduct.instMul {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] : Mul (WreathProduct A B X)

Multiplication in the wreath product. Convention: (f₁, b₁) * (f₂, b₂) = (x ↦ f₁(b₂ • x) * f₂(x), b₁ * b₂).

This is the standard "left regular" convention where the right factor's base element acts on the left factor's decoration. This convention ensures associativity with a standard left MulAction.

Note: some references use f₁(x) * f₂(b₁⁻¹ • x) (group case) or f₁(x) * f₂(b₁ • x) (right-action convention). Our choice is equivalent up to reversing the action.

Equations

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

@[instance_reducible]

instance LeanPool.KrohnRhodes.WreathProduct.instOne {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] : One (WreathProduct A B X)

The identity element of the wreath product.

Equations

• LeanPool.KrohnRhodes.WreathProduct.instOne = { one := { func := fun (x : X) => 1, base := 1 } }

@[simp]

theorem LeanPool.KrohnRhodes.WreathProduct.mul_func {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] (p q : WreathProduct A B X) (x : X) : (p * q).func x = p.func (q.base • x) * q.func x

@[simp]

theorem LeanPool.KrohnRhodes.WreathProduct.mul_base {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] (p q : WreathProduct A B X) : (p * q).base = p.base * q.base

@[simp]

theorem LeanPool.KrohnRhodes.WreathProduct.one_func {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] (x : X) : func 1 x = 1

@[simp]

theorem LeanPool.KrohnRhodes.WreathProduct.one_base {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] : base 1 = 1

@[instance_reducible]

instance LeanPool.KrohnRhodes.WreathProduct.instMonoid {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] : Monoid (WreathProduct A B X)

The wreath product of monoids is a monoid.

Equations

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

instance LeanPool.KrohnRhodes.WreathProduct.instFinite {A : Type u} {B : Type v} {X : Type w} [Monoid A] [Monoid B] [MulAction B X] [Finite X] [Finite A] [Finite B] : Finite (WreathProduct A B X)

The wreath product of finite types is finite.