OAI/GroupTheory/PolycyclicRecognition/Algebra/AbelianCyclicKernelRank.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Finite rational rank of an abelian kernel with cyclic quotient

This is deduced from actual FP-infinity and conjugation on subgroup homology. No rank, torsion-free, or character-tameness assumption is added.

  1. def OAI.PolycyclicRecognition.abelianKernelAbelianizationIso line 22
  2. theorem OAI.PolycyclicRecognition.abelianKernelQuotient_finite line 34
  3. theorem OAI.PolycyclicRecognition.rationalKernelExterior_intertwines line 41
  4. def OAI.PolycyclicRecognition.rationalCyclicKernelHomology line 50
  5. def OAI.PolycyclicRecognition.rationalCyclicKernelAction line 53
  6. def OAI.PolycyclicRecognition.rationalCyclicKernelExteriorMap line 57
  7. theorem OAI.PolycyclicRecognition.abelian_cyclic_kernel_finite_rational_rank line 62