OAI/GroupTheory/PolycyclicRecognition/Finiteness/SmallCoefficientCompletedUnit.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

Complete vanishing detects the dimension of the coefficient ring

The unit cocycles are carried by the connecting maps in the tensor tower. If their completed class vanishes, an actual positive-degree identity class vanishes and the previous splitting theorem applies.

  1. def OAI.PolycyclicRecognition.smallCoefficientGroupIdentity line 18
  2. theorem OAI.PolycyclicRecognition.smallCoefficientGroupIdentity_comparison line 22
  3. theorem OAI.PolycyclicRecognition.smallCoefficientGroupIdentity_connecting line 30
  4. theorem OAI.PolycyclicRecognition.smallCoefficientGroupIdentity_forward line 50
  5. def OAI.PolycyclicRecognition.smallCoefficientCompletedUnit line 64
  6. theorem OAI.PolycyclicRecognition.smallCoefficient_finite_dimension_of_completedUnit_zero line 68
  7. theorem OAI.PolycyclicRecognition.smallCoefficient_finite_dimension_of_complete_vanishing line 80