MagnusKernel.lean

instance : Fintype X

instance : DecidableEq X

theorem mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
    (N : Subgroup (FreeGroup X)) [N.Normal] {n : ℕ} (hn : 0 < n)
    {w : FreeGroup X} (hwN : w ∈ N)
    (hres :
      FoxDifferential.residueUniversalDifferential n (QuotientGroup.mk' N) w = 0) :
    w ∈ FoxDifferential.foxCommutatorPowerSubgroup
      (F := FreeGroup X) N n

theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_of_surjective
    {C : ProCGroups.FiniteGroupClass}
    (hC : ProCGroups.FiniteGroupClass.Hereditary C)
    (hForm : ProCGroups.FiniteGroupClass.Formation C)
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
    (hCH : C H)
    {Q : Type} [Group Q]
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (hCker : C β.ker)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hzero :
      FoxDifferential.zcUniversalDifferential C (β.comp α) w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  exact
    FoxDifferential.mem_commutator_ker_of_zcUnivDiff_eq_zero_of_finite_magnus_surj
      (C := C) (hC := hC) (X := X) (hForm := hForm) (hCH := hCH)
      (α := α) (hα := hα) (β := β) (hβ := hβ) (hCker := hCker)
      (fun j _ w hw hres =>
        mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
          (X := X) (β.comp α).ker j.positive hw hres)
      hwker hzero

theorem mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero
    {Q H : Type} [Group Q] [Group H]
    (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
    (hpow : ∀ k : β.ker, k ^ n = 1)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      FoxDifferential.foxAlgebraicStageDerivativeVector
        (X := X) (β.comp α).ker n w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  have hres :
      FoxDifferential.residueUniversalDifferential n
          (QuotientGroup.mk' (β.comp α).ker) w = 0 :=
    (foxAlgebraicStageDerivativeVector_eq_zero_iff_residueUniversalDifferential_eq_zero
      (X := X) (N := (β.comp α).ker) (n := n) (w := w)).1 hder
  exact
    FoxDifferential.mem_commutator_ker_of_residueUniversalDifferential_eq_zero_of_kernel_le
      (X := X) α β n hpow
      (fun w hw hres =>
        mem_foxCommutatorPowerSubgroup_of_residueUniversalDifferential_eq_zero
          (X := X) (β.comp α).ker hn hw hres)
      hwker hres

theorem mem_commutator_ker_of_finiteFoxStageDerivativeVector_eq_zero_finite
    {X : Type u} [Finite X] [DecidableEq X]
    {Q H : Type u} [Group Q] [Group H] [Finite Q] [Finite H]
    (α : FreeGroup X →* Q) (β : Q →* H) (n : ℕ) (hn : 0 < n)
    (hpow : ∀ k : β.ker, k ^ n = 1)
    {w : FreeGroup X}
    (hwker : w ∈ (β.comp α).ker)
    (hder :
      FoxDifferential.foxAlgebraicStageDerivativeVector
        (X := X) (β.comp α).ker n w = 0) :
    (⟨α w, by
      change β (α w) = 1
      simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) ∈
      commutator β.ker := by
  classical
  rcases Finite.exists_equiv_fin X with ⟨m, ⟨eX⟩⟩
  let : DecidableEq (Fin m) := Classical.decEq (Fin m)
  rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} Q with
    ⟨Q0, instQ0Group, _instQ0Fintype, ⟨eQ⟩⟩
  rcases Finite.exists_type_univ_nonempty_mulEquiv.{u, 0} H with
    ⟨H0, instH0Group, _instH0Fintype, ⟨eH⟩⟩
  let : Group Q0 := instQ0Group
  let : Group H0 := instH0Group
  let phi : FreeGroup X ≃* FreeGroup (Fin m) := FreeGroup.freeGroupCongr eX
  let α0 : FreeGroup (Fin m) →* Q0 :=
    eQ.toMonoidHom.comp (α.comp phi.symm.toMonoidHom)
  let β0 : Q0 →* H0 :=
    eH.toMonoidHom.comp (β.comp eQ.symm.toMonoidHom)
  let w0 : FreeGroup (Fin m) := phi w
  let M0 : Subgroup (FreeGroup (Fin m)) :=
    (β0.comp α0).ker
  have : M0.Normal := by
    dsimp [M0]
    infer_instance
  have hM0 : (β.comp α).ker.map phi.toMonoidHom = M0 := by
    ext z
    constructor
    · rintro ⟨x, hx, rfl⟩
      change β0 (α0 (phi x)) = 1
      change β (α x) = 1 at hx
      have hphi : phi.symm (phi x) = x := phi.symm_apply_apply x
      simpa [β0, α0, M0, hphi] using congrArg eH hx
    · intro hz
      refine ⟨phi.symm z, ?_, ?_⟩
      · change β (α (phi.symm z)) = 1
        have hz' : eH (β (α (phi.symm z))) = 1 := by
          simpa [β0, α0, M0] using hz
        exact eH.injective (by simpa using hz')
      · exact phi.apply_symm_apply z
  have hwker0 : w0 ∈ (β0.comp α0).ker := by
    change β0 (α0 w0) = 1
    change β (α w) = 1 at hwker
    have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
    simpa [β0, α0, w0, hphi] using congrArg eH hwker
  have hderM0 :
      FoxDifferential.foxAlgebraicStageDerivativeVector
        (X := Fin m) M0 n w0 = 0 := by
    simpa [M0, w0, phi] using
      FoxDifferential.foxAlgebraicStageDerivativeVector_eq_zero_reindex
        (X := X) (Y := Fin m) eX (β.comp α).ker M0 hM0 n hder
  have hder0 :
      FoxDifferential.foxAlgebraicStageDerivativeVector
        (X := Fin m) (β0.comp α0).ker n w0 = 0 := by
    simpa [M0] using hderM0
  have hpow0 : ∀ k : β0.ker, k ^ n = 1 := by
    intro k
    have hkβ : β (eQ.symm k.1) = 1 := by
      have hk0 : β0 k.1 = 1 := by
        exact k.2
      have hk : eH (β (eQ.symm k.1)) = 1 := by
        simpa [β0] using hk0
      exact eH.injective (by simpa using hk)
    have hkpow := hpow ⟨eQ.symm k.1, hkβ⟩
    have hkpow' : (eQ.symm k.1) ^ n = 1 :=
      congrArg Subtype.val hkpow
    have := congrArg eQ hkpow'
    apply Subtype.ext
    simpa using this
  let q0 : β0.ker :=
    ⟨α0 w0, by
      change β0 (α0 w0) = 1
      simpa [MonoidHom.mem_ker] using hwker0⟩
  have hcomm0 : q0 ∈ commutator β0.ker := by
    simpa [q0] using
      mem_commutator_ker_of_foxAlgebraicStageDerivativeVector_eq_zero
        (X := Fin m) α0 β0 n hn hpow0 hwker0 hder0
  let κ : β0.ker →* β.ker :=
    { toFun := fun k =>
        ⟨eQ.symm k.1, by
          change β (eQ.symm k.1) = 1
          have hk0 : β0 k.1 = 1 := by
            exact k.2
          have hk : eH (β (eQ.symm k.1)) = 1 := by
            simpa [β0] using hk0
          exact eH.injective (by simpa using hk)⟩
      map_one' := by
        apply Subtype.ext
        simp only [OneMemClass.coe_one, map_one]
      map_mul' := by
        intro a b
        apply Subtype.ext
        simp only [Subgroup.coe_mul, map_mul, MulMemClass.mk_mul_mk]}
  have hcomm_map : (commutator β0.ker).map κ ≤ commutator β.ker := by
    rw [_root_.map_commutator_eq]
    exact Subgroup.commutator_mono (by intro x hx; trivial) (by intro x hx; trivial)
  have hκq0 :
      κ q0 =
        (⟨α w, by
          change β (α w) = 1
          simpa [MonoidHom.mem_ker, MonoidHom.comp_apply] using hwker⟩ : β.ker) := by
    apply Subtype.ext
    have hphi : phi.symm (phi w) = w := phi.symm_apply_apply w
    simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_ofClass,
      Function.comp_apply, hphi, MonoidHom.coe_mk, OneHom.coe_mk,
      MulEquiv.symm_apply_apply, κ, q0, α0, w0]
  have hκcomm : κ q0 ∈ commutator β.ker :=
    hcomm_map ⟨q0, hcomm0, rfl⟩
  simpa [hκq0] using hκcomm

theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj_factor
    {Q : Type} [Group Q]
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
    (hn :
      FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
        (H := H) X (β.comp α) w = 0) :
    q ∈ commutator β.ker

theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    [DiscreteTopology (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    [Finite (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    (n : (QuotientGroup.mk' N).ker)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
        (QuotientGroup.mk' N) n.1 = 0) :
    n ∈ commutator (QuotientGroup.mk' N).ker

theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_allFinite_of_surjective
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (n : ψ.ker)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
        ψ n.1 = 0) :
    n ∈ commutator ψ.ker

theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_allFinite_of_surj_factor
    {Q : Type} [Group Q]
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
    (hn :
      FoxDifferential.zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
        (β.comp α) w = 0) :
    q ∈ commutator β.ker

theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_allFinite_of_surj_factor
    {Q : Type} [Group Q]
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H] [Finite H]
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.allFinite : ProCGroups.FiniteGroupClass)
        (β.comp α) w = 0) :
    q ∈ commutator β.ker

theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup
    (p : ℕ) [Fact (Nat.Prime p)]
    (N : Subgroup (FreeGroup X)) [N.Normal]
    [TopologicalSpace (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    [DiscreteTopology (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    [IsTopologicalGroup (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N)]
    (hCtarget :
      ProCGroups.FiniteGroupClass.pGroup p
        (FoxDifferential.foxAlgebraicStageTargetQuotient (X := X) N))
    (n : (QuotientGroup.mk' N).ker)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
        (QuotientGroup.mk' N) n.1 = 0) :
    n ∈ commutator (QuotientGroup.mk' N).ker

theorem mem_commutator_ker_of_zcUniversalDifferential_eq_zero_pGroup_of_surjective
    (p : ℕ) [Fact (Nat.Prime p)]
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
    (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
    (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ)
    (n : ψ.ker)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
        ψ n.1 = 0) :
    n ∈ commutator ψ.ker

theorem mem_commutator_ker_of_zcFreeFoxDerivVec_eq_zero_pGroup_of_surj_factor
    (p : ℕ) [Fact (Nat.Prime p)]
    {Q : Type} [Group Q]
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
    (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
    (hn :
      FoxDifferential.zcFreeGroupFoxDerivativeVector
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
        (β.comp α) w = 0) :
    q ∈ commutator β.ker

theorem mem_commutator_ker_of_zcUnivDiff_eq_zero_pGroup_of_surj_factor
    (p : ℕ) [Fact (Nat.Prime p)]
    {Q : Type} [Group Q]
    [TopologicalSpace H] [IsTopologicalGroup H] [DiscreteTopology H]
    (hCtarget : ProCGroups.FiniteGroupClass.pGroup p H)
    (α : FreeGroup X →* Q) (hα : Function.Surjective α)
    (β : Q →* H) (hβ : Function.Surjective β)
    (q : β.ker) (w : FreeGroup X) (hw : α w = q.1)
    (hn :
      FoxDifferential.zcUniversalDifferential
        (ProCGroups.FiniteGroupClass.pGroup p : ProCGroups.FiniteGroupClass)
        (β.comp α) w = 0) :
    q ∈ commutator β.ker