OAI/GroupTheory/PolycyclicRecognition/Finiteness/AbelianReducedCohomology.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reduced first cohomology for abelian unitary actions

For commuting group elements, a convex average of translated cocycle values is exactly a coboundary correction. The simultaneous unitary averaging lemma makes this correction uniformly small on each compact set.

  1. theorem OAI.PolycyclicRecognition.IsCocycle.finite_average_commutative line 24
  2. theorem OAI.PolycyclicRecognition.reducedCohomologyInput_of_commutative line 41