The world layer: the idealized universal virtual braid group

Definition

FRV_tor

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

forbidden-relationsquotient-groupsuniversal-braid-groupsvirtual-braids

The idealized world of the forbidden-relations problem. The definition carries: the universal virtual braid group with its generator families rho and sigma - one sigma family per crossing type; the normal subgroups generated by the two families of forbidden relations (F1) and (F2) and by the multi-virtual relations; the quotient groups with their projections - the one-forbidden quotients, their multi-virtual refinements, the multi-virtual braid group, and the universal unrestricted virtual braid group, the last obtained by imposing both forbidden families simultaneously; the involutive automorphisms theta and zeta_l given by their values on the generators - theta inverts every sigma generator and fixes the virtual generators, and zeta_l conjugates the l-th sigma family by the adjacent virtual generator and fixes the other families; and the permutation epimorphism of the unrestricted quotient onto the symmetric group. The definition also carries the subproduct machinery of Theorem 2.1: the product of the zeta automorphisms over a list of indices, optionally composed with theta.

Definition code

import Mathlib
import Definitions.Def_FRV_alg

/-!
# The world layer: the idealized universal virtual braid group

The world layer of the FRV mission: the idealized universal virtual braid
group UV_n(k) on n strings with k types of crossings of the source paper of
Oscar Ocampo and Charalampos Stylianakis. The world carries: the generator
families rho_i and sigma_(i,t); the normal subgroups generated by the two
families of forbidden relations (F1) and (F2) and by the multi-virtual
relations, with the corresponding quotient groups - the one-forbidden
quotients, their multi-virtual refinements, the multi-virtual braid group
M_kVB_n, and the universal unrestricted virtual braid group UUV_n(k) - as
abstract quotient types with their projections; the involutive
automorphisms theta and zeta_l of Theorem 2.1 given by their values on the
generators; and the permutation epimorphism of the unrestricted quotient.
-/

namespace FRV

/-- The idealized world of the forbidden-relations problem: the universal
virtual braid group V with its generators, the forbidden-relation normal
subgroups and the quotient groups with their projections, the involutive
automorphisms theta and zeta with their generator values, and the
permutation map of the unrestricted quotient. -/
structure ForbiddenWorld (n k : ℕ)
    (V Q1 Q2 QM1 QM2 Mk U : Type*)
    [Group V] [Group Q1] [Group Q2] [Group QM1] [Group QM2] [Group Mk] [Group U] where
  rho : Fin (n - 1) → V
  sigma : Fin (n - 1) → Fin k → V
  hk : 0 < k
  N1 : Subgroup V
  N2 : Subgroup V
  NM : Subgroup V
  N1normal : N1.Normal
  N2normal : N2.Normal
  NMnormal : NM.Normal
  f1mem : ∀ (i : ℕ) (hi : i + 3 ≤ n) (t : Fin k),
    (rho ⟨i, by omega⟩ * sigma ⟨i + 1, by omega⟩ t * sigma ⟨i, by omega⟩ t
      * (sigma ⟨i + 1, by omega⟩ t * sigma ⟨i, by omega⟩ t * rho ⟨i + 1, by omega⟩)⁻¹) ∈ N1
  f2mem : ∀ (i : ℕ) (hi : i + 3 ≤ n) (t : Fin k),
    (rho ⟨i + 1, by omega⟩ * sigma ⟨i, by omega⟩ t * sigma ⟨i + 1, by omega⟩ t
      * (sigma ⟨i, by omega⟩ t * sigma ⟨i + 1, by omega⟩ t * rho ⟨i, by omega⟩)⁻¹) ∈ N2
  p1 : V →* Q1
  p1ker : MonoidHom.ker p1 = N1
  p1surj : ∀ y : Q1, ∃ x : V, p1 x = y
  p2 : V →* Q2
  p2ker : MonoidHom.ker p2 = N2
  p2surj : ∀ y : Q2, ∃ x : V, p2 x = y
  pm : V →* Mk
  pmker : MonoidHom.ker pm = NM
  pmsurj : ∀ y : Mk, ∃ x : V, pm x = y
  pm1 : V →* QM1
  pm1ker : MonoidHom.ker pm1 = NM ⊔ N1
  pm1surj : ∀ y : QM1, ∃ x : V, pm1 x = y
  pm2 : V →* QM2
  pm2ker : MonoidHom.ker pm2 = NM ⊔ N2
  pm2surj : ∀ y : QM2, ∃ x : V, pm2 x = y
  pu : V →* U
  puker : MonoidHom.ker pu = N1 ⊔ N2
  pusurj : ∀ y : U, ∃ x : V, pu x = y
  theta : V ≃* V
  thetaRho : ∀ i : Fin (n - 1), theta (rho i) = rho i
  thetaSigma : ∀ (i : Fin (n - 1)) (t : Fin k), theta (sigma i t) = (sigma i t)⁻¹
  zeta : Fin k → (V ≃* V)
  zetaRho : ∀ (l : Fin k) (i : Fin (n - 1)), zeta l (rho i) = rho i
  zetaSigma : ∀ (l : Fin k) (i : Fin (n - 1)) (t : Fin k),
    zeta l (sigma i t) = if t = l then rho i * sigma i t * rho i else sigma i t
  uuvPerm : U →* Equiv.Perm (Fin n)

/-- The product of the zeta automorphisms indexed by the list L. -/
def zetaProd {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) (L : List (Fin k)) : V ≃* V :=
  L.foldr (fun l e => (W.zeta l).trans e) (MulEquiv.refl V)

/-- The product of the zeta automorphisms indexed by the list L, composed
with theta when the flag eps is set. -/
def zetaApplied {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) (L : List (Fin k)) (eps : Bool) : V ≃* V :=
  if eps then (zetaProd W L).trans W.theta else zetaProd W L

end FRV

Source

O. Ocampo, C. Stylianakis, Forbidden relations in universal virtual braid groups, arXiv:2606.06095 (2026), Sections 2 and 3 (the generator framework, the forbidden relations, and the quotient groups).

View graph