OAI/GroupTheory/PolycyclicRecognition/Algebra/FieldCyclicKernelRank.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Finite rank of cyclic kernels after extension to a field

This includes prime-field reductions as well as rationalization. The exterior cross product is injective in every characteristic.

  1. def OAI.PolycyclicRecognition.fieldCyclicKernelAction line 20
  2. def OAI.PolycyclicRecognition.fieldCyclicKernelHomology line 24
  3. theorem OAI.PolycyclicRecognition.fieldKernelExterior_intertwines line 28
  4. def OAI.PolycyclicRecognition.fieldCyclicKernelExteriorMap line 37
  5. theorem OAI.PolycyclicRecognition.abelian_cyclic_kernel_field_finite_rank line 43