The kernel of the universal welded epimorphism contains the generator squares (Proposition 2.3)

Proved

MWT.uw_kernel_squares

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

epimorphismsquotientswelded-groups

The canonical epimorphism from the universal welded braid group onto the multi-welded twin group kills the squares of all the generators: the squares of the non-virtual generators and the squares of the virtual generators all map to the identity, because every image - the twin generators and the virtual generators of every family - is an involution in the multi-welded twin group. The kernel of the epimorphism of Proposition 2.3 therefore contains the squares of all the generators, and the multi-welded twin group arises as the quotient by an involutivity imposition.

Preamble

import Mathlib
import Definitions.Def_MWT_alg
import Definitions.Def_MWT_tor

Formal statement

namespace MWT

/-!  Milestone 2 (Proposition 2.3): the canonical epimorphism from the
universal welded braid group UW_n(k) onto the multi-welded twin group
identifies the virtual generators with the distinguished virtual family,
the first k-1 non-virtual families with the remaining virtual families,
and the last non-virtual family with the twin generators; since all
images are involutions, the kernel contains the squares of all non-virtual
generators and of the virtual generators. -/
theorem uw_kernel_squares {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
    (W : MultiWeldedTwinWorld n k G UW) :
    ∀ (i : Fin (n - 1)) (t : Fin k),
      W.uw (W.uwSigma i t * W.uwSigma i t) = 1 ∧
      W.uw (W.uwRho i * W.uwRho i) = 1 := by sorry

end MWT

Source

M. N. Nasser, O. Ocampo, Multi-welded twin groups, arXiv:2605.31298 (2026), Section 2 (Proposition 2.3, the kernel content).

Read-back

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

Restate: in a multi-welded twin world, the image under the canonical epimorphism of the square of any non-virtual generator is the identity, and so is the image of the square of any virtual generator. Hypotheses: the world is given; no further hypotheses appear.

View graph