OAI/GroupTheory/PolycyclicRecognition/Algebra/CentralCocycleAverage.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Central averaging of a cocycle

The orthogonal complement of the central fixed subspace has no central invariants. Averaging over the center makes a cocycle uniformly small on compact sets in that summand, without requiring the whole group to commute.

  1. theorem OAI.PolycyclicRecognition.IsCocycle.finite_central_average line 24
  2. theorem OAI.PolycyclicRecognition.exists_small_correction_of_no_central_invariants line 42