OAI/GroupTheory/PolycyclicRecognition/Lattices/KernelCompletionAction.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

Extending an action to the nilpotent completion

Existence comes from the constructed homomorphism extension. Uniqueness on the integer grid forces the extensions to satisfy the action law.

  1. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.action_extension_exists line 23
  2. def OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAutomorphism line 32
  3. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAutomorphism_smooth line 35
  4. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAutomorphism_embed line 40
  5. def OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAction line 44
  6. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAction_embed line 68
  7. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAction_smooth line 72
  8. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.extendedAction_preserves_hom line 76