The unrestricted group splits over its pure subgroup (Proposition 4.5)
DisprovedFRV.uuv_splitsThe universal unrestricted virtual braid group splits as the semidirect product of its pure subgroup with the symmetric group. The permutation epimorphism onto the symmetric group admits a group-theoretic section carrying each transposition to the class of the corresponding virtual generator, so the pure sequence of the unrestricted setting splits. This is Proposition 4.5 of the paper.
import Mathlib import Definitions.Def_FRV_alg import Definitions.Def_FRV_tor
namespace FRV
/-! Milestone 6 (Proposition 4.5): the universal unrestricted virtual
braid group splits as the semidirect product of its pure subgroup with the
symmetric group. The permutation epimorphism onto the symmetric group
admits a group-theoretic section, carrying each transposition to the class
of the corresponding virtual generator. -/
theorem uuv_splits {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) :
∃ sec : Equiv.Perm (Fin n) →* U, ∀ p : Equiv.Perm (Fin n), W.uuvPerm (sec p) = p := 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 symmetric group on the strands to the unrestricted quotient such that the permutation of the image of any permutation is that permutation. Hypotheses: the world is given; the number of strands is at least three; no further hypotheses appear.