OAI/GroupTheory/PolycyclicRecognition/Lattices/KernelCompletionHeight.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

The real quotient of a nilpotent kernel completion

The quotient homomorphism extends to the constructed completion. Its kernel is exactly the original real kernel, by the dimension retained in the cyclic construction. No exactness property is postulated for the completion.

  1. def OAI.PolycyclicRecognition.integralRealHeight line 21
  2. theorem OAI.PolycyclicRecognition.integralRealHeight_injective line 26
  3. theorem OAI.PolycyclicRecognition.integralRealHeight_range line 30
  4. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.exists_height line 44
  5. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.height_surjective line 61
  6. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.height_kernel_eq line 80
  7. theorem OAI.PolycyclicRecognition.NilpotentKernelCompletion.embed_range_eq_height_lattice line 130