NilpotentExtensionFactorSystem.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The actual real factor system of a nilpotent-kernel extension

Its failure to be an action is exactly the exponential of the inner Lie derivation obtained from the section defect.

def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionFactorSystem line 20
theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionFactorSystem_smooth line 37
Source documentation
Smoothness is proved from the lattice polynomial extension.
```
theorem extensionFactorSystem_smooth (q : Q) :
    ContMDiff (𝓘(ℝ, C.carrier)) (𝓘(ℝ, C.carrier)) ∞
      ((C.extensionFactorSystem S σ hσ).action q) :=
…
```

theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extension_linear_defect line 43

Source documentation

The exact defect formula on continuous linear operators.

theorem extension_linear_defect (q r : Q) :
    LinearMap.toContinuousLinearMap (C.automorphismLinear (S.conjAct (σ q))) *
        LinearMap.toContinuousLinearMap (C.automorphismLinear (S.conjAct (σ r))) =
      NormedSpace.exp (LinearMap.toContinuousLinearMap
          (LieAlgebra.ad ℝ C.carrier (C.equiv (factor S σ q r)))) *
        LinearMap.toContinuousLinearMap (C.automorphismLinear (S.conjAct (σ (q * r)))) := by
…