OAI/GroupTheory/PolycyclicRecognition/Lattices/IntegralNilshadow.lean

GitHub source file

11 declarations, 0 contain sorry, 0 declared as axioms

Constructing the nilshadow of an integral abelian extension

Both the section and the removed action are constructed from the original extension. The twisted group has a nilpotent real completion of the correct dimension. Its removed action extends, and the original group embeds faithfully in the corresponding semidirect product. The quotient here is still integral.

  1. structure OAI.PolycyclicRecognition.IntegralNilshadowData line 22
  2. theorem OAI.PolycyclicRecognition.exists_integralNilshadowData line 40
  3. abbrev OAI.PolycyclicRecognition.IntegralNilshadowData.system line 65
  4. abbrev OAI.PolycyclicRecognition.IntegralNilshadowData.twistedSystem line 66
  5. abbrev OAI.PolycyclicRecognition.IntegralNilshadowData.integralAction line 67
  6. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.integralAction_kernel_smooth line 69
  7. def OAI.PolycyclicRecognition.IntegralNilshadowData.completedAction line 75
  8. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.completedAction_smooth line 78
  9. def OAI.PolycyclicRecognition.IntegralNilshadowData.completionSemidirectMap line 82
  10. def OAI.PolycyclicRecognition.IntegralNilshadowData.originalEmbedding line 92
  11. theorem OAI.PolycyclicRecognition.IntegralNilshadowData.originalEmbedding_injective line 98