GroupExtensionFactorSystem.lean`

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A group extension is its actual section factor system

def OAI.PolycyclicRecognition.GroupExtensionSection.factorSystem line 15
def OAI.PolycyclicRecognition.GroupExtensionSection.coordinate line 25
Source documentation
The kernel coordinate of an element relative to the chosen section.
```
def coordinate (g : G) : N :=
…
```
theorem OAI.PolycyclicRecognition.GroupExtensionSection.inl_coordinate line 28
theorem OAI.PolycyclicRecognition.GroupExtensionSection.coordinate_inl_mul line 34
def OAI.PolycyclicRecognition.GroupExtensionSection.normalFormEquiv line 41
Source documentation
The underlying normal-form coordinates are bijective.
```
def normalFormEquiv : G ≃ FactorExtension (factorSystem S σ hσ) where
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension, OAI.PolycyclicRecognition.GroupExtensionSection.factorSystem
def OAI.PolycyclicRecognition.GroupExtensionSection.decode line 53
Source documentation
Decoding the normal form respects the nonabelian multiplication.
```
def decode : FactorExtension (factorSystem S σ hσ) →* G where
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension, OAI.PolycyclicRecognition.GroupExtensionSection.factorSystem
def OAI.PolycyclicRecognition.GroupExtensionSection.mulEquiv line 63
Source documentation
No splitting is assumed: the section factor supplies the full group law.
```
def mulEquiv : G ≃* FactorExtension (factorSystem S σ hσ) :=
…
```
Mentions: OAI.PolycyclicRecognition.FactorExtension, OAI.PolycyclicRecognition.GroupExtensionSection.factorSystem