ConjugationLift.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Recovering a group action from faithful conjugation

Pointwise automorphisms compatible with ambient conjugation automatically form an action. This removes a separate action-law assumption when the Cartan automorphisms have already been identified in a faithful representation.

def OAI.PolycyclicRecognition.conjugationLift line 20

Source documentation

Faithful ambient conjugation forces the action laws.

def conjugationLift (ι : N →* G) (κ : D →* G) (hι : Function.Injective ι)
    (a : D → MulAut N)
    (ha : ∀ d n, ι (a d n) = κ d * ι n * (κ d)⁻¹) : D →* MulAut N where
…

theorem OAI.PolycyclicRecognition.conjugationLift_apply line 36
def OAI.PolycyclicRecognition.conjugationLiftOfNormal line 43
Source documentation
A normal image supplies the pointwise automorphisms by transport from the actual subgroup. In particular, no action is part of this premise.
```
def conjugationLiftOfNormal (ι : N →* G) (κ : D →* G) (hι : Function.Injective ι)
    (hnormal : ι.range.Normal) : D →* MulAut N := by
…
```
theorem OAI.PolycyclicRecognition.conjugationLiftOfNormal_spec line 53