The abelianization of the unrestricted group: the free part and the order-two part (Proposition 4.6)
DisprovedFRV.uuv_abelianizationThe abelianization of the universal unrestricted virtual braid group is the direct sum of the free Abelian group of rank k with the cyclic group of order two. All virtual generators of a given family share one class in the abelianization, all sigma generators of a given type share one free class, and the forbidden relations impose no additional relation on the abelianization beyond the order-two identification of the virtual class. This is Proposition 4.6 of the paper.
import Mathlib import Definitions.Def_FRV_alg import Definitions.Def_FRV_tor
namespace FRV
/-! Milestone 7 (Proposition 4.6): the abelianization of the universal
unrestricted virtual braid group is the direct sum of the free Abelian
group of rank k with the cyclic group of order two. All virtual generators
of a given family share one class in the abelianization, all sigma
generators of a given type share one free class, and the forbidden
relations impose no additional relation on the abelianization. -/
theorem uuv_abelianization {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 : 3 ≤ n) :
∃ ab : U →* Multiplicative ((Fin k → ℤ) × ZMod 2),
(∀ y : Multiplicative ((Fin k → ℤ) × ZMod 2), ∃ x : U, ab x = y) ∧
MonoidHom.ker ab = Derived U := by sorry
end FRV
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a forbidden-relations world with at least three strands, there exists a homomorphism from the unrestricted quotient onto the multiplicative twin of the product of the integer-valued functions on the family indices with the integers modulo two, whose kernel is the derived subgroup. Hypotheses: the world is given; the number of strands is at least three; no further hypotheses appear.