FactorAutomorphismDescent.lean`

12 declarations, 0 contain sorry, 0 declared as axioms

Descending automorphisms through overlapping group factors

theorem OAI.PolycyclicRecognition.commutes_of_surjective_coordinates line 11

Source documentation

A commutation identity can be checked on surjective coordinate maps.

theorem commutes_of_surjective_coordinates {X Y N D : Type*}
    (eN : X → N) (eD : Y → D) (hn : Function.Surjective eN) (hd : Function.Surjective eD)
    (A : N → N) (B : D → N → N) (a : X → X) (b : Y → X → X)
    (hA : ∀ x, A (eN x) = eN (a x))
    (hB : ∀ y x, B (eD y) (eN x) = eN (b y x))
    (hab : ∀ y x, a (b y x) = b y (a x)) : ∀ d n, A (B d n) = B d (A n) := by
…

theorem OAI.PolycyclicRecognition.character_invariant_of_factor_coordinates line 23

Source documentation

Invariance of a character can be checked in surjective factor coordinates.

theorem character_invariant_of_factor_coordinates {X N D G Q K : Type*}
    [Monoid N] [Monoid D] [Monoid G] [Monoid Q]
    (ι : N →* G) (κ : D →* G) (q : G →* Q) (e : X → N)
    (he : Function.Surjective e)
    (hp : Function.Surjective (fun p : N × D => ι p.1 * κ p.2))
    (rot : K → X → X) (act : K → G → G)
    (hq : ∀ x, q (ι (e x)) = 1)
    (ha : ∀ k x d, act k (ι (e x) * κ d) = ι (e (rot k x)) * κ d) :
    ∀ k g, q (act k g) = q g := by
…

def OAI.PolycyclicRecognition.rotatedFactorHom line 46
theorem OAI.PolycyclicRecognition.factorHom_surjective line 53
theorem OAI.PolycyclicRecognition.rotatedFactorHom_kernel line 60
def OAI.PolycyclicRecognition.descendedFactorHom line 71
Source documentation
The induced endomorphism on the original group.
```
def descendedFactorHom (k : K) : G →* G :=
…
```
theorem OAI.PolycyclicRecognition.descendedFactorHom_product line 77
theorem OAI.PolycyclicRecognition.descendedFactorHom_one line 82
theorem OAI.PolycyclicRecognition.descendedFactorHom_mul line 87
def OAI.PolycyclicRecognition.descendedFactorAction line 96
Source documentation
An action on the first factor commuting with the second factor and fixing their actual intersection descends to an action on the whole group.
```
def descendedFactorAction : K →* MulAut G where
…
```
theorem OAI.PolycyclicRecognition.descendedFactorAction_product line 112

theorem OAI.PolycyclicRecognition.continuous_descendedFactorAction line 122

Source documentation

Joint continuity descends through the open factor product.

theorem continuous_descendedFactorAction
    (hι : Continuous ι) (hκ : Continuous κ)
    (hα : Continuous (fun p : K × N => α p.1 p.2))
    (hopen : IsOpenMap (fun p : N × D => ι p.1 * κ p.2)) :
    Continuous (fun p : K × G => descendedFactorAction ι κ φ hconj hsurj α hcomm hfix p.1 p.2) := by
…

Mentions: OAI.PolycyclicRecognition.descendedFactorAction