The finite Abelian subgroups of the quotient correspond to the odd Abelian subgroups of the permutation layer (Theorem 6)

Disproved

BQC.abelian_subgroups_correspondence

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

abelian-groupsbraid-groupscrystallographic-groups

There is a one-to-one correspondence between the isomorphism classes of the finite Abelian subgroups of the braid quotient and the isomorphism classes of the Abelian subgroups of the permutation layer of odd order. Every finite Abelian group of odd order embedded in the permutation layer is realized by a subgroup of the quotient - the lift of the embedding of Corollary 4 extended from the cyclic to the Abelian groups, following the invariant of Hoffman cited as [11] in the source paper - and every finite Abelian subgroup of the quotient has odd order, so by Lemma 9 it embeds isomorphically into the permutation layer. This is Theorem 6 of the source paper, the goal of the mission.

Preamble

import Mathlib
import Definitions.Def_BQC_alg
import Definitions.Def_BQC_tor

Formal statement

namespace BQC

/-!  The goal (Theorem 6): there is a one-to-one correspondence between the
isomorphism classes of the finite Abelian subgroups of the braid quotient and
the isomorphism classes of the Abelian subgroups of the permutation layer of
odd order. Every finite Abelian group of odd order embedded in the
permutation layer is realized by a subgroup of the quotient - the lift of the
embedding of Corollary 4 extended to Abelian subgroups - and every finite
Abelian subgroup of the quotient has odd order, so by Lemma 9 it embeds
isomorphically into the permutation layer. -/
theorem abelian_subgroups_correspondence {n : Nat} {Q S : Type*} [Group Q] [Group S] [Fintype S]
    (W : BraidQuotient n Q S) (hn : 3 ≤ n) :
    (∀ (H : Type) [Group H] [Fintype H] [CommGroup H] (i : H →* S)
        (hi : ∀ x y : H, i x = i y → x = y) (hodd : Odd (Fintype.card H)), LiftsOver W i) ∧
    (∀ (H : Type) [Group H] [Fintype H] [CommGroup H] (f : H →* Q)
        (hf : ∀ x y : H, f x = f y → x = y), Odd (Fintype.card H)) := by sorry

end BQC

Source

D. L. Goncalves, J. Guaschi, O. Ocampo, A quotient of the Artin braid groups related to crystallographic groups, Journal of Algebra 474 (2017) 393-423, Section 6 (Theorem 6).

Read-back

What the Lean code literally says, in plain math · glm-5-latest-short

Restate: two conjuncts for the braid quotient world on n strings with n at least three. First, every finite Abelian group H of odd order, embedded injectively into the permutation layer, is realized: the embedding lifts to a homomorphism into the quotient that commutes with the projections and is injective. Second, every finite Abelian group embedded injectively into the quotient has odd order. Hypotheses: n is at least three; the groups are Abelian; the embeddings are injective; in the first conjunct the order of H is odd.

Human review

Flagged by Shuze Chen · Oct 23, 2026
The statement quantifies over every BraidQuotient n Q S with 3 ≤ n and is false: the accepted disproof takes n = 3 and the non split world T described under BQC_tor, embeds Z/3 into the holonomy group by the identity, and shows that LiftsOver fails because no element of T projecting to the generator has order 3. Theorem 6 of the paper concerns B_n/[P_n,P_n] with holonomy S_n and is proved through the explicit elements δ of Section 6 and Hoffman's invariant; its truth depends on the specific group and cannot be recovered from the characterization of Lemma 8 alone. The statement must be made against a definition of the braid quotient itself, with S replaced by Equiv.Perm (Fin n).

View graph