OAI/GroupTheory/PolycyclicRecognition/Algebra/EquivariantCommutatorFiltration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Linear control of iterated commutators in a normal subgroup

An equivariant homomorphism from a normal subgroup into an additive vector space sends action commutators to action differences. Vanishing of the linear action filtration therefore puts the relative commutator series in the kernel of that homomorphism.

  1. def OAI.PolycyclicRecognition.linearPreimageSubgroup line 20
  2. theorem OAI.PolycyclicRecognition.relativeCommutatorSeries_le_linearFiltration line 33
  3. theorem OAI.PolycyclicRecognition.relativeCommutatorSeries_le_kernel_of_linearFiltration line 62