ResidualAbelianizationPrimePowers.lean

theorem HasOpenNormalBasisInClass.eq_one_of_primePower_roots
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [T2Space G]
    (hG : HasOpenNormalBasisInClass (FiniteGroupClass.sigmaGroup sigma) G)
    (x : G)
    (hx : ∀ ℓ : ℕ, ℓ ∈ sigma → ℓ.Prime →
      ∀ s : ℕ, 0 < s → ∃ y : G, y ^ (ℓ ^ s) = x) : x = 1

theorem hasOpenNormalBasisInClass_sigma_of_primePower_exponent
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (ℓ : ℕ) (hℓ : ℓ.Prime) (hℓsigma : ℓ ∈ sigma) (s : ℕ)
    (hpow : ∀ x : G, x ^ (ℓ ^ s) = 1) :
    HasOpenNormalBasisInClass (FiniteGroupClass.sigmaGroup sigma) G

theorem residualAbelianization_hasOpenNormalBasisInClass
    {sigma : Set ℕ} (G : Type u)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] :
    HasOpenNormalBasisInClass (FiniteGroupClass.sigmaGroup sigma)
      (TopologicalAbelianization (G ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G))

theorem residualAbelianization_map_eq_iff_primePower
    {sigma : Set ℕ} (G : Type u)
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (x y : TopologicalAbelianization G) :
    let π : G →ₜ* (G ⧸ proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G) :=
      ⟨QuotientGroup.mk' _, QuotientGroup.continuous_mk⟩
    TopologicalAbelianization.map π x = TopologicalAbelianization.map π y ↔
      ∀ ℓ : ℕ, ℓ ∈ sigma → ℓ.Prime → ∀ s : ℕ, 0 < s →
        ∃ b : TopologicalAbelianization G, x = y * b ^ (ℓ ^ s) := by
  let R := proCResidualCore (FiniteGroupClass.sigmaGroup sigma) G
  let Q := G ⧸ R
  let π : G →ₜ* Q := ⟨QuotientGroup.mk' R, QuotientGroup.continuous_mk⟩
  let f := TopologicalAbelianization.map π
  change f x = f y ↔ _
  constructor
  · intro hxy ℓ hℓsigma hℓ s _
    let A := TopologicalAbelianization G
    let P : Subgroup A := (powMonoidHom (α := A) (ℓ ^ s)).range
    let powerMap : A →ₜ* A :=
      ⟨powMonoidHom (ℓ ^ s), continuous_id.pow _⟩
    have hPclosed : IsClosed (P : Set A) :=
      ContinuousMonoidHom.isClosed_range powerMap
    have : IsClosed (P : Set A) := hPclosed
    have : TotallyDisconnectedSpace A :=
      ProCGroups.totallyDisconnectedSpace_quotient_closedNormal
        (Subgroup.closedCommutator G) (Subgroup.isClosed_closedCommutator G)
    have : TotallyDisconnectedSpace (A ⧸ P) :=
      ProCGroups.totallyDisconnectedSpace_quotient_closedNormal P hPclosed
    let q : A →ₜ* (A ⧸ P) :=
      ⟨QuotientGroup.mk' P, QuotientGroup.continuous_mk⟩
    have hpow (a : A ⧸ P) : a ^ (ℓ ^ s) = 1 := by
      obtain ⟨a, rfl⟩ := QuotientGroup.mk'_surjective P a
      rw [← map_pow]
      exact (QuotientGroup.eq_one_iff (N := P) (a ^ (ℓ ^ s))).mpr ⟨a, rfl⟩
    have hAP := hasOpenNormalBasisInClass_sigma_of_primePower_exponent
      ℓ hℓ hℓsigma s hpow
    let ψ : Q →ₜ* (A ⧸ P) :=
      lift_proCResidualCoreQuotient
        (FiniteGroupClass.sigmaGroup_fullFormation sigma).hereditary
        (q.comp (TopologicalAbelianization.mkₜ G)) hAP
    let F := TopologicalAbelianization.lift ψ
    have hcompare (a : A) : F (f a) = q a := by
      obtain ⟨g, rfl⟩ := TopologicalAbelianization.surjective_mk G a
      change TopologicalAbelianization.lift ψ
        (TopologicalAbelianization.mk Q (QuotientGroup.mk' R g)) = _
      rw [TopologicalAbelianization.lift_apply_mk, lift_proCResidualCoreQuotient_mk]
      rfl
    have hq : q x = q y := (hcompare x).symm.trans ((congrArg F hxy).trans (hcompare y))
    have hmem : y⁻¹ * x ∈ P := QuotientGroup.eq.mp hq.symm
    obtain ⟨b, hb⟩ := hmem
    refine ⟨b, ?_⟩
    change b ^ (ℓ ^ s) = y⁻¹ * x at hb
    rw [hb, ← mul_assoc, mul_inv_cancel, one_mul]
  · intro hxy
    have hA := residualAbelianization_hasOpenNormalBasisInClass (sigma := sigma) G
    have hzero : f x * (f y)⁻¹ = 1 := by
      apply hA.eq_one_of_primePower_roots
      intro ℓ hℓsigma hℓ s hs
      obtain ⟨b, hb⟩ := hxy ℓ hℓsigma hℓ s hs
      refine ⟨f b, ?_⟩
      rw [hb, map_mul, map_pow, mul_comm (f y), mul_assoc, mul_inv_cancel, mul_one]
    exact mul_inv_eq_one.mp hzero

theorem residualAbelianizationQuotientConjugation_eq_one_iff_primePower
    {sigma : Set ℕ} {G : Type u}
    [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    (N : Subgroup G) [N.Normal] (hN : IsClosed (N : Set G)) :
    residualAbelianizationQuotientConjugation
        (FiniteGroupClass.sigmaGroup_fullFormation sigma) N hN = 1 ↔
      ∀ g : G ⧸ N, ∀ a : TopologicalAbelianization N,
        ∀ ℓ : ℕ, ℓ ∈ sigma → ℓ.Prime → ∀ s : ℕ, 0 < s →
          ∃ b : TopologicalAbelianization N,
            quotientConjugationTopologicalAbelianizationMap N g a = a * b ^ (ℓ ^ s)