{"id":"palomar/PALOMAR-2026-09-30-000017","url":"https://github.com/adii800/krohn-rhodes-lean/tree/1f4a7e39ba2baede5434ac48c7571a442f8d521d","json":"https://data.palomar-registry.org/entries/PALOMAR-2026-09-30-000017-v1.json","repo":"https://github.com/adii800/krohn-rhodes-lean","tags":["math.GR","cs.FL","msc:20M10","msc:20M35","msc:20M20","msc:68Q70","group-theory","finite-monoids","krohn-rhodes","lean-formalization"],"score":0,"title":"Krohn–Rhodes decomposition of finite monoids into aperiodic and simple-group factors","trust":"high","domain":"math.GR","source":"palomar","authors":["Aditya Rao"],"reviews":0,"subject":"math.GR","summary":"A Lean 4 and Mathlib formalization of the Krohn–Rhodes prime decomposition theorem for finite monoids, in a form with aperiodic factors: every finite monoid M divides an iterated wreath product of finite monoids, each of which is aperiodic or a simple group, and every simple group among the factors divides M. The proof follows the local-divisor proof of Diekert, Kufleitner and Steinberg. Unlike the classical statement, the aperiodic factors are not reduced to copies of the three-element flip-flop monoid U₂; for an aperiodic M the statement holds with M as its only factor, and in general it…","category":"research","comments":0,"disputed":false,"division":"math","mentions":0,"verified":true,"discussed":0,"published":"2026-09-30","reactions":{},"formalized":true,"formalizes":[{"title":"Algebraic theory of machines. I. Prime decomposition theorem for finite semigroups and machines","identifier":"https://doi.org/10.1090/S0002-9947-1965-0188316-1","relationship":"adapts"},{"title":"The Krohn-Rhodes Theorem and Local Divisors","identifier":"arXiv:1111.1585v1","relationship":"adapts"}]}