OAI/GroupTheory/PolycyclicRecognition/Algebra/CoordinateOrbitRepresentation.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Linearizing a group through its translated coordinate functions

Right translates of separating coordinates span a faithful representation. A uniform finite-dimensional space containing those translates makes the representation finite dimensional; polynomial multiplication will supply it.

  1. def OAI.PolycyclicRecognition.rightTranslateLinear line 19
  2. def OAI.PolycyclicRecognition.coordinateOrbitSpan line 24
  3. theorem OAI.PolycyclicRecognition.coordinate_mem_orbitSpan line 27
  4. theorem OAI.PolycyclicRecognition.rightTranslate_mem_coordinateOrbitSpan line 33
  5. def OAI.PolycyclicRecognition.coordinateOrbitRepresentation line 47
  6. theorem OAI.PolycyclicRecognition.coordinateOrbitRepresentation_apply line 65
  7. theorem OAI.PolycyclicRecognition.coordinateOrbitRepresentation_injective line 69
  8. theorem OAI.PolycyclicRecognition.finiteDimensional_coordinateOrbitSpan line 80