OAI/GroupTheory/PolycyclicRecognition/Algebra/InvariantLinearLayer.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Endomorphisms on an invariant subquotient

This is the concrete linear bridge used on successive lower-central factors. Commutation modulo the smaller subspace becomes exact commutation, and unipotence survives restriction and quotient.

  1. abbrev OAI.PolycyclicRecognition.InvariantLinearLayer line 18
  2. def OAI.PolycyclicRecognition.invariantLayerEnd line 20
  3. theorem OAI.PolycyclicRecognition.invariantLayerEnd_commute line 25
  4. theorem OAI.PolycyclicRecognition.invariantLayerEnd_unipotent line 39