Monoid wreath bridge

Bridges Mathlib's group-theoretic RegularWreathProduct D Q to the semigroup-theoretic WreathProduct A B X of WreathProduct.lean.

Mathlib's regular wreath product uses the multiplication (a * b).left x = a.left x * b.left (a.right⁻¹ * x), while WreathProduct uses (p * q).func x = p.func (q.base • x) * q.func x.

When Q acts on itself by left multiplication (Monoid.toMulAction), these two conventions are conjugate via the substitution f ↦ (x ↦ f (q * x)), so we obtain an injective monoid homomorphism D ≀ᵣ Q →* WreathProduct D Q Q.

Main results

• regularWreathToMonoidWreath : the bridge, a monoid homomorphism.
• regularWreathToMonoidWreath_injective : injectivity of the bridge.

def LeanPool.KrohnRhodes.regularWreathToMonoidWreathFun (D Q : Type u) [Group D] [Group Q] (a : D ≀ᵣ Q) : WreathProduct D Q Q

The bridge function on underlying data: send (a, q) ∈ D ≀ᵣ Q to the WreathProduct element with decoration x ↦ a (q * x) and base q.

This change of variable is needed because Mathlib's regular wreath uses b.left (a.right⁻¹ * x) in multiplication while WreathProduct uses p.func (q.base • x); they match precisely after this substitution.

Equations

• LeanPool.KrohnRhodes.regularWreathToMonoidWreathFun D Q a = { func := fun (x : Q) => a.left (a.right * x), base := a.right }

def LeanPool.KrohnRhodes.regularWreathToMonoidWreath (D Q : Type u) [Group D] [Group Q] : D ≀ᵣ Q →* WreathProduct D Q Q

Bridge: a group regular wreath product D ≀ᵣ Q embeds as a monoid into WreathProduct D Q Q, where Q acts on itself by left multiplication.

Equations

• LeanPool.KrohnRhodes.regularWreathToMonoidWreath D Q = { toFun := LeanPool.KrohnRhodes.regularWreathToMonoidWreathFun D Q, map_one' := ⋯, map_mul' := ⋯ }

theorem LeanPool.KrohnRhodes.regularWreathToMonoidWreath_injective (D Q : Type u) [Group D] [Group Q] : Function.Injective ⇑(regularWreathToMonoidWreath D Q)

The bridge is injective.