The world layer: the idealized braid quotient as a crystallographic group
DefinitionBQC_torThe world layer of the braid quotient problem. The definition carries: the idealized quotient of the Artin braid group on n strings by the commutator subgroup of its pure braid group, which by Proposition 1 is a crystallographic group of dimension n(n-1)/2 - the rank of the abelianization of the pure braid group - whose holonomy group is the permutation layer, carried as an abstract crystallographic world of that dimension; and the realization predicate for an abstract finite group over the permutation layer - given by an embedding into it - recording when the group is realized by a subgroup of the quotient, that is, when the embedding lifts to a homomorphism into the quotient that commutes with the projections and is injective, as in Corollary 4 and Theorem 6.
import Mathlib
import Definitions.Def_BQC_alg
/-!
# The world layer: the idealized braid quotient as a crystallographic group
The world layer of the BQC mission: the idealized quotient of the Artin
braid group on n strings by the commutator subgroup of its pure braid group,
which by Proposition 1 is a crystallographic group of dimension n(n - 1)/2
whose holonomy group is the permutation layer; and the realization predicate
for an abstract finite group over the permutation layer, recording when a
finite subgroup of the permutation layer is realized by a subgroup of the
quotient, as in Corollary 4 and Theorem 6.
-/
namespace BQC
/-- The idealized world of the quotient of the Artin braid group on n strings
by the commutator subgroup of its pure braid group: by Proposition 1 it is a
crystallographic group of dimension n(n - 1)/2 - the rank of the abelianization
of the pure braid group - whose holonomy group is the permutation layer S. -/
abbrev BraidQuotient (n : Nat) (Q S : Type*) [Group Q] [Group S] [Fintype S] :=
CryWorld (Nat.choose n 2) Q S
/-- The abstract finite group H over the permutation layer - given by an
embedding into S - is realized by a subgroup of the braid quotient: there is a
lift of the embedding to Q that commutes with the projections. This is the
realization of isomorphism classes of subgroups of the permutation layer by
subgroups of the quotient, as in Corollary 4 and Theorem 6. -/
def LiftsOver {n : Nat} {Q S : Type*} [Group Q] [Group S] [Fintype S]
{H : Type} [Group H] [Fintype H]
(W : BraidQuotient n Q S) (i : H →* S) : Prop :=
∃ f : H →* Q, (∀ h : H, W.proj (f h) = i h) ∧ (∀ x y : H, f x = f y → x = y)
end BQC
BraidQuotient n Q S := CryWorld (Nat.choose n 2) Q S carries no information about the braid group: S is any finite group, Q is any group with a short exact sequence from the rank n(n−1)/2 lattice onto S with faithful holonomy, and nothing ties the extension class or the holonomy action to the symmetric group acting on the basis A_{i,j} of P_n/[P_n,P_n] as in equation (8) of the paper. Kernel checked counterexamples accepted on the platform: for n = 3 the split world Z^3 ⋊ Z/2 with Z/2 acting by negation is a BraidQuotient 3 and contains an element of order 2 (refutes BQC.no_even_torsion); the subgroup T of Z^3 ⋊ Z/3 of pairs (z, g) with z_2 ≡ g mod 3, with lattice embedded through (a, b, c) ↦ (a, b, 3c), is a BraidQuotient 3 in which the generator of Z/3 has no preimage of order 3 (refutes BQC.odd_permutations_lift, BQC.lcm_orders and the goal); the split world Z^3 ⋊ Z/3 contains the elements (0, t) and ((1,0,0), t) of order 3 with the same projection that are not conjugate (refutes BQC.conjugacy_cycle_type); and the identity of Z/3 lifts to no injective compatible homomorphism from the split world to T (refutes BQC.product_inclusion). Proposition 1 of the paper is not a definition of the quotient and cannot be replaced by an abstract world. A concrete definition is available in Mathlib: let B n be the PresentedGroup on n − 1 generators with the Artin relations, let P n be the kernel of the homomorphism B n →* Equiv.Perm (Fin n) sending the i th generator to the transposition (i, i+1), and let the quotient be B n ⧸ ⁅P n, P n⁆, which is a group since ⁅P n, P n⁆ is normal; the platform already carries BraidsLinksMCG.artinBraidGroup_equiv_artinTits identifying such a presentation with the Artin Tits group of type A.