ExponentialQuotientSection.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

The selected pure-word section in actual exponential coordinates

def OAI.PolycyclicRecognition.exponentialQuotientSection line 27
Source documentation
The prescribed linear quotient section, transported through the two actual global exponential charts.
```
def exponentialQuotientSection : C(Q, N) :=
…
```
theorem OAI.PolycyclicRecognition.exponentialQuotientSection_apply line 33
theorem OAI.PolycyclicRecognition.exponentialQuotientSection_rightInverse line 42
Source documentation
Naturality of the actual quotient exponential proves that this is a right inverse of the group quotient.
```
theorem exponentialQuotientSection_rightInverse (π : N →* Q)
    (hπ : ∀ v, π (chartN (eN v)) = chartQ (eQ (U.toSubmodule.mkQ v))) :
    ∀ q, π (exponentialQuotientSection U bQ lift eN eQ chartN chartQ q) = q := by
…
```
Mentions: OAI.PolycyclicRecognition.exponentialQuotientSection

theorem OAI.PolycyclicRecognition.exponentialQuotientSection_residual line 54

Source documentation

Factoring off the selected pure-word section gives exactly the kernel residual used by quotient integration.

theorem exponentialQuotientSection_residual (π : N →* Q)
    (hπ : ∀ v, π (chartN (eN v)) = chartQ (eQ (U.toSubmodule.mkQ v)))
    (hzeroQ : chartQ (eQ 0) = 1)
    (u : U) (q : V ⧸ U.toSubmodule) :
    ((quotientSectionResidual π
      (exponentialQuotientSection U bQ lift eN eQ chartN chartQ)
      (exponentialQuotientSection_rightInverse U bQ lift hlift eN eQ chartN chartQ π hπ)
      (chartN (eN (u : V)) * chartN (eN (quotientLinearSection U bQ lift q)))) : N) =
      chartN (eN (u : V)) := by
…

Mentions: OAI.PolycyclicRecognition.quotientSectionResidual, OAI.PolycyclicRecognition.exponentialQuotientSection, OAI.PolycyclicRecognition.exponentialQuotientSection_rightInverse, OAI.PolycyclicRecognition.quotientLinearSection