QuotientGroupAction.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Descending automorphisms through an actual surjective group map

def OAI.PolycyclicRecognition.descendQuotientAutomorphism line 16
Source documentation
A kernel-preserving automorphism descends using any section of the surjective quotient map. Its value on a projected point is independent of the choice of section.
```
def descendQuotientAutomorphism (π : N →* Q) (s : Q → N)
    (hs : Function.RightInverse s π) (e : N ≃* N)
    (he : ∀ n, e n ∈ π.ker ↔ n ∈ π.ker) : Q ≃* Q := by
…
```
theorem OAI.PolycyclicRecognition.descendQuotientAutomorphism_project line 39

def OAI.PolycyclicRecognition.descendQuotientAction line 48

Source documentation

A group of automorphisms preserving the kernel acts on the quotient.

def descendQuotientAction (π : N →* Q) (s : Q → N)
    (hs : Function.RightInverse s π) (a : D →* MulAut N)
    (ha : ∀ d n, a d n ∈ π.ker ↔ n ∈ π.ker) : D →* MulAut Q where
…

theorem OAI.PolycyclicRecognition.descendQuotientAction_project line 61

theorem OAI.PolycyclicRecognition.continuous_descendQuotientAutomorphism line 69

Source documentation

A continuous section makes each descended automorphism continuous as soon as the original automorphism and quotient map are continuous.

theorem continuous_descendQuotientAutomorphism
    [TopologicalSpace N] [TopologicalSpace Q]
    (π : N →* Q) (s : Q → N) (hs : Function.RightInverse s π) (e : N ≃* N)
    (he : ∀ n, e n ∈ π.ker ↔ n ∈ π.ker)
    (hπ : Continuous π) (hscont : Continuous s) (hecont : Continuous e) :
    Continuous (descendQuotientAutomorphism π s hs e he) :=
…

Mentions: OAI.PolycyclicRecognition.descendQuotientAutomorphism