The two twin-welded forbidden relations are equivalent (Remark 2.2 (2))
ProvedMWT.second_forbiddenIn the multi-welded twin group, the two twin-welded forbidden relations are equivalent: the product of the two adjacent twin generators with the virtual generator of any family in the first position equals the product with the virtual generator in the last position. The equivalence follows by taking inverses in the welded relation and using that all the generators are involutions: each factor is its own inverse. This is the observation of Remark 2.2 (2) of the paper, which shows that the presentation of Definition 2.1 admits the second forbidden relation as a derived relation.
import Mathlib import Definitions.Def_MWT_alg import Definitions.Def_MWT_tor
namespace MWT
/-! Milestone 1 (Remark 2.2 (2)): the two twin-welded forbidden relations
are equivalent in the multi-welded twin group. Taking inverses in the
welded relation (2.9) and using that all generators are involutions yields
the second forbidden relation s_i s_(i+1) rho_i^(alpha) =
rho_(i+1)^(alpha) s_i s_(i+1). -/
theorem second_forbidden {n k : ℕ} {G UW : Type*} [Group G] [Group UW]
(W : MultiWeldedTwinWorld n k G UW) (α : Fin k) (i : ℕ) (hi : i + 3 ≤ n) :
W.s ⟨i, by omega⟩ * W.s ⟨i + 1, by omega⟩ * W.rho α ⟨i, by omega⟩
= W.rho α ⟨i + 1, by omega⟩ * W.s ⟨i, by omega⟩ * W.s ⟨i + 1, by omega⟩ := 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, for every family index and every adjacent pair of twin generators, the product of the first twin generator, the second twin generator, and the virtual generator of the family in the first position equals the product of the shifted virtual generator and the two twin generators in the reverse order. Hypotheses: the world is given; the index satisfies the adjacency bound; no further hypotheses appear.