NilpotentExtensionLangSplitting.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The sufficient hypothesis is the invertibility of A - 1 for one quotient lift. It is checked on the actual linear action, not assumed as a splitting.

def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionSplitting line 23
Source documentation
The completed extension splits if one lift has no fixed infinitesimal vector in the nilpotent kernel.
```
def completedExtensionSplitting [IsMulCommutative Q] (q : Q)
    (hA : Function.Bijective
      (fun x : C.carrier => C.automorphismLinear (S.conjAct (σ q)) x - x)) :
    (FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)).Splitting := by
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension.groupExtension
theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.completedExtensionSplitting_action_smooth line 43
Source documentation
Every action obtained from a splitting of this completed extension is smooth on its nilpotent kernel.
```
theorem completedExtensionSplitting_action_smooth
    (s : (FactorExtension.groupExtension (C.extensionFactorSystem S σ hσ)).Splitting)
    (q : Q) :
    ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, C.carrier)) ∞ (s.conjAct q) := by
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension.groupExtension