FactorQuotientAction.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

The quotient action descends through overlapping group factors

The factors need not form a direct or injective semidirect decomposition. The only overlap condition is that the nilpotent quotient kills it.

def OAI.PolycyclicRecognition.factorQuotientAction line 19

Source documentation

Translations and quotient automorphisms form the affine action of the actual semidirect product.

def factorQuotientAction (π : N →* Q) (s : Q → N)
    (hs : Function.RightInverse s π) (a : D →* MulAut N)
    (ha : ∀ d n, a d n ∈ π.ker ↔ n ∈ π.ker) : (N ⋊[a] D) →* Equiv.Perm Q where
…

theorem OAI.PolycyclicRecognition.factorQuotientAction_apply line 36

theorem OAI.PolycyclicRecognition.exists_descended_factor_quotient_action line 44

Source documentation

Killing the overlap makes the affine action well-defined on the ambient group, even when multiplication of the two factors is not injective.

theorem exists_descended_factor_quotient_action
    (ι : N →* G) (κ : D →* G) (hι : Function.Injective ι)
    (a : D →* MulAut N)
    (hconj : ∀ d n, ι (a d n) = κ d * ι n * (κ d)⁻¹)
    (hsurj : Function.Surjective (fun p : N × D => ι p.1 * κ p.2))
    (π : N →* Q) (s : Q → N) (hs : Function.RightInverse s π)
    (ha : ∀ d n, a d n ∈ π.ker ↔ n ∈ π.ker)
    (hoverlap : ∀ n d, ι n = κ d → π n = 1) :
    ∃ act : G →* Equiv.Perm Q,
      (∀ n d q, act (ι n * κ d) q = π n * descendQuotientAction π s hs a ha d q) ∧
      (∀ g, act g 1 = 1 ↔ ∃ n d, n ∈ π.ker ∧ ι n * κ d = g) ∧
      ∀ g h, act (g * h) 1 = act g (act h 1) := by
…

Mentions: OAI.PolycyclicRecognition.descendQuotientAction