Krohn–Rhodes factor towers

This file supplies the vocabulary for the aperiodic/simple-group decomposition variant, and the wreath-product algebra used to assemble factor towers.

• KRFactor — a finite monoid together with a witnessed flag: either every element is aperiodic, or the carrier carries a simple group structure whose underlying monoid is the factor's monoid. Constructors KRFactor.ofAperiodic and KRFactor.ofSimpleGroup.
• DivTowerWreath M [F₁, …, Fₖ] — a recursive sequence of wreath divisions. It is defined by recursion on the list: M divides WreathProduct F₁ B Y for some finite monoid B acting on a finite type Y, where B in turn satisfies DivTowerWreath B [F₂, …, Fₖ]; the empty list means M is trivial.
• Wreath-product algebra: associativity up to division (sgDiv_wreath_assoc, via the embedding WreathAssoc.Phi), monotonicity in the decoration (sgDiv_wreath_decoration_mono), the concatenation step divTowerWreath_wreathStep, and divTowerWreath_of_sgDiv (towers pull back along division).
• group_subquotient_faithful_aux — every finite group has a factor tower all of whose factors divide the group; the construction uses only simple groups (induction along a normal subgroup, using the Krasner–Kaloujnine embedding of KrasnerKaloujnine.lean).

References

• [K. Krohn, J. Rhodes, Algebraic Theory of Machines. I. Prime Decomposition Theorem for Finite Semigroups and Machines, Trans. AMS 116 (1965), 450–464]
• [Eilenberg, Automata, Languages, and Machines, Vol. B, 1976]

theorem LeanPool.KrohnRhodes.sgDiv_refl (S : Type u) [Semigroup S] : SgDiv S S

Division is reflexive for semigroups. S divides itself via the identity homomorphism on the whole semigroup.

Factor towers

A factor tower of a finite monoid M is an explicit list of Krohn–Rhodes factors [F₁, …, Fₖ], each flagged and witnessed as aperiodic or simple group, together with a proof of the recursive division predicate DivTowerWreath M [F₁, …, Fₖ]. The intermediate base monoids and their actions are existential witnesses at each step; this file does not identify the tower with a single prescribed transformation wreath product.

• KRFactorKind, KRFactor — the two factor kinds, and one flagged, witnessed factor.
• DivTowerWreath M factors — the recursive division predicate.
• divTowerWreath_wreathStep — concatenation of towers along a wreath division; the hard step (wreath associativity) is sgDiv_wreath_assoc.

inductive LeanPool.KrohnRhodes.KRFactorKind : Type

The two kinds of factors used here: a finite aperiodic monoid or a finite simple group. The aperiodic factors need not be irreducible or three-element reset monoids.

• aperiodic : KRFactorKind

  The factor is a finite aperiodic monoid.

• simpleGroup : KRFactorKind

  The factor is a finite simple group.

@[instance_reducible]

instance LeanPool.KrohnRhodes.instDecidableEqKRFactorKind : DecidableEq KRFactorKind

Equations

• LeanPool.KrohnRhodes.instDecidableEqKRFactorKind x✝ y✝ = if h : x✝.ctorIdx = y✝.ctorIdx then isTrue ⋯ else isFalse ⋯

def LeanPool.KrohnRhodes.instReprKRFactorKind.repr : KRFactorKind → ℕ → Std.Format

Equations

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

@[instance_reducible]

instance LeanPool.KrohnRhodes.instReprKRFactorKind : Repr KRFactorKind

Equations

• LeanPool.KrohnRhodes.instReprKRFactorKind = { reprPrec := LeanPool.KrohnRhodes.instReprKRFactorKind.repr }

structure LeanPool.KrohnRhodes.KRFactor : Type (u + 1)

A single Krohn-Rhodes factor: a finite monoid carrier together with a flag kind and a proof that carrier really satisfies its flag. The proof field is what makes the decomposition genuinely informative (not a vacuous existential): an aperiodic factor must actually be aperiodic (every element has a trivial H-class), and a simpleGroup factor must actually carry a Group instance that is IsSimpleGroup.

• carrier : Type u

  The carrier monoid of the factor.

• mon : Monoid self.carrier

  The factor's monoid structure.

• fin : Finite self.carrier

  The factor is finite.

• kind : KRFactorKind

  Whether the factor is an aperiodic factor or a simple-group factor.

• isKind : (self.kind = KRFactorKind.aperiodic ∧ ∀ (a : self.carrier), Green.IsAperiodicElem a) ∨ self.kind = KRFactorKind.simpleGroup ∧ ∃ (g : Group self.carrier), g.toMonoid = self.mon ∧ IsSimpleGroup self.carrier

  The flag is witnessed: an aperiodic-flagged factor is genuinely aperiodic; a simpleGroup-flagged factor genuinely carries a finite simple-group structure on carrier whose underlying monoid is the factor's own monoid field (g.toMonoid = mon). Recording the g.toMonoid = mon compatibility lets one transport monoid-indexed data between F.mon and the witnessed group instance g.

def LeanPool.KrohnRhodes.KRFactor.ofAperiodic (A : Type u) [Monoid A] [Finite A] (hA : ∀ (a : A), Green.IsAperiodicElem a) : KRFactor

Build an aperiodic factor from a finite aperiodic monoid.

Equations

• LeanPool.KrohnRhodes.KRFactor.ofAperiodic A hA = { carrier := A, mon := inst✝¹, fin := inst✝, kind := LeanPool.KrohnRhodes.KRFactorKind.aperiodic, isKind := ⋯ }

def LeanPool.KrohnRhodes.KRFactor.ofSimpleGroup (G : Type u) [g : Group G] [Finite G] [IsSimpleGroup G] : KRFactor

Build a simple-group factor from a finite simple group.

Equations

• LeanPool.KrohnRhodes.KRFactor.ofSimpleGroup G = { carrier := G, mon := g.toMonoid, fin := inst✝¹, kind := LeanPool.KrohnRhodes.KRFactorKind.simpleGroup, isKind := ⋯ }

@[simp]

theorem LeanPool.KrohnRhodes.KRFactor.ofAperiodic_carrier (A : Type u) [Monoid A] [Finite A] (hA : ∀ (a : A), Green.IsAperiodicElem a) : (ofAperiodic A hA).carrier = A

@[simp]

theorem LeanPool.KrohnRhodes.KRFactor.ofAperiodic_kind (A : Type u) [Monoid A] [Finite A] (hA : ∀ (a : A), Green.IsAperiodicElem a) : (ofAperiodic A hA).kind = KRFactorKind.aperiodic

@[simp]

theorem LeanPool.KrohnRhodes.KRFactor.ofSimpleGroup_carrier (G : Type u) [Group G] [Finite G] [IsSimpleGroup G] : (ofSimpleGroup G).carrier = G

@[simp]

theorem LeanPool.KrohnRhodes.KRFactor.ofSimpleGroup_kind (G : Type u) [Group G] [Finite G] [IsSimpleGroup G] : (ofSimpleGroup G).kind = KRFactorKind.simpleGroup

def LeanPool.KrohnRhodes.DivTowerWreath (M : Type u) [Monoid M] [Finite M] : List KRFactor → Prop

The recursive division predicate of a factor tower.

DivTowerWreath M factors records the following recursive wreath divisions:

• [] — M divides the trivial monoid PUnit (the empty product; this forces M to be a single point up to division).
• F :: rest — there is a finite base monoid B that itself decomposes via the tail rest (DivTowerWreath B rest), and M divides WreathProduct F.carrier B Y for some finite type Y on which B acts: the head factor F.carrier sits in the decoration slot over the base B.

No action-lifting or equivalence with a single iterated transformation wreath product is asserted by this definition. The intermediate base at each step has its own tower.

Equations

• One or more equations did not get rendered due to their size.
• LeanPool.KrohnRhodes.DivTowerWreath x✝² [] = LeanPool.KrohnRhodes.SgDiv x✝² PUnit.{?u.1 + 1}

@[simp]

theorem LeanPool.KrohnRhodes.divTowerWreath_nil (M : Type u) [Monoid M] [Finite M] : DivTowerWreath M [] = SgDiv M PUnit.{u + 1}

theorem LeanPool.KrohnRhodes.divTowerWreath_cons (M : Type u) [Monoid M] [Finite M] (F : KRFactor) (rest : List KRFactor) : DivTowerWreath M (F :: rest) ↔ ∃ (B : Type u) (x : Monoid B) (x_1 : Finite B) (Y : Type u) (x_2 : Fintype Y) (x_3 : MulAction B Y), DivTowerWreath B rest ∧ SgDiv M (WreathProduct F.carrier B Y)

Base-case constructors for the factor tower

theorem LeanPool.KrohnRhodes.sgDiv_wreath_subsingleton_base (A B : Type u) [Monoid A] [Monoid B] [Subsingleton B] : SgDiv A (WreathProduct A B B)

A single finite factor A over a subsingleton base B divides A ≀_B B (the wreath of A over the trivial base, with B acting on itself). This is the "one rung" building block: when B is a single point the wreath multiplication collapses to a copy of A.

Stated for a general subsingleton B (rather than literally PUnit) so that the wreath-product instances match exactly those produced by the cons case of DivTowerWreath at the call site (avoiding MulAction PUnit PUnit instance ambiguity).

theorem LeanPool.KrohnRhodes.divTowerWreath_nil_of_subsingleton (M : Type u) [Monoid M] [Finite M] [Subsingleton M] : DivTowerWreath M []

The empty factor tower for a subsingleton monoid: a subsingleton M divides PUnit.

theorem LeanPool.KrohnRhodes.divTowerWreath_single (F : KRFactor) : DivTowerWreath F.carrier [F]

A single-factor tower over a factor F: DivTowerWreath F.carrier [F], witnessed by the PUnit base. (Stated directly over F.carrier with its canonical F.mon/F.fin instances so the wreath-product instances coincide with the recursive predicate's.)

theorem LeanPool.KrohnRhodes.divTowerWreath_ofAperiodic (M : Type u) [Monoid M] [Finite M] (hAper : ∀ (a : M), Green.IsAperiodicElem a) : DivTowerWreath M [KRFactor.ofAperiodic M hAper]

Single aperiodic factor tower. A finite aperiodic monoid M has the one-element factor tower [KRFactor.ofAperiodic M hAper].

theorem LeanPool.KrohnRhodes.divTowerWreath_ofSimpleGroup (G : Type u) [Group G] [Finite G] [IsSimpleGroup G] : DivTowerWreath G [KRFactor.ofSimpleGroup G]

Single simple-group factor tower. A finite simple group G has the one-element factor tower [KRFactor.ofSimpleGroup G].

Division compatibility of the factor tower

The tower predicate is monotone under semigroup division on the left: if S divides T and T has a recursive wreath-division tower, then so does S. It is used to transfer a tower along a division SgDiv S (WreathProduct A B X).

theorem LeanPool.KrohnRhodes.divTowerWreath_of_sgDiv {S T : Type u} [Monoid S] [Finite S] [Monoid T] [Finite T] (h : SgDiv S T) {factors : List KRFactor} : DivTowerWreath T factors → DivTowerWreath S factors

Division transfers the factor tower. If SgDiv S T and DivTowerWreath T factors, then DivTowerWreath S factors.

Wreath associativity (the inductive-step engine)

To combine towers of the decoration factor A and the base factor B (in S ≼ A ≀ B) into a single factor list we need the classical associativity of the wreath product up to division: a wreath nested in the decoration slot re-associates into the base.

For the left-action convention (p * q).func x = p.func (q.base • x) * q.func x, the precise associativity is

(G ≀_{B'} B') ≀_X B ≼ G ≀_W (B' × X), where W = B' ≀_X B,

with W acting on the product state space B' × X by the imprimitive action ⟨γ, b⟩ • (p, x) = (γ x * p, b • x). This is the standard wreath-associativity theorem (Eilenberg, Automata, Languages and Machines, Vol. B, Ch. III; Wells, "Some applications of the wreath product construction", 1976), realised by the canonical "unscrambling" embedding Phi below. The q.base • x cocycle threads through both levels exactly because the inner state action of B' on B' is left multiplication.

@[instance_reducible]

def LeanPool.KrohnRhodes.WreathAssoc.actW (B' B Y X : Type u) [Monoid B'] [Monoid B] [MulAction B' Y] [MulAction B X] : MulAction (WreathProduct B' B X) (Y × X)

The imprimitive action of the base wreath W = B' ≀_X B on the product state space Y × X: ⟨γ, b⟩ • (y, x) = (γ x • y, b • x) — the inner base B' acts on the inner state Y, the outer base B acts on the outer state X.

Equations

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

def LeanPool.KrohnRhodes.WreathAssoc.Phi (G B' B Y X : Type u) [Monoid G] [Monoid B'] [Monoid B] [MulAction B' Y] [MulAction B X] : WreathProduct (WreathProduct G B' Y) B X →ₙ* WreathProduct G (WreathProduct B' B X) (Y × X)

The canonical unscrambling embedding (G ≀_{B'} Y) ≀_X B →ₙ* G ≀_W (Y × X) realising wreath associativity: the two-level decoration F becomes the one-level decoration (y, x) ↦ (F.func x).func y, and the bases collect to ⟨fun x => (F.func x).base, F.base⟩.

Equations

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

theorem LeanPool.KrohnRhodes.WreathAssoc.Phi_injective (G B' B Y X : Type u) [Monoid G] [Monoid B'] [Monoid B] [MulAction B' Y] [MulAction B X] : Function.Injective ⇑(Phi G B' B Y X)

theorem LeanPool.KrohnRhodes.sgDiv_wreath_assoc (G B' B Y X : Type u) [Monoid G] [Monoid B'] [Monoid B] [MulAction B' Y] [MulAction B X] : SgDiv (WreathProduct (WreathProduct G B' Y) B X) (WreathProduct G (WreathProduct B' B X) (Y × X))

Wreath associativity, up to division. (G ≀_{B'} Y) ≀_X B divides G ≀_W (Y × X) where the base W = B' ≀_X B acts on Y × X by WreathAssoc.actW (the inner base on the inner state, the outer base on the outer state). Fully proved via the unscrambling embedding WreathAssoc.Phi (an injective semigroup homomorphism).

theorem LeanPool.KrohnRhodes.sgDiv_wreath_decoration_mono (A A' B X : Type u) [Monoid A] [Monoid A'] [Monoid B] [MulAction B X] (h : SgDiv A A') : SgDiv (WreathProduct A B X) (WreathProduct A' B X)

Wreath product is monotone in the decoration factor. If A divides A', then A ≀_X B divides A' ≀_X B: lift the surjection U' ↠ A pointwise over the decoration, restricting to the subsemigroup of A' ≀_X B whose decorations land in U'.

theorem LeanPool.KrohnRhodes.subsingleton_of_sgDiv_punit (A : Type u) [Monoid A] (h : SgDiv A PUnit.{u + 1}) : Subsingleton A

SgDiv A PUnit forces A to be a subsingleton (it is a quotient of a subsemigroup of the one-point monoid).

theorem LeanPool.KrohnRhodes.sgDiv_wreath_of_subsingleton_decoration (A B X : Type u) [Monoid A] [Monoid B] [MulAction B X] [Subsingleton A] : SgDiv (WreathProduct A B X) B

When the decoration factor A is a subsingleton, A ≀_X B ≅ B, so A ≀_X B divides B (the projection onto the base is an isomorphism).

theorem LeanPool.KrohnRhodes.divTowerWreath_wreathStep (towA : List KRFactor) {S A B X : Type u} [Monoid S] [Finite S] [Monoid A] [Finite A] [Monoid B] [Finite B] [Finite X] [MulAction B X] : SgDiv S (WreathProduct A B X) → DivTowerWreath A towA → ∀ {towB : List KRFactor}, DivTowerWreath B towB → DivTowerWreath S (towA ++ towB)

The factor-tower concatenation step.

If S divides A ≀_X B, the decoration factor A has a factor tower towA, and the base factor B has a factor tower towB, then S has the concatenated factor tower towA ++ towB.

It flattens the two sub-decompositions into one explicit list. The proof is by induction on towA, using sgDiv_wreath_decoration_mono to push the decomposition of A into the decoration slot and sgDiv_wreath_assoc to re-associate the nested wreath into the base.

Factor towers whose factors divide the monoid

KRFactorTowerSub M is a factor tower of M in which every factor divides M. For finite groups such a tower is built by induction along a normal subgroup (group_subquotient_faithful_aux); the main theorem uses it in its group case.

Monoid-division helpers

theorem LeanPool.KrohnRhodes.monoidDivides_of_surjective {M N : Type u} [Monoid M] [Monoid N] (φ : M →* N) (hφ : Function.Surjective ⇑φ) : MonoidDivides N M

A surjective monoid homomorphism φ : M ↠ N exhibits N as a quotient of M, hence N divides M.

theorem LeanPool.KrohnRhodes.monoidDivides_refl (M : Type u) [Monoid M] : MonoidDivides M M

Monoid division is reflexive.

theorem LeanPool.KrohnRhodes.monoidDivides_subgroup {G : Type u} [Group G] (N : Subgroup G) : MonoidDivides (↥N) G

A subgroup N ≤ G divides G.

theorem LeanPool.KrohnRhodes.quotientGroup_divides {G : Type u} [Group G] (N : Subgroup G) [N.Normal] : MonoidDivides (G ⧸ N) G

The quotient group G/N divides G.

The subquotient-faithful factor tower

def LeanPool.KrohnRhodes.SubFactorsDivide (M : Type u) [Monoid M] (factors : List KRFactor) : Prop

SubFactorsDivide M factors asserts every factor's carrier divides M.

Equations

• LeanPool.KrohnRhodes.SubFactorsDivide M factors = ∀ F ∈ factors, LeanPool.KrohnRhodes.MonoidDivides F.carrier M

theorem LeanPool.KrohnRhodes.subFactorsDivide_nil (M : Type u) [Monoid M] : SubFactorsDivide M []

theorem LeanPool.KrohnRhodes.subFactorsDivide_single {M : Type u} [Monoid M] (F : KRFactor) (h : MonoidDivides F.carrier M) : SubFactorsDivide M [F]

theorem LeanPool.KrohnRhodes.subFactorsDivide_of_divides {A M : Type u} [Monoid A] [Monoid M] (hAM : MonoidDivides A M) {factors : List KRFactor} (h : SubFactorsDivide A factors) : SubFactorsDivide M factors

If every factor of factors divides A, and A divides M, then every factor divides M (transitivity of division).

theorem LeanPool.KrohnRhodes.subFactorsDivide_append {M : Type u} [Monoid M] {towA towB : List KRFactor} (hA : SubFactorsDivide M towA) (hB : SubFactorsDivide M towB) : SubFactorsDivide M (towA ++ towB)

The append of two divides-witnessed factor lists.

structure LeanPool.KrohnRhodes.KRFactorTowerSub (M : Type u) [Monoid M] [Finite M] : Type (u + 1)

A factor tower whose factors divide M. A factor list, a proof that M has the recursive wreath-division tower, and the guarantee that every factor's carrier divides M.

• factors : List KRFactor

  The explicit list of Krohn-Rhodes factors.

• divides : DivTowerWreath M self.factors

  The recursive wreath-division tower for M over factors.

• factorsDivide : SubFactorsDivide M self.factors

  Every factor's carrier divides M (the subquotient-faithful condition).

Subquotient-faithful Krohn-Rhodes for finite groups

theorem LeanPool.KrohnRhodes.group_subquotient_faithful_aux (n : ℕ) (G : Type u) [Group G] [Finite G] : Nat.card G ≤ n → Nonempty (KRFactorTowerSub G)

Subquotient-faithful Krohn-Rhodes for finite groups. Every finite group G has a subquotient-faithful factor tower: simple-group factors, each dividing G, together with a recursive wreath-division tower for G. Proved by strong induction on Nat.card G, peeling a proper normal subgroup N and recursing on the subgroup ↥N (÷ G) and the quotient G/N (÷ G), threading the MonoidDivides-to-G witness through every factor (subgroup-divides / quotient-divides + transitivity).