OAI/GroupTheory/PolycyclicRecognition/Finiteness/CentralQuotientVanishing.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

Reduced cocycle vanishing through the central quotient

The central moving summand is handled by central averaging. On the central fixed summand, cocycle values at central elements are globally fixed and therefore zero; the cocycle descends to the quotient by the center.

  1. theorem OAI.PolycyclicRecognition.unitaryReducedVanishing_of_centerQuotient line 22