The abelianization is the elementary Abelian 2-group of rank k+1 (Theorem 2.7 (i))
DisprovedMWT.abelianization_isoThe abelianization of the multi-welded twin group is the elementary Abelian 2-group of rank k+1. The k+1 collapsed classes - the class of the twin generators and the classes of the k virtual families - are each of exponent two, by the involutivity of the generators, and they form a basis: the abelianization is multiplicatively equivalent to the group of (k+1)-tuples of bits under pointwise addition. This is Theorem 2.7 (i) of the paper.
import Mathlib import Definitions.Def_MWT_alg import Definitions.Def_MWT_tor
namespace MWT
/-! Milestone 4 (Theorem 2.7 (i)): the abelianization of the multi-welded
twin group M_kWT_n is the elementary Abelian 2-group of rank k+1: the
classes of the collapsed families, each of exponent two, form a basis. -/
theorem abelianization_iso {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
(W : MultiWeldedTwinWorld n k G UW) :
Nonempty (Abelianization G ≃* Multiplicative (Fin (k + 1) → ZMod 2)) := 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, the abelianization of the group is multiplicatively equivalent to the multiplicative twin of the additive group of functions from a set of k+1 elements to the integers modulo two. Hypotheses: the world is given; no further hypotheses appear.