OAI/GroupTheory/PolycyclicRecognition/Algebra/Extensions.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Cyclic factors and extensions of polycyclic groups

These are elementary consequences of concrete cyclic subnormal series. They are used in the nilpotent branch of the recognition argument.

  1. theorem OAI.PolycyclicRecognition.isPolycyclic_of_isCyclic line 19

    Source documentation

    A cyclic group has a one-step cyclic series.

    theorem isPolycyclic_of_isCyclic [IsCyclic G] : IsPolycyclic G := by
…

    Mentions: OAI.PolycyclicRecognition.IsPolycyclic

  2. theorem OAI.PolycyclicRecognition.isPolycyclic_of_normal_subgroup line 26

    Source documentation

    Polycyclic groups are closed under group extensions, by concatenating the series in the kernel with the lifted series in the quotient.

    theorem isPolycyclic_of_normal_subgroup (N : Subgroup G) [N.Normal]
    (hN : IsPolycyclic N) (hQ : IsPolycyclic (G ⧸ N)) : IsPolycyclic G := by
…

    Mentions: OAI.PolycyclicRecognition.IsPolycyclic