OAI/GroupTheory/PolycyclicRecognition/Lattices/NilpotentLatticeAutomorphisms.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Extending the lattice automorphism group to its nilpotent Lie model

The extension respects composition. This retains arbitrary discrete actions, without imposing unipotence on their automorphisms.

  1. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.ext_polynomial line 21
  2. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism line 36
  3. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_polynomial line 40
  4. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_smooth line 46
  5. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_on_lattice line 52
  6. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_one line 58
  7. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_mul line 66
  8. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismHom line 81
  9. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphism_injective line 86
  10. def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLieEquiv line 96
  11. theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.automorphismLieEquiv_apply line 99