The algebraic layer: involutions, derived subgroups, and finite quotients
DefinitionFRV_algThe algebraic interface of the forbidden-relations theory of the paper. The definition carries: the involution predicate for automorphisms - an automorphism is involutive when its square is the identity, the property shared by theta and the automorphisms zeta_l of Theorem 2.1; the derived subgroup of a group as the subgroup generated by the commutators of pairs of elements, with the perfectness predicate - the derived subgroup of the derived subgroup is the whole derived subgroup - through which Proposition 4.7 and Corollary 4.9 are expressed; and the predicate that every finite quotient of order strictly below a given bound is Abelian, through which the smallest non-Abelian finite quotient is expressed, with the symmetric group of order n! as the witnessing quotient.
import Mathlib
/-!
# The algebraic layer: involutions, derived subgroups, and finite quotients
The algebraic layer of the FRV mission, carrying the interface of Oscar
Ocampo and Charalampos Stylianakis, "Forbidden relations in universal virtual
braid groups" (arXiv:2606.06095, 2026): the involution predicate for
automorphisms used in Theorem 2.1, the derived subgroup of a group as the
subgroup generated by the commutators with the perfectness predicate used
in Proposition 4.7 and Corollary 4.9, and the predicate that every finite
quotient of order below a given bound is Abelian, through which the
smallest non-Abelian finite quotient is expressed.
-/
namespace FRV
/-- The automorphism phi is an involution: its square is the identity. -/
def IsInvolutive {G : Type*} [Group G] (phi : G ≃* G) : Prop :=
∀ x : G, phi (phi x) = x
/-- The derived subgroup of G: the subgroup generated by all commutators
of pairs of elements. -/
def Derived (G : Type*) [Group G] : Subgroup G :=
Subgroup.closure {x | ∃ a b : G, a * b * a⁻¹ * b⁻¹ = x}
/-- Every finite quotient of G of order strictly less than m is Abelian.
With the symmetric group of order n! as the witnessing non-Abelian
quotient, this expresses that S_n is the smallest non-Abelian finite
quotient. -/
def FiniteQuotientsAbelianBelow (G : Type*) [Group G] (m : ℕ) : Prop :=
∀ (F : Type) [inst : Group F] [Fintype F] (q : G →* F),
Fintype.card F < m → ∀ x y : F, x * y = y * x
end FRV