OAI/GroupTheory/PolycyclicRecognition/Algebra/NilpotentLangMap.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The Lang map for a nilpotent Lie automorphism without fixed vectors

The nonlinear error raises the lower central series. After applying the inverse of A - 1, the finite correction algorithm gives a global inverse.

  1. theorem OAI.PolycyclicRecognition.polynomial_lang_bijective line 23

    Source documentation

    Fixed-point-freeness of the linear automorphism suffices for bijectivity of its nonlinear twisted difference on the simply connected nilpotent group.

    theorem polynomial_lang_bijective (A : L ≃ₗ⁅ℝ⁆ L)
    (hA : Function.Bijective (fun x : L => A x - x)) :
    Function.Bijective (fun x : L => x⁻¹ * A x) := by
…