OAI/GroupTheory/PolycyclicRecognition/Algebra/TorsionFreeCyclicExtension.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Virtual torsion freeness across a cyclic extension

The finite-index subgroup of the kernel is first made characteristic. For an infinite cyclic quotient, lift its generator and take the subgroup generated by that lift and the characteristic subgroup. Its torsion lies in the kernel, where torsion freeness is already known.

  1. theorem OAI.PolycyclicRecognition.HasNoNontrivialTorsion.of_injective line 21
  2. theorem OAI.PolycyclicRecognition.finiteIndex_of_kernel_cover line 31

    Source documentation

    A finite-index subgroup of the kernel gives finitely many cosets whenever the chosen subgroup surjects onto the quotient. No normality of H is needed.

    theorem finiteIndex_of_kernel_cover (N : Subgroup G) [N.Normal]
    (K : Subgroup N) [K.FiniteIndex] (H : Subgroup G)
    (hKH : K.map N.subtype ≤ H)
    (hcover : ∀ g : G, ∃ h ∈ H, (QuotientGroup.mk' N) h = (QuotientGroup.mk' N) g) :
    H.FiniteIndex := by
…
  3. theorem OAI.PolycyclicRecognition.torsionFree_finiteIndex_of_cyclic_extension line 55