The holonomy projection is injective on finite subgroups (Lemma 9)
ProvedBQC.finite_subgroup_injIf the finite group K embeds into the crystallographic group Cry, then two elements of K whose images have the same projection to the holonomy group are equal. The kernel of the projection is the integer lattice, which is torsion free, while the difference of the two embedded elements would have finite order inside the lattice. This is Lemma 9 of the source paper: the restriction of the projection to any finite subgroup is an isomorphism onto its image, so every finite subgroup of a crystallographic group embeds isomorphically into its holonomy group.
import Mathlib import Definitions.Def_BQC_alg import Definitions.Def_BQC_tor
namespace BQC
/-! Milestone 1 (Lemma 9): the projection of a crystallographic group to its
holonomy group is injective on finite subgroups. If the finite group K embeds
into the crystallographic group Cry, then two elements of K with the same
projection are equal. The proof observes that the kernel of the projection is
the integer lattice, which is torsion free, while a nonzero element of the
difference would have finite order inside the lattice. -/
theorem finite_subgroup_inj {d : Nat} {Cry Ph : Type*} [Group Cry] [Group Ph] [Fintype Ph]
(W : CryWorld d Cry Ph) {K : Type} [Group K] [Fintype K] (f : K →* Cry)
(finj : ∀ x y : K, f x = f y → x = y) (x y : K)
(hxy : W.proj (f x) = W.proj (f y)) : x = y := by sorry
end BQC
Read-back
What the Lean code literally says, in plain math · glm-5-latest-short
Restate: given a crystallographic world, a finite group K, a homomorphism from K into the crystallographic group that is injective, and two elements of K whose images under the homomorphism have the same projection to the holonomy group, the two elements of K are equal. Hypotheses: the homomorphism from K is injective; the projections of the two images coincide.