The generator families collapse in the abelianization

Proved

MWT.abelian_families_collapse

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

abelianizationtwin-groupswelded-groups

In the abelianization of the multi-welded twin group, each generator family collapses to a single class: the classes of all the twin generators coincide - the MR2-type relations identify the classes of adjacent twin generators - and, within each virtual family, the classes of all the virtual generators coincide - the mixed relations identify the classes of adjacent virtual generators. The abelianization is therefore generated by the class of one twin generator and the classes of one virtual generator from each of the k families.

Preamble

import Mathlib
import Definitions.Def_MWT_alg
import Definitions.Def_MWT_tor

Formal statement

namespace MWT

/-!  Milestone 3: in the abelianization of the multi-welded twin group,
each generator family collapses to a single class. The MR2-type relations
(2.5) identify the classes of s_i and s_(i+1), and the mixed relations
identify the classes of the virtual generators of each family, so the
abelianization is generated by the class of one twin generator and the
classes of one generator from each virtual family. -/
theorem abelian_families_collapse {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
    (W : MultiWeldedTwinWorld n k G UW) :
    (∀ i j : Fin (n - 1), Abelianization.of (W.s i) = Abelianization.of (W.s j)) ∧
    (∀ (α : Fin k) (i j : Fin (n - 1)),
      Abelianization.of (W.rho α i) = Abelianization.of (W.rho α j)) := by sorry

end MWT

Source

M. N. Nasser, O. Ocampo, Multi-welded twin groups, arXiv:2605.31298 (2026), Section 2 (the first step of the proof of Theorem 2.7 (i)).

Read-back

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

Restate: in a multi-welded twin world, the images of all the twin generators in the abelianization are equal to each other, and, for each family index, the images of all the virtual generators of that family are equal to each other. Hypotheses: the world is given; no further hypotheses appear.

View graph