The preimage of a two-power holonomy subgroup is Bieberbach (Proposition 2.5)
DisprovedCTB.preimage_bieberbachThe full preimage of a finite 2-group of holonomies is Bieberbach. If a subgroup of the symmetric group consists of elements of two-power order, then the preimage under the holonomy projection is torsion-free - the absence of even-order torsion in the braid quotient forces any torsion element into the translation lattice, where powers vanish only trivially - the holonomy projection maps the preimage back onto the subgroup, and the translation lattice is contained in it. This is Proposition 2.5 of the paper, the preimage lemma of the companion paper restated in the present setting.
import Mathlib import Definitions.Def_CTB_alg import Definitions.Def_CTB_tor
namespace CTB
/-! Milestone 1 (Proposition 2.5): the full preimage of a finite
2-group of holonomies is Bieberbach. If H is a subgroup of the symmetric
group all of whose elements are of two-power order, then the preimage of
H under the holonomy projection is torsion-free - a Bieberbach group -
and the holonomy projection maps this preimage back onto H, while the
translation lattice is contained in it. -/
theorem preimage_bieberbach {n : ℕ} {Q : Type*} [Group Q]
(W : CrystallographicBraidWorld n Q)
(H : Subgroup (Equiv.Perm (Fin n)))
(hH : ∀ g : Equiv.Perm (Fin n), g ∈ H → IsTwoTorsion g) :
TorsionFree ↥(Subgroup.comap W.hol H) ∧
Subgroup.map W.hol (Subgroup.comap W.hol H) = H ∧
W.lattice ≤ Subgroup.comap W.hol H := by sorry
end CTB
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: in a crystallographic braid world, for every subgroup of the symmetric group all of whose elements are of two-power order, the preimage under the holonomy projection is torsion-free, the image of the preimage under the holonomy projection is the subgroup, and the translation lattice is contained in the preimage. Hypotheses: the world is given; every element of the subgroup is of two-power order; no further hypotheses appear.