QuotientSectionCoordinates.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Coordinates separating a quotient and its kernel

A continuous section of the actual quotient map gives global coordinates. The formulas retain the conjugation and section cocycle needed for product Haar measure and the ideal-coordinate estimates.

def OAI.PolycyclicRecognition.quotientSectionResidual line 23
Source documentation
The kernel component left after removing the chosen section.
```
def quotientSectionResidual (n : N) : π.ker :=
…
```
def OAI.PolycyclicRecognition.quotientSectionHomeomorph line 29
Source documentation
Quotient coordinate first, followed by the actual kernel coordinate.
```
def quotientSectionHomeomorph : N ≃ₜ Q × π.ker := by
…
```
def OAI.PolycyclicRecognition.quotientSectionCocycle line 57
Source documentation
The section cocycle of left translation, valued in the actual kernel.
```
def quotientSectionCocycle (n : N) (q : Q) : π.ker :=
…
```
def OAI.PolycyclicRecognition.quotientKernelConjugate line 61
Source documentation
Conjugation on the kernel, expressed without selecting logarithms.
```
def quotientKernelConjugate (n : N) (i : π.ker) : π.ker :=
…
```
theorem OAI.PolycyclicRecognition.quotientSection_left_translation line 67
theorem OAI.PolycyclicRecognition.continuous_quotientSectionCocycle line 80