OAI/GroupTheory/PolycyclicRecognition/Algebra/SmallCoefficientIdentityDimension.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

A vanishing unit cocycle splits the coefficient-ring syzygy

Multiplication in the coefficient ring extends an integral cochain to a coefficient-linear cochain. Applied to a primitive of the identity cocycle, this splits the next kernel and gives finite projective dimension.

  1. theorem OAI.PolycyclicRecognition.smallCoefficientIdentityClass_zero_projective line 20
  2. theorem OAI.PolycyclicRecognition.smallCoefficient_finite_dimension_of_identityClass_zero line 46