Every subgroup of the holonomy group is the holonomy group of a crystallographic subgroup (Corollary 10)
ProvedBQC.holonomy_restrictionFor every embedding of the finite group H into the holonomy group Ph of a crystallographic group, the set of the elements whose projection is the image of some element of H is a subgroup of the crystallographic group. This is the crystallographic subgroup of Corollary 10 of the source paper: every subgroup of the holonomy group occurs as the holonomy group of a crystallographic subgroup of the same dimension, the starting point of the Bieberbach group constructions of Theorem 20.
import Mathlib import Definitions.Def_BQC_alg import Definitions.Def_BQC_tor
namespace BQC
/-! Milestone 2 (Corollary 10): every subgroup of the holonomy group is the
holonomy group of a crystallographic subgroup. For every embedding of the
finite group H into the holonomy group Ph, the preimage of the image of H
under the projection is a subgroup of the crystallographic group; it is the
crystallographic subgroup of Corollary 10, the starting point of the
Bieberbach group constructions of Theorem 20. -/
theorem holonomy_restriction {d : Nat} {Cry Ph : Type*} [Group Cry] [Group Ph] [Fintype Ph]
(W : CryWorld d Cry Ph) {H : Type} [Group H] [Fintype H] (j : H →* Ph)
(hinj : ∀ x y : H, j x = j y → x = y) :
∃ T : Subgroup Cry, ∀ p : Cry, p ∈ T ↔ ∃ h : H, W.proj p = j h := by sorry
end BQC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: given a crystallographic world and an injective homomorphism from a finite group H into the holonomy group, there is a subgroup T of the crystallographic group whose members are exactly the elements whose projection equals the image of some element of H. Hypotheses: the homomorphism from H into the holonomy group is injective.
The statement asserts only ∃ T : Subgroup Cry, ∀ p, p ∈ T ↔ ∃ h : H, W.proj p = j h, which is the preimage of the range of j under W.proj and exists for every homomorphism; the accepted proof is a one line comap. Corollary 10 of the paper asserts that this preimage is a crystallographic group of dimension d with holonomy group H, that is, that it again carries a CryWorld structure with the restricted lattice, projection and holonomy. The row is true as written but does not state the result it is labelled with; please either restate it as the existence of a CryWorld d T H whose projection factors through j, or relabel it as the elementary preimage lemma it is.