Theorem5Dot1FaithfulAbelianExtension.lean

def functions : Subgroup (A → M) where
  carrier := {f | ∀ (x y : A) (d : D), f (x * d) * f y = f (y * d) * f x}
  one_mem' := by
    intro x y d
    rfl
  mul_mem' := by
    intro f g hf hg x y d
    change (f (x * d) * g (x * d)) * (f y * g y) =
      (f (y * d) * g (y * d)) * (f x * g x)
    calc
      _ = (f (x * d) * f y) * (g (x * d) * g y) := by ac_rfl
      _ = (f (y * d) * f x) * (g (y * d) * g x) := by rw [hf x y d, hg x y d]
      _ = _ := by ac_rfl
  inv_mem' := by
    intro f hf x y d
    change (f (x * d))⁻¹ * (f y)⁻¹ = (f (y * d))⁻¹ * (f x)⁻¹
    rw [← mul_inv, ← mul_inv, hf x y d]

def translate (a : A) : MulAut (functions D M) where
  toFun f := ⟨fun x => f.val (a⁻¹ * x), by
    intro x y d
    simpa only [mul_assoc] using f.property (a⁻¹ * x) (a⁻¹ * y) d⟩
  invFun f := ⟨fun x => f.val (a * x), by
    intro x y d
    simpa only [mul_assoc] using f.property (a * x) (a * y) d⟩
  left_inv f := by
    apply Subtype.ext
    funext x
    change f.val (a⁻¹ * (a * x)) = f.val x
    rw [inv_mul_cancel_left]
  right_inv f := by
    apply Subtype.ext
    funext x
    change f.val (a * (a⁻¹ * x)) = f.val x
    rw [mul_inv_cancel_left]
  map_mul' f g := rfl

def action : A →* MulAut (functions D M) where
  toFun := translate D M
  map_one' := by
    apply MulEquiv.ext
    intro f
    apply Subtype.ext
    funext x
    change f.val ((1 : A)⁻¹ * x) = f.val x
    rw [inv_one, one_mul]
  map_mul' a b := by
    apply MulEquiv.ext
    intro f
    apply Subtype.ext
    funext x
    change f.val ((a * b)⁻¹ * x) = f.val (b⁻¹ * (a⁻¹ * x))
    rw [mul_inv_rev, mul_assoc]

def difference : functions D M →* (D → M) where
  toFun f d := f.val d / f.val 1
  map_one' := by
    funext d
    exact one_div_one
  map_mul' f g := by
    funext d
    change (f.val d * g.val d) / (f.val 1 * g.val 1) = (f.val d / f.val 1) * (g.val d / g.val 1)
    rw [div_mul_div_comm]

theorem difference_action (a : A) (f : functions D M) :
    difference D M (action D M a f) = difference D M f

theorem constant_of_difference_eq_one (f : functions D M)
    (hf : difference D M f = 1) (x : A) (d : D) :
    f.val (x * d) = f.val x

theorem action_eq_self_of_difference_eq_one [D.Normal]
    (a : D) (f : functions D M) (hf : difference D M f = 1) :
    action D M (a : A) f = f

def coordinate [D.Normal] (x : A) : D

theorem coordinate_mul [D.Normal] (x : A) (d : D) :
    coordinate D (x * d) = coordinate D x * d

theorem action_injective [D.Normal] [Nontrivial M]
    (ι : D →* M) (hι : Function.Injective ι) :
    Function.Injective (action D M)

def extensionDifference : (functions D M) ⋊[action D M] A →* (D → M) where
  toFun b := difference D M b.left
  map_one' := map_one (difference D M)
  map_mul' b c := by
    change difference D M (b.left * action D M b.right c.left) = _
    rw [map_mul, difference_action]

theorem difference_eq_one_of_mem_derived
    {b : (functions D M) ⋊[action D M] A}
    (hb : b ∈ derivedSeries ((functions D M) ⋊[action D M] A) 1) :
    difference D M b.left = 1

theorem faithful_abelian_extension_solvable_length
    (A : Type u) [Group A] [Finite A] (m : ℕ) (hm : 2 ≤ m)
    (hA : derivedSeries A m = ⊥) :
    ∃ (C : Type u) (_ : CommGroup C) (_ : Finite C) (φ : A →* MulAut C),
      Function.Injective φ ∧ derivedSeries (C ⋊[φ] A) m = ⊥