OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeLinearAction.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

A faithful linear action of the discrete lattice automorphisms

The constructed action is the differential of the actual smooth extension. It is not a separately assumed representation of the discrete group.

  1. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLinear line 16
  2. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLinear_apply line 31
  3. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLinear_injective line 35
  4. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismMatrix line 44
  5. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismMatrix_injective line 49