OAI/GroupTheory/PolycyclicRecognition/Analysis/ControlledChainRepresentation.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Equivariant control of finite chains

Left translation preserves every relative-position bound. Consequently an equivariant image of a finitely generated representation lies at one finite scale in the homogeneous standard chains.

  1. theorem OAI.PolycyclicRecognition.IsControlledTuple.left_translate line 20
  2. def OAI.PolycyclicRecognition.controlledChainSubrepresentation line 25
  3. theorem OAI.PolycyclicRecognition.exists_common_controlledChainScale line 35
  4. theorem OAI.PolycyclicRecognition.finiteRepresentation_range_controlled line 49