The least common multiple orders are realized in the larger quotient (Theorem 3(b))

Disproved

BQC.lcm_orders

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

braid-groupstorsion

The braid quotient on m strings possesses elements of every odd order realized by the smaller quotient: given the injective inclusion homomorphism of the quotients of Theorem 3(a), an element of odd exact order r of the smaller permutation layer lifts through the inclusion to an element of the same exact order in the larger quotient, whose projection is the embedded element. Together with Proposition 21 this constructs the elements of the least common multiple orders of Theorem 3(b), with the prescribed cycle type.

Preamble

import Mathlib
import Definitions.Def_BQC_alg
import Definitions.Def_BQC_tor

Formal statement

namespace BQC

/-!  Milestone 7 (Theorem 3(b)): the braid quotient on m strings possesses
elements of every odd order realized by the smaller quotient. Given the
injective inclusion homomorphism of the quotients of milestone 6, an element
of odd exact order r of the smaller permutation layer lifts through the
inclusion to an element of the same exact order in the larger quotient, whose
permutation has the corresponding cycle type. Together with Proposition 21
this constructs elements of the least common multiple orders of Theorem 3. -/
theorem lcm_orders {n m : Nat} {Q1 S1 Q2 S2 : Type*} [Group Q1] [Group S1] [Fintype S1]
    [Group Q2] [Group S2] [Fintype S2]
    (W1 : BraidQuotient n Q1 S1) (W2 : BraidQuotient m Q2 S2)
    (iS : S1 →* S2) (hiS : ∀ x y : S1, iS x = iS y → x = y)
    (iQ : Q1 →* Q2) (hcomm : ∀ q : Q1, W2.proj (iQ q) = iS (W1.proj q))
    (hiQ : ∀ x y : Q1, iQ x = iQ y → x = y)
    (th : S1) (r : Nat) (hr : ExactOrder r th) (hodd : Odd r) :
    ∃ b : Q2, ExactOrder r b ∧ W2.proj b = iS th := 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, Sections 1 and 4 (Theorem 3(b), with Proposition 21).

Read-back

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

Restate: given the two braid quotient worlds, an injective homomorphism of the permutation layers, an inclusion homomorphism of the quotients that commutes with the projections and is injective, and an element of the smaller permutation layer of odd exact order r, there is an element of the larger quotient of exact order r whose projection is the embedded element. Hypotheses: the inclusion homomorphism exists, commutes with the projections, and is injective; the element has exact order r; r is odd.

View graph