The commutator subgroup is perfect for n at least five (Theorem 2.7 (ii))
DisprovedMWT.commutator_perfectFor n at least five, the commutator subgroup of the multi-welded twin group is perfect: the derived subgroup of the derived subgroup is the whole derived subgroup. The rigidity of the universal welded framework descends to the involutive quotient, and every commutator of two elements of the commutator subgroup is again a product of commutators of elements of the commutator subgroup. This is Theorem 2.7 (ii) of the paper.
import Mathlib import Definitions.Def_MWT_alg import Definitions.Def_MWT_tor
namespace MWT
/-! Milestone 5 (Theorem 2.7 (ii)): for n at least five, the commutator
subgroup of the multi-welded twin group is perfect - the derived subgroup
of the derived subgroup is everything. The rigidity of the universal
welded framework descends to the involutive quotient. -/
theorem commutator_perfect {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
(W : MultiWeldedTwinWorld n k G UW) (hn : 5 ≤ n) :
DerivedPerfect G := by sorry
end MWT
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a multi-welded twin world with at least five strands, the derived subgroup of the derived subgroup of the group equals the whole derived subgroup. Hypotheses: the world is given; the number of strands is at least five; no further hypotheses appear.