NilpotentExtensionFixedFreeRealization.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Connected realization of nonsplit extensions with a fixed-point-free lift

The quotient lift is allowed to have nontrivial commutators. The Lang inverse constructs a splitting only after the nilpotent kernel has been completed.

theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extension_realization_of_fixedPointFree_lift line 25
Source documentation
A concrete sufficient condition for the general nonsplit realization: one quotient lift acts without fixed vectors on the completed kernel.
```
theorem extension_realization_of_fixedPointFree_lift (q : IntegralLatticeGroup n)
    (hA : Function.Bijective
      (fun x : C.carrier => C.automorphismLinear (S.conjAct (σ q)) x - x)) :
    ∃ K : Subgroup G, K.FiniteIndex ∧ ∃ (R : SimplyConnectedSolvableLieModel)
      (Λ : Subgroup R.carrier), IsUniformLattice Λ ∧ Nonempty (K ≃* Λ) := by
…
```
Mentions: OAI.PolycyclicRecognition.IntegralLatticeGroup, OAI.PolycyclicRecognition.SimplyConnectedSolvableLieModel