ExtensionSectionFactor.lean`

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

The normalized factor system of an actual group extension

def OAI.PolycyclicRecognition.normalizedExtensionSection line 13
Source documentation
A normalized section exists for every surjective group extension.
```
def normalizedExtensionSection (S : GroupExtension N G Q) : S.Section where
…
```
theorem OAI.PolycyclicRecognition.normalizedExtensionSection_one line 21
def OAI.PolycyclicRecognition.GroupExtensionSection.factor line 29
Source documentation
This element measures the failure of the chosen section to multiply.
```
def factor (q r : Q) : N :=
…
```
theorem OAI.PolycyclicRecognition.GroupExtensionSection.inl_factor line 32
theorem OAI.PolycyclicRecognition.GroupExtensionSection.section_mul line 36
theorem OAI.PolycyclicRecognition.GroupExtensionSection.factor_one_left line 40
theorem OAI.PolycyclicRecognition.GroupExtensionSection.factor_one_right line 44
theorem OAI.PolycyclicRecognition.GroupExtensionSection.factor_cocycle line 49
Source documentation
The exact nonabelian two-cocycle identity.
```
theorem factor_cocycle (q r s : Q) :
    factor S σ q r * factor S σ (q * r) s =
      S.conjAct (σ q) (factor S σ r s) * factor S σ q (r * s) := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupExtensionSection.factor
theorem OAI.PolycyclicRecognition.GroupExtensionSection.section_action_mul line 58
Source documentation
Conjugation by the section multiplies up to the stated inner factor.
```
theorem section_action_mul (q r : Q) :
    S.conjAct (σ q) * S.conjAct (σ r) =
      MulAut.conj (factor S σ q r) * S.conjAct (σ (q * r)) := by
…
```
Mentions: OAI.PolycyclicRecognition.GroupExtensionSection.factor