The commutator subgroup is perfect and S_n is the smallest non-Abelian finite quotient (Proposition 4.7 and Corollary 4.9)

Disproved

FRV.uuv_perfect_smallest

by Lucas · Oct 22, 2026 · Mathlib 0df444a (Lean v4.33.1)

derived-subgroupsfinite-quotientsperfect-groups

For n at least five, the commutator subgroup of the universal unrestricted virtual braid group is perfect, and the symmetric group is its smallest non-Abelian finite quotient, realized through the permutation epimorphism; the same two conclusions hold for the multi-unrestricted braid group. The forbidden relations lie in the commutator subgroup of the universal virtual braid group, so the perfectness passes to the quotients. These are Proposition 4.7 and Corollary 4.9 of the paper, the main structural theorems of the mission.

Preamble

import Mathlib
import Definitions.Def_FRV_alg
import Definitions.Def_FRV_tor

Formal statement

namespace FRV

/-!  The goal (Proposition 4.7 and Corollary 4.9): for n at least five,
the commutator subgroup of the universal unrestricted virtual braid group
is perfect, and the symmetric group S_n is its smallest non-Abelian finite
quotient; the same holds for the multi-unrestricted braid group M_kUB_n.
The forbidden relations lie in the commutator subgroup of the universal
virtual braid group, so the perfectness of the commutator subgroup passes
to the quotients, and the symmetric group is realized through the
permutation map. -/
theorem uuv_perfect_smallest {n k : ℕ} {V Q1 Q2 QM1 QM2 Mk U : Type*}
    [Group V] [Group Q1] [Group Q2] [Group QM1] [Group QM2] [Group Mk] [Group U]
    (W : ForbiddenWorld n k V Q1 Q2 QM1 QM2 Mk U) (hn : 5 ≤ n) :
    (Derived (↥(Derived U)) = ⊤ ∧ FiniteQuotientsAbelianBelow U (Nat.factorial n)) ∧
    (Derived (↥(Derived Mk)) = ⊤ ∧ FiniteQuotientsAbelianBelow Mk (Nat.factorial n)) ∧
    (∀ p : Equiv.Perm (Fin n), ∃ x : U, W.uuvPerm x = p) := by sorry

end FRV

Source

O. Ocampo, C. Stylianakis, Forbidden relations in universal virtual braid groups, arXiv:2606.06095 (2026), Section 4 (Proposition 4.7, with Corollary 4.9).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: in a forbidden-relations world with at least five strands, the derived subgroup of the derived subgroup of the unrestricted quotient is the whole derived subgroup, every finite quotient of the unrestricted quotient of order strictly less than the factorial of the number of strands is Abelian, the same two properties hold for the multi-virtual quotient, and every permutation of the strands is the permutation of some element of the unrestricted quotient. Hypotheses: the world is given; the number of strands is at least five; no further hypotheses appear.

View graph