OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianNormalHigherExteriorFiniteness.lean

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

FP-infinity controls every rational exterior power of an abelian kernel

The quotient acts by actual conjugation. The surjective map from homology transfers finite generation to the higher exterior powers.

  1. def OAI.PolycyclicRecognition.higherExteriorRepresentation line 18
  2. def OAI.PolycyclicRecognition.scalarNormalHomology line 28
  3. def OAI.PolycyclicRecognition.scalarAbelianNormalExterior line 31
  4. def OAI.PolycyclicRecognition.scalarAbelianNormalExteriorMap line 35
  5. theorem OAI.PolycyclicRecognition.typeFPInfinity_abelianNormalHigherExterior_finite_of_factorial_ne_zero line 42
  6. theorem OAI.PolycyclicRecognition.typeFPInfinity_abelianNormalHigherExterior_finite line 67