NilpotentExtensionEmbedding.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Extending a nilpotent lattice to the full nonsplit extension

Only the nilpotent kernel is completed here. The original quotient, section, and all of its defects are retained exactly.

def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionFactorMap line 19
Source documentation
The original and completed factor systems agree on the kernel lattice.
```
def extensionFactorMap :
    FactorExtension (GroupExtensionSection.factorSystem S σ hσ) →*
      FactorExtension (C.extensionFactorSystem S σ hσ) :=
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension, OAI.PolycyclicRecognition.GroupExtensionSection.factorSystem
theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionFactorMap_injective line 26
def OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionEmbedding line 31
Source documentation
A faithful map of the original nonsplit extension into the group with completed nilpotent kernel and unchanged quotient.
```
def extensionEmbedding : G →* FactorExtension (C.extensionFactorSystem S σ hσ) :=
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension
theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.extensionEmbedding_injective line 34
theorem OAI.PolycyclicRecognition.NilpotentLatticeCoordinates.mem_extensionEmbedding_range line 39
Source documentation
This range description retains the full quotient and only restricts the nilpotent coordinate to its constructed lattice.
```
theorem mem_extensionEmbedding_range (a : FactorExtension (C.extensionFactorSystem S σ hσ)) :
    a ∈ (C.extensionEmbedding S σ hσ).range ↔ a.left ∈ C.lattice := by
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension