ElementarySplitCriterion.lean

def regularFiberNorm
    {A Q B : Type u} [CommGroup A] [Group Q] [Finite Q] [Group B]
    (J : Subgroup Q) (ρ : J →* B) : (Q → A) →* (B → A)

theorem regularFiberNorm_equivariant
    {A Q B : Type u} [CommGroup A] [Group Q] [Finite Q] [Group B]
    (J : Subgroup Q) (ρ : J →* B) (j : J) (f : Q → A) :
    regularFiberNorm J ρ
      ((mulAutArrow (G := Q) (A := Q) (M := A)) (j : Q) f) =
      (mulAutArrow (G := B) (A := B) (M := A)) (ρ j) (regularFiberNorm J ρ f)

theorem isSigmaAbFaithful_singleton_of_elementarySplit_solutions
    (q : ℕ) [Fact q.Prime]
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions
      (FiniteGroupClass.abelianExponent q) G) :
    IsSigmaAbFaithful {q} G

theorem isSigmaAbFaithful_of_elementarySplit_solutions
    {sigma : Set ℕ} (hne : sigma.Nonempty)
    (hprime : ∀ q ∈ sigma, Nat.Prime q)
    (hsolve : ∀ q ∈ sigma, HasFiniteSplitAbelianKernelEmbeddingSolutions
      (FiniteGroupClass.abelianExponent q) G) :
    IsSigmaAbFaithful sigma G ∧ ∀ q ∈ sigma, IsSigmaAbFaithful {q} G

theorem isSigmaAbFaithful_of_abelianSigmaSplit_solutions
    {sigma : Set ℕ} (hne : sigma.Nonempty)
    (hprime : ∀ q ∈ sigma, Nat.Prime q)
    (hsolve : HasFiniteSplitAbelianKernelEmbeddingSolutions
      (FiniteGroupClass.sigmaGroup sigma) G) :
    IsSigmaAbFaithful sigma G ∧ ∀ q ∈ sigma, IsSigmaAbFaithful {q} G

theorem regular_split_problems_suffice
    {q : ℕ} [Fact q.Prime] (G : ProfiniteGrp.{u})
    (hregular :
      ∀ V : OpenNormalSubgroup G,
        let Q := G ⧸ (V : Subgroup G)
        let W := ProCGroups.WreathProducts.PermutationalWreathProduct
          (ULift.{u} (Multiplicative (ZMod q))) Q Q
        letI : TopologicalSpace W := ⊥
        ∃ θ : G →ₜ* W,
          Function.Surjective θ ∧
            ∀ g : G,
              (SemidirectProduct.rightHom : W →* Q) (θ g) =
                ProCGroups.ProC.OpenNormalSubgroup.quotientProj V g) :
    IsSigmaAbFaithful {q} G := by
  classical
  apply HasFiniteFaithfulAbelianSigmaEmbeddingSolutions.isSigmaAbFaithful
  intro H B hBfinite hBdiscrete π hπ
  have : Finite B := hBfinite
  have : DiscreteTopology B := hBdiscrete
  obtain ⟨V, _hVH, η, ρ, _hη, hρ, hηval, hρη, hpreimage⟩ :=
    exists_finiteQuotient_factor_of_openSubgroup H π hπ
  let Q := G ⧸ (V : Subgroup G)
  let J : Subgroup Q :=
    ((QuotientGroup.mk' (V : Subgroup G)).comp (H : Subgroup G).subtype).range
  let A := ULift.{u} (Multiplicative (ZMod q))
  let W := ProCGroups.WreathProducts.PermutationalWreathProduct A Q Q
  let : TopologicalSpace W := ⊥
  have : DiscreteTopology W := ⟨rfl⟩
  obtain ⟨θ, hθ, hθright⟩ := hregular V
  have hθcoord (g : G) : (θ g).right =
      ProCGroups.ProC.OpenNormalSubgroup.quotientProj V g := hθright g
  let N : Subgroup W := J.comap (SemidirectProduct.rightHom : W →* Q)
  have hθH (h : H) : θ (h : G) ∈ N := by
    change (θ (h : G)).right ∈ J
    rw [hθcoord]
    exact (hpreimage (h : G)).mpr h.property
  let θH : H →ₜ* N :=
    { toMonoidHom :=
        (θ.toMonoidHom.comp (H : Subgroup G).subtype).codRestrict N hθH
      continuous_toFun :=
        (θ.continuous_toFun.comp continuous_subtype_val).subtype_mk hθH }
  have hθHsurj : Function.Surjective θH := by
    intro w
    obtain ⟨x, hx⟩ := hθ (w : W)
    have hxH : x ∈ H := (hpreimage x).mp (by
      rw [← hθcoord x, hx]
      exact w.property)
    exact ⟨⟨x, hxH⟩, Subtype.ext hx⟩
  let φ : Q →* MulAut (Q → A) := mulAutArrow (G := Q) (A := Q) (M := A)
  let eN : N ≃* (Q → A) ⋊[φ.comp J.subtype] J :=
    ProCGroups.semidirectRightPreimageEquiv φ J
  let W_B := ProCGroups.WreathProducts.PermutationalWreathProduct A B B
  let push : (Q → A) ⋊[φ.comp J.subtype] J →* W_B :=
    SemidirectProduct.map (ProCGroups.regularWreathFiberNorm J ρ.toMonoidHom)
      ρ.toMonoidHom (by
        intro j
        apply MonoidHom.ext
        intro f
        exact ProCGroups.regularWreathFiberNorm_equivariant J ρ.toMonoidHom j f)
  have hpush : Function.Surjective push := by
    intro w
    obtain ⟨f, hf⟩ :=
      ProCGroups.regularWreathFiberNorm_surjective J ρ.toMonoidHom hρ w.left
    obtain ⟨j, hj⟩ := hρ w.right
    refine ⟨⟨f, j⟩, ?_⟩
    exact SemidirectProduct.ext hf hj
  let : TopologicalSpace W_B := ⊥
  have : DiscreteTopology W_B := ⟨rfl⟩
  have : Finite W_B := Finite.of_equiv ((B → A) × B)
    (show (B → A) × B ≃ W_B from SemidirectProduct.equivProd.symm)
  let E : TopGrp.{u} := TopGrp.of W_B
  let α : E →ₜ* B :=
    { toMonoidHom := (SemidirectProduct.rightHom : W_B →* B)
      continuous_toFun := continuous_of_discreteTopology }
  have hα : Function.Surjective α := SemidirectProduct.rightHom_surjective
  have hcomm : ∀ a b : α.toMonoidHom.ker, Commute (a : E) (b : E) :=
    regularWreathKernel_commute (A := A) (B := B)
  have hSigma : FiniteGroupClass.sigmaGroup {q} α.toMonoidHom.ker :=
    FiniteGroupClass.sigmaGroup_of_abelianExponent q (Set.mem_singleton q)
      (regularWreathKernel_cyclicZMod_mem_abelianExponent (B := B) q)
  have hfaith : Function.Injective
      (abelianKernelConjugation α.toMonoidHom hα hcomm) :=
    regularWreathKernel_conjugation_injective (A := A) (B := B)
  let ψ : N →ₜ* E :=
    { toMonoidHom := push.comp eN.toMonoidHom
      continuous_toFun := continuous_of_discreteTopology }
  refine ⟨E, inferInstance, inferInstance, α, hα, hcomm, hSigma, hfaith,
    ⟨⟨ψ.comp θH, (hpush.comp eN.surjective).comp hθHsurj, ?_⟩⟩⟩
  apply ContinuousMonoidHom.ext
  intro h
  change ρ ⟨(θ (h : G)).right, hθH h⟩ = π h
  have hcoord : (⟨(θ (h : G)).right, hθH h⟩ : J) = η h := by
    apply Subtype.ext
    exact (hθcoord (h : G)).trans (hηval h).symm
  rw [hcoord]
  exact DFunLike.congr_fun hρη h