OAI/GroupTheory/PolycyclicRecognition/Algebra/RationalNilpotentQuotient.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

A faithful rational action on the quotient by the nilpotent radical

The finitely many upper central layers give a direct-product vector space. For a maximal nilpotent normal subgroup, the action kernel is exactly that subgroup, by the proved central-filtration criterion.

  1. abbrev OAI.PolycyclicRecognition.CentralLayersSpace line 19
  2. def OAI.PolycyclicRecognition.centralLayersAction line 22
  3. theorem OAI.PolycyclicRecognition.centralLayersAction_ker_iff line 37
  4. theorem OAI.PolycyclicRecognition.subgroup_le_centralLayersAction_ker line 60
  5. theorem OAI.PolycyclicRecognition.centralLayersAction_ker line 65
  6. theorem OAI.PolycyclicRecognition.centralLayersSpace_finite line 86
  7. def OAI.PolycyclicRecognition.nilpotentQuotientRationalAction line 95
  8. theorem OAI.PolycyclicRecognition.nilpotentQuotientRationalAction_injective line 103