CentralizerExtensionSplitting.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Splitting an extension using a bijective twisted-difference map

A central quotient element with bijective Lang map on the kernel selects a unique commuting lift in every quotient fiber. These lifts form a subgroup.

def OAI.PolycyclicRecognition.extensionLangMap line 19
Source documentation
The twisted difference on the kernel, with the order needed for correcting left coset representatives.
```
def extensionLangMap (n : N) : N := n⁻¹ * S.conjAct t n
```
theorem OAI.PolycyclicRecognition.extensionLangMap_one line 21
def OAI.PolycyclicRecognition.centralizerProjection line 24
theorem OAI.PolycyclicRecognition.centralizerProjection_surjective line 27
theorem OAI.PolycyclicRecognition.centralizerProjection_injective line 52
def OAI.PolycyclicRecognition.centralizerSplitting line 74
Source documentation
The centralizer provides an actual homomorphic section of the extension.
```
def centralizerSplitting
    (ht : ∀ q : Q, Commute (S.rightHom t) q)
    (hLang : Function.Bijective (extensionLangMap S t)) : S.Splitting := by
…
```
Mentions: OAI.PolycyclicRecognition.extensionLangMap