The algebraic layer: derived subgroups, perfectness, and finite quotients

import Mathlib

/-!
# The algebraic layer: derived subgroups and finite quotients

The algebraic layer of the MWT mission, carrying the interface of Mohamad
N. Nasser and Oscar Ocampo, "Multi-welded twin groups" (arXiv:2605.31298,
2026): the derived subgroup of a group as the subgroup generated by the
commutators, the perfectness predicate for the commutator subgroup used in
Theorem 2.7 (ii), and the predicate that every finite quotient of order
below a given bound is Abelian, through which the smallest non-Abelian
finite quotient of Theorem 2.7 (iii) and the finite quotient of order at
least 2^k n! of Theorem 2.7 (iv) are expressed.
-/

namespace MWT

/-- The derived subgroup of G: the subgroup generated by all commutators
of pairs of elements. -/
def Derived (G : Type*) [Group G] : Subgroup G :=
  Subgroup.closure {x | ∃ a b : G, a * b * a⁻¹ * b⁻¹ = x}

/-- The commutator subgroup of G is perfect: the derived subgroup of the
derived subgroup is the whole derived subgroup, the assertion of
Theorem 2.7 (ii) of the source paper. -/
def DerivedPerfect (G : Type*) [Group G] : Prop :=
  Derived (↥(Derived G)) = ⊤

/-- Every finite quotient of G of order strictly less than m is Abelian.
With the symmetric group of order n! as the witnessing non-Abelian
quotient, this expresses that S_n is the smallest non-Abelian finite
quotient, Theorem 2.7 (iii) of the source paper. -/
def FiniteQuotientsAbelianBelow (G : Type*) [Group G] (m : ℕ) : Prop :=
  ∀ (F : Type) [inst : Group F] [Fintype F] (q : G →* F),
    Fintype.card F < m → ∀ x y : F, x * y = y * x

end MWT