OAI/GroupTheory/PolycyclicRecognition/Algebra/FactorSystemCocycleReduction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Removing the split part of a kernel cocycle

A splitting after projection of the kernel gives explicit corrections of the original quotient section. The corrected cocycle lies in the kernel of that projection. This retains the original extension through its gauge isomorphism.

  1. theorem OAI.PolycyclicRecognition.factorSystem_cocycle_reduction line 19
  2. theorem OAI.PolycyclicRecognition.factorSystem_cocycle_reduction_of_bijective_lang line 45