OAI/GroupTheory/PolycyclicRecognition/Geometry/CartanCocycleRestriction.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Reduced cocycles restricted to the actual Cartan factor

Contracted root generation identifies its fixed vectors with those of the ambient representation. Its nilpotent Lie model is algebraically nilpotent, so the proved reduced-cohomology theorem applies on every compact subset.

  1. theorem OAI.PolycyclicRecognition.cartan_unitary_no_fixed line 34
  2. theorem OAI.PolycyclicRecognition.cartan_cocycle_approximation line 51