OAI/GroupTheory/PolycyclicRecognition/Finiteness/NormalCentralHomologyExact.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Exactness over the actual ambient quotient group ring

Ambient FP-infinity makes the kernel of the central transgression finitely generated over the quotient ring. This does not assert that its entire source or the central layer has finite scalar rank.

  1. def OAI.PolycyclicRecognition.normalCentralQuotientProjection line 21
  2. def OAI.PolycyclicRecognition.normalCentralProjectionModuleMap line 36
  3. def OAI.PolycyclicRecognition.normalCentralTransgressionModuleMap line 42
  4. theorem OAI.PolycyclicRecognition.normalCentralHomologyModule_exact line 48
  5. theorem OAI.PolycyclicRecognition.typeFPInfinity_centralTransgressionKernel_finite line 55