Aperiodic/simple-group wreath-division towers for finite monoids #
krohn_rhodes_prime_decomposition constructs KRFactorTowerGrp M for every finite monoid
M : Type: a finite recursive wreath-division tower with aperiodic or simple-group factors,
and a proof that each simple-group factor is a monoid divisor of M.
This is a variant of the local-divisor argument of V. Diekert, M. Kufleitner and B. Steinberg,
The Krohn–Rhodes Theorem and Local Divisors, Fundamenta Informaticae 116 (2012),
arXiv:1111.1585, Sections 3–4. It uses left actions and the
larger local divisor cM ∩ Mc described in their Section 2.5. The endpoint retains recursive
semigroup divisions, allows arbitrary finite aperiodic factors, and does not claim the
three-element flip-flop reduction, a single transformation-monoid strong division, or the
quantitative bounds in Theorem 4.1. See DivTowerWreath for the exact recursion.
The declarations in this file are for types in universe 0.
The full transformation monoid of a finite type is finite. Function.End Q is
definitionally Q → Q, but the Pi.finite instance does not fire through the semireducible
Function.End. Needed so that statements about
DivTowerWreath ↥(closureMonoid act) … elaborate. Finite is a Prop, so the instance cannot
create diamonds.
The reset submonoid (constants with identity) #
Convention: Function.End Q multiplies by composition (f * g) x = f (g x), so the constant
maps constEnd q are LEFT zeros (constEnd p * t = constEnd p,
t * constEnd q = constEnd (t q)). The reset submonoid is the left-action counterpart of the
reset monoid U_X = const(X) ∪ {1} of DKS §2.4.
The reset submonoid of the full transformation monoid. For a type $Q$, the reset
submonoid of the full transformation monoid $\mathrm{End}(Q)$ (multiplication is composition,
$(f \cdot g)(x) = f(g(x))$) is the submonoid generated by the constant maps $\overline{q}$ (Lean:
constEnd), $q \in Q$. Constant maps are left zeros ($\overline{p} \cdot t = \overline{p}$ and
$t \cdot \overline{q} = \overline{t(q)}$), so the generated carrier collapses to
$\{1\} \cup \{\overline{q} \mid q \in Q\}$ (mem_reset_submonoid). This is the left-action
counterpart of the reset monoid $U_X = \bar{X} \cup \{1\}$ of DKS (arXiv:1111.1585) §2.4 — right
zeros there, left zeros here, the flip forced by the composition order. It is defined as a
Submonoid.closure of the generators rather than by its explicit carrier, so the definition
carries no closedness obligations; the carrier description is the separate mem_reset_submonoid.
Equations
Instances For
Membership in the reset submonoid: identity or constant. For every transformation
$t \in \mathrm{End}(Q)$ of a type $Q$: $t$ lies in the reset submonoid resetSubmonoid if and
only if $t = 1$ or $t$ is a constant map (the predicate IsConstEnd:
$\exists q,\ t = \overline{q}$).
Proof sketch. Right-to-left: $1$ belongs to every submonoid, and every constant map is a
generator (Submonoid.subset_closure). Left-to-right: induction over the submonoid closure
(Submonoid.closure_induction): a generator is a constant (isConstEnd_constEnd); $1$ is the
left disjunct; and for a product $x \cdot y$ with both factors identity-or-constant, either
$x = 1$ — then the product is $y$ and the inductive hypothesis for $y$ applies — or
$x = \overline{p}$ is constant and absorbs $y$ on the left by the left-zero law
(constEnd_mul: $\overline{p} \cdot y = \overline{p}$), so the product
is again a constant. This is the closure computation of DKS §2.4.
The reset submonoid is aperiodic. Every element of the reset submonoid resetSubmonoid
of $\mathrm{End}(Q)$, viewed as a finite monoid in its own right, is aperiodic in the sense of
Green's relations (Green.IsAperiodicElem): its $\mathcal{H}$-class inside the submonoid is
trivial — $a \mathrel{\mathcal{H}} b$ implies $a = b$. This witnesses the reset factor of the
decomposition as a genuine aperiodic Krohn-Rhodes factor (DKS §2.4: the reset monoid is aperiodic).
Proof sketch. By mem_reset_submonoid every member of the submonoid is the identity or a
constant, so isAperiodicElem_of_id_or_const applies; its conclusion
is exactly the $\mathcal{H}$-triviality shape obtained by unfolding Green.H (an
$\mathcal{L}$-witness pair and an $\mathcal{R}$-witness pair in the subtype monoid) — destructure
the $\mathcal{H}$ hypothesis and apply.
The constants closure of an action #
The constants closure of a transformation representation. For a monoid homomorphism
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$, the constants closure is the submonoid of
$\mathrm{End}(Q)$ generated by the image of $\mathrm{act}$ together with all constant maps
$\overline{q}$. This is the counterpart of the closure $\overline{(X,M)} = (X, M \cup \bar{X})$
of DKS §2.4. DKS define the closure by its explicit carrier $M \cup \bar{X}$ and verify
closedness by a four-case product computation; here it is a Submonoid.closure, so that
computation is not a separate proof obligation — the only facts used later are generation over a
generating set of $M$ (closure_monoid_gen) and the division sgdiv_closure_monoid. The whole
DKS induction runs on closures: it produces towers for $\overline{(Q,M)}$, and the main theorem
recovers $M$ through sgdiv_closure_monoid.
Equations
Instances For
A faithfully represented monoid divides its constants closure. Let $M$ be a monoid and
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ an injective monoid homomorphism. Then $M$ divides
the constants closure closureMonoid as a semigroup (SgDiv: some subsemigroup of
$\overline{(Q,M)}$ maps onto $M$ by a multiplicative surjection). Used once, in the master
assembly krohn_rhodes_prime_decomposition, to pull the tower of the closure back to $M$.
Proof sketch. The image of $\mathrm{act}$ is contained in the closure (left disjunct of the
generating set, Submonoid.subset_closure), so $\mathrm{act}$ corestricts to a monoid
homomorphism $M \to^* \overline{(Q,M)}$ (MonoidHom.codRestrict), injective because
$\mathrm{act}$ is. sgDiv_of_injective_monoidHom turns an injective
monoid homomorphism into a semigroup division.
A generating set of the monoid generates its constants closure. Let
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ be a monoid homomorphism and $A \subseteq M$ a
generating set of $M$ ($\texttt{Submonoid.closure}\,A = \top$). Then the submonoid of
$\mathrm{End}(Q)$ generated by $\mathrm{act}(A) \cup \{\overline{q} \mid q\}$ equals the
constants closure closureMonoid. This is what lets the covering argument of
main_decomposition check covers on the generators $\mathrm{act}(a)$, $a \in A$, only.
Proof sketch. Both sides split along the union (Submonoid.closure_union) with identical
constants summand, so it suffices to identify the other summands with the range submonoid of
$\mathrm{act}$: $\langle \mathrm{act}(A) \rangle = \mathrm{act}(\langle A \rangle) = \mathrm{act}(\top) = \mathrm{mrange} (\mathrm{act})$ — the image of a closure is the closure of
the image (MonoidHom.map_mclosure), then the hypothesis $\langle A \rangle = \top$ and
MonoidHom.mrange_eq_map; and
$\langle \mathrm{range}(\mathrm{act}) \rangle = \mathrm{mrange}(\mathrm{act})$ because the range
is already a submonoid (Submonoid.closure_eq at the carrier identification
MonoidHom.coe_mrange). Pure closure algebra — no closure induction is needed,
$\mathrm{act}(1) = 1$ and multiplicativity being absorbed into map_mclosure.
Covers and division from covering (DKS §2.3, Prop 2.3) #
The evaluation wreath action used throughout is w • (p, y) = (w.func y • p, w.base • y), the
action WreathAssoc.actW of KrohnRhodes/FactorTower.lean; the Covers predicate
inlines it, so no new MulAction instance is introduced.
The cover relation between wreath elements and transformations. Fix monoids $A, B$, an
$A$-set $P$, a $B$-set $X$, a type $R$, and a map $\varphi \colon P \times X \to R$. An element
$w$ of the wreath product $A \wr_X B$ (multiplication
$(f_1,b_1)(f_2,b_2) = (x \mapsto f_1(b_2 \cdot x) f_2(x),\ b_1 b_2)$) covers a transformation
$t \in \mathrm{End}(R)$ when $\varphi(w \bullet s) = t(\varphi(s))$ for every $s \in P \times X$,
where $w \bullet (p, y) = (w.\mathrm{func}(y) \cdot p,\ w.\mathrm{base} \cdot y)$ is the
evaluation wreath action (WreathAssoc.actW; the definition inlines it). This is DKS §2.3; with
left actions, covers compose covariantly, with no order reversal.
Equations
Instances For
The identity wreath element covers the identity transformation. In the setting of
Covers, the identity of the wreath product $A \wr_X B$ covers the identity of
$\mathrm{End}(R)$: $\varphi(1 \bullet s) = \varphi(s)$ for all $s$.
Proof sketch. Immediate: the identity wreath element has trivial decoration and base
(WreathProduct.one_func, one_base), and $1 \cdot p = p$, $1 \cdot y = y$ (one_smul).
Covers compose: a product of covers covers the product. In the setting of Covers: if
$w_1$ covers $t_1$ and $w_2$ covers $t_2$, then $w_1 w_2$ covers $t_1 t_2$ (composition in
$\mathrm{End}(R)$, i.e. $(t_1 t_2)(r) = t_1(t_2(r))$). This is DKS Prop 2.3(1); with left actions
the orders align without reversal.
Proof sketch. $\varphi((w_1 w_2) \bullet s) = \varphi(w_1 \bullet (w_2 \bullet s))$ by the
wreath action law ($(w_1 w_2) \bullet s = w_1 \bullet (w_2 \bullet s)$, computed from
WreathProduct.mul_func/mul_base and mul_smul — the mul_smul field of WreathAssoc.actW);
this equals $t_1(\varphi(w_2 \bullet s)) = t_1(t_2(\varphi(s)))$ by the two cover hypotheses.
A wreath element covers at most one transformation (surjective decoding). In the setting
of Covers, assume $\varphi$ is surjective. If $w$ covers both $t_1$ and $t_2$, then $t_1 = t_2$
(DKS Prop 2.3(2)). This is what makes the decoded transformation of a covering wreath element
well-defined in sgdiv_of_covering.
Proof sketch. For every $r \in R$ pick $s$ with $\varphi(s) = r$ (surjectivity); then
$t_1(r) = \varphi(w \bullet s) = t_2(r)$, and transformations agreeing pointwise are equal
(funext).
Division from covering: covered generators yield a wreath divisor. In the setting of
Covers, let $\varphi \colon P \times X \to R$ be surjective, let $T$ be a submonoid of
$\mathrm{End}(R)$, and let $S \subseteq \mathrm{End}(R)$ generate $T$
($\texttt{Submonoid.closure}\,S = T$). If every $t \in S$ is covered by some $w \in A \wr_X B$,
then $T$ divides $A \wr_X B$ as a semigroup (SgDiv). This is the division-from-covering
argument of DKS §2.3.
Proof sketch. First, every $t \in T = \langle S \rangle$ is covered by some wreath element: by
induction over the closure representation (Submonoid.closure_induction), generators are covered
by hypothesis, $1$ is covered by covers_one, and products of covered elements are covered by
covers_mul. Let $V := \{w \mid \exists t \in T,\ w \text{ covers } t\}$: it is closed under
products by covers_mul (the covered transformations multiply inside the submonoid $T$), so $V$
is a subsemigroup of the wreath. Define $\psi \colon V \to T$ sending $w$ to THE transformation
it covers: well-defined by covers_unique (with surjectivity of $\varphi$) plus choice, and
multiplicative by covers_mul together with covers_unique (both sides of the multiplicativity
equation cover the same product element). $\psi$ is surjective onto $T$: a $t \in T$ is covered
by some $w$ by the first step, $w \in V$, and the decoded transformation of $w$ is $t$ by
covers_unique.
The local divisor and its action on the image state set #
The local divisor LocalDivisor M c (carrier cM ∩ Mc, twisted
product, identity c, and the division localDivides : M_c ÷ M) is defined in
KrohnRhodes/Foundations/LocalDivisor.lean; DKS §2.5 allows the cM ∩ Mc variant. This
section adds the cardinality drop for a non-unit c and the faithful action of M_c on the
image state set cQ.
The local divisor at a non-unit is strictly smaller. Let $M$ be a finite monoid and
$c \in M$ a non-unit. Then $|M_c| < |M|$, where $M_c$ is the local divisor
LocalDivisor $M$ $c$ (carrier $cM \cap Mc$). Cardinalities are
Nat.card; both sides are finite. (DKS §2.5: if $c$ is not a unit then $1 \notin cM \cap Mc$.)
Proof sketch. Pure algebra, no finiteness in the key step: if $1 = c a$ and $1 = b c$ then
$b = b(ca) = (bc)a = a$, so $a$ is a two-sided inverse of $c$ ($ca = 1$ and $ac = 1$) and $c$ is
a unit — contradiction. Hence no element of $M_c$ has value $1$: the value map
$M_c \hookrightarrow M$ (injective by LocalDivisor.ext) misses the point $1$. Transporting both
cardinalities through Fintype.ofFinite and Nat.card_eq_fintype_card, the
injection-missing-a-point counting lemma Fintype.card_lt_of_injective_of_notMem gives the
strict inequality.
The image state set of the chosen non-unit. For a monoid homomorphism $\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ and $c \in M$, the image state set $cQ$ is the subtype $\{q \in Q \mid \exists x,\ q = \mathrm{act}(c)(x)\}$ — the set of states in the image of the transformation induced by $c$. This is the state set on which the local divisor $M_c$ acts (DKS Lemma 2.11).
Instances For
The action of the local divisor on the image state set. For
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ and $c \in M$, the monoid homomorphism
$M_c \to^* \mathrm{End}(cQ)$: an element $u \in cM \cap Mc$ with chosen factorization $u = b c$
(the Classical.choose of LocalDivisor.mem_right) acts on $p \in cQ$ by
$p \mapsto \mathrm{act}(b)(p)$. Well-definedness (the obligations embedded in this definition,
following DKS Lemma 2.11 with the $Mc$-witness — left actions force the $Mc$-side where DKS use
$cM$): (i) the value lands in $cQ$ — for $p = \mathrm{act}(c)(x)$,
$\mathrm{act}(b)(p) = \mathrm{act}(bc)(x) = \mathrm{act}(u)(x)$, and writing $u = c a$ (left
membership) this is $\mathrm{act}(c)(\mathrm{act}(a)(x)) \in cQ$; (ii) the displayed formula
$\mathrm{act}(u)(x)$ depends only on $u$, not on the chosen $b$; (iii) the identity $c = 1_{M_c}$
acts as the identity, and the twisted product acts by composition — both computed from
$\mathrm{act}(u)(x)$-normal forms via LocalDivisor.mul_val. Faithfulness is the separate
local_act_injective.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The local divisor acts faithfully on the image state set. If
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ is injective, then the local-divisor action
localActHom is injective: distinct elements of $M_c$ induce distinct transformations of $cQ$.
This is the faithfulness half of DKS Lemma 2.11, supplying the injectivity hypothesis when the
induction dks_aux recurses into $(cQ, M_c)$.
Proof sketch. Suppose $u, v \in M_c$ act identically on $cQ$. For every $x \in Q$ the point
$\mathrm{act}(c)(x)$ lies in $cQ$, and the displayed well-definedness formula of localActHom
gives $\mathrm{act}(u)(x) = u \bullet (\mathrm{act}(c)(x)) = v \bullet (\mathrm{act}(c)(x)) = \mathrm{act}(v)(x)$ (values through LocalDivisor.val); hence
$\mathrm{act}(u.\mathrm{val}) = \mathrm{act}(v.\mathrm{val})$ as transformations, so
$u.\mathrm{val} = v.\mathrm{val}$ by injectivity of $\mathrm{act}$, so $u = v$
(LocalDivisor.ext).
The local-divisor decomposition (variant of DKS Theorem 3.1) #
The extension action of a submonoid on states plus carrier. For
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ and a submonoid $N \le M$, the monoid homomorphism
$N \to^* \mathrm{End}(Q \sqcup N)$: $n$ sends $\mathrm{inl}\,q$ to
$\mathrm{inl}\,(\mathrm{act}(n)(q))$ and $\mathrm{inr}\,m$ to $\mathrm{inr}\,(n m)$ (left
multiplication in $N$). This is the base coordinate $X' = Q \sqcup N$ of DKS Thm 3.1 (their
$X \cup N$, with $N$ acting on itself on the left). The embedded obligations (identity and
multiplicativity) are the case computations $\mathrm{act}(1) = 1$, $1 \cdot m = m$,
$\mathrm{act}(n_1 n_2) = \mathrm{act}(n_1)\mathrm{act}(n_2)$, and associativity of
multiplication. Injectivity is the separate ext_act_injective.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The extension action is faithful. For every monoid homomorphism
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ and submonoid $N \le M$, the extension action
extAct is injective — with NO faithfulness hypothesis on $\mathrm{act}$: the $\mathrm{inr}$
component alone separates elements (evaluate at $\mathrm{inr}\,1$). Supplies the injectivity
hypothesis when the induction dks_aux recurses into $(Q \sqcup N, N)$.
Proof sketch. If $n_1, n_2 \in N$ induce the same transformation of $Q \sqcup N$, evaluate at
$\mathrm{inr}\,1$: $\mathrm{inr}\,(n_1 \cdot 1) = \mathrm{inr}\,(n_2 \cdot 1)$, so $n_1 = n_2$ by
injectivity of $\mathrm{inr}$ and mul_one.
The decoding surjection of the main decomposition. For $\mathrm{act} \colon M \to^* \mathrm{End}(Q)$, $c \in M$, and a submonoid $N \le M$, the map $\varphi \colon cQ \times (Q \sqcup N) \to Q$ defined by $\varphi(p, \mathrm{inl}\,q) = q$ and $\varphi(p, \mathrm{inr}\,n) = \mathrm{act}(n)(p)$ (the value of the local state $p \in cQ$, transported by $n$). This is the cover decoding of DKS Thm 3.1.
Equations
- LeanPool.KrohnRhodes.dksProj act c N s = Sum.elim (fun (q : Q) => q) (fun (n : ↥N) => act ↑n ↑s.1) s.2
Instances For
The decoding map is surjective. If $Q$ is nonempty, the decoding map dksProj is
surjective: every $q \in Q$ is $\varphi(p_0, \mathrm{inl}\,q)$ for any point $p_0$ of the image
state set $cQ$ — which is nonempty because $\mathrm{act}(c)(q_0) \in cQ$ for any $q_0 \in Q$.
(The empty/subsingleton $Q$ case never reaches this lemma: the induction dks_aux dispatches it
to the empty tower first.)
Proof sketch. As stated: $cQ$ is inhabited by $\langle \mathrm{act}(c)(q_0), q_0 \rangle$ for
$q_0$ from Nonempty $Q$, and $\varphi(p_0, \mathrm{inl}\,q) = q$.
Cover family 1: constants are covered. In the wreath product
$\overline{(cQ, M_c)} \wr_{Q \sqcup N} \overline{(Q \sqcup N, N)}$ — decoration the constants
closure closureMonoid of the local action localActHom, base the constants closure of the
extension action extAct, both acting by evaluation — every constant transformation
$\overline{x} \in \mathrm{End}(Q)$, $x \in Q$, is covered (Covers) with respect to the decoding
dksProj. (DKS Thm 3.1, first cover family.)
Proof sketch. Take $\hat{w} := (\lambda y.\,1,\ \overline{\mathrm{inl}\,x})$ — trivial decoration, base the constant onto $\mathrm{inl}\,x$, which lies in the base closure because constants are generators. Then $\hat{w} \bullet (p, y) = (p, \mathrm{inl}\,x)$, so $\varphi(\hat{w} \bullet (p,y)) = x = \overline{x}(\varphi(p,y))$. Direct computation.
Cover family 2: the action of a submonoid element is covered. In the wreath product of
cover_const_end, for every $n \in N$ the transformation $\mathrm{act}(n) \in \mathrm{End}(Q)$
is covered (Covers) with respect to the decoding dksProj. (DKS Thm 3.1, second cover family —
their $k_c$ with identity decoration.)
Proof sketch. Take $\hat{w} := (\lambda y.\,1,\ \mathrm{extAct}(n))$ — trivial decoration, base the extension action of $n$ (a generator of the base closure). On $(p, \mathrm{inl}\,q)$: $\hat{w} \bullet (p, \mathrm{inl}\,q) = (p, \mathrm{inl}\,(\mathrm{act}(n)(q)))$, and $\varphi = \mathrm{act}(n)(q) = \mathrm{act}(n)(\varphi(p, \mathrm{inl}\,q))$. On $(p, \mathrm{inr}\,m)$: $\hat{w} \bullet (p, \mathrm{inr}\,m) = (p, \mathrm{inr}\,(n m))$, and $\varphi = \mathrm{act}(nm)(p) = \mathrm{act}(n)(\mathrm{act}(m)(p)) = \mathrm{act}(n)(\varphi(p, \mathrm{inr}\,m))$ by multiplicativity. Direct computation.
Cover family 3: the action of the chosen non-unit is covered. In the wreath product of
cover_const_end, the transformation $\mathrm{act}(c) \in \mathrm{End}(Q)$ itself is covered
(Covers) with respect to the decoding dksProj. This is THE local-divisor step of DKS Thm 3.1
(their decoration $f_c$ with $y f_c = \overline{y \cdot c}$ on states and $n f_c = cnc$ on $N$,
base constant onto $1 \in N$).
Proof sketch. Take $\hat{w} := (f_c,\ \overline{\mathrm{inr}\,1})$ with decoration
$f_c(\mathrm{inl}\,q) := \overline{\langle \mathrm{act}(c)(q) \rangle}$ (a constant of
$\mathrm{End}(cQ)$, hence in the decoration closure) and
$f_c(\mathrm{inr}\,n) := \mathrm{localActHom}\,\langle c n c \rangle$ (in the range of the local
action, hence in the decoration closure; $cnc \in cM \cap Mc$ with the two evident factorizations
$cnc = c \cdot (nc) = (cn) \cdot c$). Then
$\hat{w} \bullet (p, y) = (f_c(y) \bullet p,\ \mathrm{inr}\,1)$, so
$\varphi(\hat{w} \bullet (p,y)) = \mathrm{act}(1)$ applied to the underlying value of
$f_c(y) \bullet p$ — which is that value itself. For $y = \mathrm{inl}\,q$: the value is
$\mathrm{act}(c)(q) = \mathrm{act}(c)(\varphi(p, \mathrm{inl}\,q))$. For $y = \mathrm{inr}\,n$
and $p = \mathrm{act}(c)(x)$: writing $cnc = b'c$ for the chosen right factorization baked into
localActHom, the value is $\mathrm{act}(b')(p) = \mathrm{act}(b'c)(x) = \mathrm{act}(cnc)(x) = \mathrm{act}(c)(\mathrm{act}(n)(\mathrm{act}(c)(x))) = \mathrm{act}(c)(\varphi(p, \mathrm{inr}\,n))$ — the chosen $b'$ drops out because the displayed value $\mathrm{act}(cnc)(x)$
is determined by $cnc$ alone. Direct computation.
Main decomposition: the closure divides local-divisor wreath extension. Let $M$ be a
monoid with decidable equality, $Q$ a nonempty type,
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$, $A$ a finite generating set of $M$
($\texttt{Submonoid.closure}\,A = \top$), $c \in M$, and $N \le M$ a submonoid containing
$A \setminus \{c\}$. Then the constants closure $\overline{(Q, M)}$ (closureMonoid) divides, as
a semigroup, the wreath product
$\overline{(cQ, M_c)} \wr_{Q \sqcup N} \overline{(Q \sqcup N, N)}$ of cover_const_end. This is
a left-action, semigroup-division variant of DKS Theorem 3.1, using cM ∩ Mc;
$c \in A$ is not needed (if $c \notin A$, family 3 is simply unused). No
injectivity of $\mathrm{act}$ is needed here.
Proof sketch. Apply sgdiv_of_covering with the decoding $\varphi$ of dksProj — surjective
by dks_proj_surjective ($Q$ nonempty) — and the generating set
$\mathrm{act}(A) \cup \{\overline{x}\}$ of the closure, which generates by closure_monoid_gen
at the hypothesis $\langle A \rangle = \top$. Coverage of the generators: constants
$\overline{x}$ by cover_const_end; $\mathrm{act}(a)$ for $a \in A$, $a \ne c$ by
cover_act_of_mem applied at the member of $N$ that the containment hypothesis produces from
$a$; and $\mathrm{act}(c)$ by cover_act_c.
The group case (DKS Lemma 2.9) #
The decoding surjection of the group case. For a group $G$ and a monoid homomorphism $\mathrm{act} \colon G \to^* \mathrm{End}(Q)$, the map $\varphi \colon Q \times G \to Q$, $\varphi(q, g) = \mathrm{act}(g)(q)$. It is surjective since $\varphi(q, 1) = q$. This is the decoding of DKS Lemma 2.9.
Equations
- LeanPool.KrohnRhodes.groupProj act s = act s.2 s.1
Instances For
Group-case cover family 1: group translations are covered. In the wreath product
$U(Q) \wr_G G$ — decoration the reset submonoid resetSubmonoid acting on $Q$ by evaluation,
base $G$ acting on itself by left multiplication — every $\mathrm{act}(g) \in \mathrm{End}(Q)$,
$g \in G$, is covered (Covers) with respect to the decoding groupProj. (DKS Lemma 2.9,
appendix, cover $(k_1, g)$.)
Proof sketch. Take $\hat{w} := (\lambda m.\,1,\ g)$ (trivial decoration, base $g$). Then $\hat{w} \bullet (q, m) = (q, g m)$ and $\varphi = \mathrm{act}(gm)(q) = \mathrm{act}(g)(\mathrm{act}(m)(q)) = \mathrm{act}(g)(\varphi(q,m))$ by multiplicativity. Direct computation.
Group-case cover family 2: constants are covered (uses inverses). In the wreath product
of cover_act_group, every constant $\overline{x} \in \mathrm{End}(Q)$, $x \in Q$, is covered
(Covers) with respect to the decoding groupProj. This is the only place in the whole
construction where invertibility is used (DKS Lemma 2.9, appendix, cover $(f_x, 1)$ with
$h f_x = x \cdot h^{-1}$, adapted to left actions).
Proof sketch. Take $\hat{w} := (f_x, 1)$ with decoration $f_x(m) := \overline{\, \mathrm{act}(m^{-1})(x)\,}$ (a constant of $\mathrm{End}(Q)$, hence in the reset submonoid). Then $\hat{w} \bullet (q, m) = (\mathrm{act}(m^{-1})(x),\ m)$ and $\varphi = \mathrm{act}(m)(\mathrm{act}(m^{-1})(x)) = \mathrm{act}(m m^{-1})(x) = x = \overline{x}(\varphi(q,m))$ — the group inverse cancels. Direct computation.
Group case: the closure of a group representation divides resets wreath G. Let $G$ be a
group and $\mathrm{act} \colon G \to^* \mathrm{End}(Q)$ a monoid homomorphism (no faithfulness
needed). Then the constants closure $\overline{(Q, G)}$ (closureMonoid) divides, as a
semigroup, the wreath product $U(Q) \wr_G G$ of cover_act_group (reset decoration over the left
regular base). This is DKS Lemma 2.9.
Proof sketch. Apply sgdiv_of_covering with the decoding groupProj, surjective because
$\varphi(q, 1) = \mathrm{act}(1)(q) = q$, and the DEFINING generating set
$\mathrm{range}(\mathrm{act}) \cup \{\overline{x}\}$ of the closure (closureMonoid is literally
the closure of this set, so the generation hypothesis is definitional and no generating-set
transport is needed). Coverage: $\mathrm{act}(g)$ by cover_act_group; constants by
cover_const_group.
The induction on |M| (DKS Corollary 3.2) #
A submonoid divides its ambient monoid. For every submonoid $N$ of a monoid $M$, the
subtype monoid $N$ divides $M$ in the sense of MonoidDivides (a
surjective monoid homomorphism from a submonoid of $M$ onto $N$). Used by dks_aux to transport
the simple-group divisibility guarantee from the recursive base factor $(Q \sqcup N, N)$ up to
$M$.
Proof sketch. Witness: the submonoid $N$ itself with the identity homomorphism, which is surjective onto the subtype.
Every finite monoid has a minimal finite generating set. Every finite monoid $M$ (with decidable equality) has a finite generating set $A$ ($\texttt{Submonoid.closure}\,A = \top$) that is $\subseteq$-minimal in the strong sense that no single generator can be dropped: for every $a \in A$, $\texttt{Submonoid.closure}\,(A \setminus \{a\}) \ne \top$. (Folklore.)
Proof sketch. $\texttt{Finset.univ}$ generates ($1$ and all of $M$ are in the closure). Among
all generating finsets pick one of minimal cardinality (strong induction on Finset.card, or
well-foundedness of $<$ on $\mathbb{N}$): if some $a \in A$ could be dropped with
$\langle A \setminus \{a\} \rangle = \top$, the erased set would be a strictly smaller generating
finset, contradicting minimality.
A non-group monoid has a non-unit in every generating set. Let $M$ be a monoid, $A$ a finite generating set ($\texttt{Submonoid.closure}\,A = \top$), and suppose $M$ is not a group: some $m \in M$ is not a unit. Then some $c \in A$ is not a unit. (Folklore.)
Proof sketch. Contrapositive: if every element of $A$ is a unit, then every element of the
closure is a unit, by Submonoid.closure_induction — $1$ is a unit and units are closed under
multiplication (IsUnit.mul); since the closure is all of $M$, this contradicts the non-unit
$m$.
A proper submonoid of a finite monoid is strictly smaller. For a finite monoid $M$ and a
submonoid $N \ne \top$, $\mathrm{Nat.card}\,N < \mathrm{Nat.card}\,M$. Applied by dks_aux to
$N = \langle A \setminus \{c\} \rangle$, proper by the minimality clause of
exists_minimal_generating, to make the second recursive call decrease.
Proof sketch. $N \ne \top$ makes the carrier set of $N$ a proper subset of the universe set
of $M$ (Set.ssubset_univ_iff; carrier-set equality converts back to $N = \top$ via
SetLike.coe_set_eq and Submonoid.coe_top). A proper subset of a finite set has strictly
smaller cardinality (Set.Finite.card_lt_card at Set.finite_univ), and Nat.card_univ
identifies $\mathrm{Nat.card}\,(\mathrm{Set.univ})$ with $\mathrm{Nat.card}\,M$.
Group dispatch: the closure tower for an all-units monoid. Let $Q$ be a finite type, $M$
a finite monoid all of whose elements are units, and
$\mathrm{act} \colon M \to^* \mathrm{End}(Q)$ a monoid homomorphism. Then there is a factor list
(KRFactor factors at universe $0$) giving the constants closure
$\overline{(Q,M)}$ (closureMonoid) a recursive division tower (DivTowerWreath), with every
simple-group factor
dividing $M$ (MonoidDivides). The aperiodic factors — here a single
reset factor — are unconstrained. (DKS Cor 3.2, group case = Lemma 2.9 + Cor 2.8; Cor 2.8 is
replaced here by group_subquotient_faithful_aux, whose tower has all factors dividing the
group.)
Proof sketch. Endow $M$ with its group structure (groupOfIsUnit, definitionally extending the
given monoid). group_decomposition gives $\overline{(Q,M)} \preceq U(Q) \wr_M M$. The
decoration contributes the single aperiodic factor $\texttt{KRFactor.ofAperiodic}$ of the reset
submonoid — genuinely aperiodic by reset_submonoid_aperiodic — with its one-rung tower
(divTowerWreath_ofAperiodic). The base $M$ has the group tower
group_subquotient_faithful_aux (at $n = \mathrm{Nat.card}\,M$), whose factorsDivide
field already gives every factor (in particular every simple-group factor) dividing $M$. Assemble
with divTowerWreath_wreathStep: factors $:=$ reset factor $::$ group tower; the simple-group
factors all sit in the tail.
The DKS induction: closure towers with group factors dividing M. For every $n$, every
finite type $Q$, every finite monoid $M$ with $\mathrm{Nat.card}\,M \le n$, and every INJECTIVE
monoid homomorphism $\mathrm{act} \colon M \to^* \mathrm{End}(Q)$: there is a factor list giving
the constants closure $\overline{(Q,M)}$ (closureMonoid) a recursive division tower
(DivTowerWreath), with every
simple-group factor dividing $M$. The motive is stated over
closures, as in DKS, so that both recursive calls return exactly the decoration and base of the
main decomposition; the induction is on the monoid size only, never the state set (DKS Cor 3.2).
Proof sketch. Induction on the bound $n$ (the Nat.rec pattern of
group_subquotient_faithful_aux); the base $n = 0$ is vacuous, since a finite monoid is
nonempty and so has positive cardinality. DEGENERATE CASE ($Q$ subsingleton, covering
$Q = \emptyset$ and $|Q| = 1$): $\mathrm{End}(Q)$ is a subsingleton, hence so is the closure, and
the empty tower works (divTowerWreath_nil_of_subsingleton); the divisibility condition is
vacuous. GROUP CASE (every element a unit): dks_aux_group. NON-GROUP CASE ($Q$ nontrivial,
hence nonempty; some non-unit exists): choose a minimal generating finset $A$ by
exists_minimal_generating and a non-unit $c \in A$ by exists_nonunit_generator; set
$N := \langle A \setminus \{c\} \rangle$, proper by minimality, so
$\mathrm{Nat.card}\,N < \mathrm{Nat.card}\,M$ by card_lt_of_proper; also
$\mathrm{Nat.card}\,M_c < \mathrm{Nat.card}\,M$ by local_divisor_card_lt. Apply the inductive
hypothesis twice: at $(cQ,\ M_c,\ \mathrm{localActHom})$ — injective by local_act_injective
(here the faithfulness hypothesis is consumed), the $cQ$ Fintype instance by Fintype.ofFinite —
yielding a tower for the decoration closure with simple-group factors dividing $M_c$, hence
dividing $M$ through LocalDivisor.localDivides and MonoidDivides.trans; and at
$(Q \sqcup N,\ N,\ \mathrm{extAct})$ — injective by ext_act_injective — yielding a tower for
the base closure with simple-group factors dividing $N$, hence dividing $M$ through
submonoid_divides and MonoidDivides.trans. main_decomposition (at the containment
$A \setminus \{c\} \subseteq N$ by Submonoid.subset_closure) gives
$\overline{(Q,M)} \preceq \overline{(cQ, M_c)} \wr \overline{(Q \sqcup N, N)}$, and
divTowerWreath_wreathStep concatenates the two towers: factors $:=$ decoration tower $++$ base
tower.
The main theorem: a variant of the DKS decomposition #
A recursive wreath-division tower with aperiodic or simple-group factors, where every simple-group factor is a monoid divisor of the original monoid. Aperiodic factors have no additional restriction. This is the aperiodic/simple-group variant described in the module header, at universe 0.
The explicit list of aperiodic or simple-group factors.
- divides : DivTowerWreath M self.factors
The recursive wreath-division tower for
Moverfactors. - groupFactorsDivide (F : KRFactor) : F ∈ self.factors → F.kind = KRFactorKind.simpleGroup → MonoidDivides F.carrier M
Every SIMPLE-GROUP factor divides
M(the Krohn-Rhodes prime-divisor guarantee; aperiodic factors are only required to be aperiodic).
Instances For
Every finite monoid in universe 0 has a recursive wreath-division tower with finite aperiodic or finite simple-group factors, and every simple-group factor divides the original monoid. This is the variant described in the module header, not the flip-flop or transformation-monoid conclusion of DKS Theorem 4.1.
The proof applies dks_aux to the faithful left regular action and pulls its tower back from
the constants closure using sgdiv_closure_monoid.
A chosen factor tower #
The chosen Krohn-Rhodes factor tower of a finite monoid. For a finite monoid $M$, a
chosen factor tower with the prime-divisor guarantee (KRFactorTowerGrp), extracted from the
existence theorem krohn_rhodes_prime_decomposition by Nonempty.some.