UniversalProperty.lean

theorem proCResidualCore_le_of_proCQuotient
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
    (K : Subgroup G) [K.Normal]
    (hKclosed : IsClosed (K : Set G))
    (hK : HasOpenNormalBasisInClass C (G ⧸ K)) :
    proCResidualCore C G ≤ K

theorem hasOpenNormalBasisInClass_quotient_ker
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (f : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
    HasOpenNormalBasisInClass C (G ⧸ f.toMonoidHom.ker)

theorem map_proCResidualCore_le_of_hom
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →* H) (hφ : Continuous φ) :
    (proCResidualCore C G).map φ ≤ proCResidualCore C H

theorem map_proCResidualCore_le_of_continuousMonoidHom
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →ₜ* H) :
    (proCResidualCore C G).map φ.toMonoidHom ≤ proCResidualCore C H

theorem proCResidualCore_le_ker_of_continuousMonoidHom_to_proC
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
    proCResidualCore C G ≤ φ.toMonoidHom.ker

def lift_proCResidualCoreQuotient
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) :
    G ⧸ proCResidualCore C G →ₜ* H

theorem lift_proCResidualCoreQuotient_mk
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H) (x : G) :
    lift_proCResidualCoreQuotient (C := C) hHer φ hH
      (QuotientGroup.mk' (proCResidualCore C G) x) = φ x

theorem lift_proCResidualCoreQuotient_unique
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hHer : FiniteGroupClass.Hereditary C)
    (φ : G →ₜ* H) (hH : HasOpenNormalBasisInClass C H)
    (ψ : G ⧸ proCResidualCore C G →ₜ* H)
    (hψ : ∀ x : G, ψ (QuotientGroup.mk' (proCResidualCore C G) x) = φ x) :
    ψ = lift_proCResidualCoreQuotient (C := C) hHer φ hH

theorem map_proCResidualCore_eq_of_surjective
    {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
      [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
    {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H] [T2Space H]
    (hC : FiniteGroupClass.FullFormation C)
    (φ : G →* H) (hφ : Continuous φ) (hφsurj : Function.Surjective φ)
    (hcoreQuot :
      letI : (proCResidualCore C G).Normal := proCResidualCore_normal C G
      HasOpenNormalBasisInClass C (G ⧸ proCResidualCore C G)) :
    (proCResidualCore C G).map φ = proCResidualCore C H := by
  let R : Subgroup G := proCResidualCore C G
  have : R.Normal := proCResidualCore_normal C G
  let N : Subgroup H := R.map φ
  have hNnormal : N.Normal := by
    refine ⟨?_⟩
    intro y hy h
    rcases hy with ⟨x, hx, rfl⟩
    rcases hφsurj h with ⟨g, rfl⟩
    exact (Subgroup.mem_map).2 ⟨g * x * g⁻¹, (show R.Normal from inferInstance).conj_mem x hx g, by
      simp only [mul_assoc, map_mul, map_inv]⟩
  have hRclosed : IsClosed (R : Set G) := by
    simpa [R] using proCResidualCore_isClosed C G
  have : TotallyDisconnectedSpace (G ⧸ R) :=
    ProCGroups.totallyDisconnectedSpace_quotient_closedNormal R hRclosed
  have hNclosed : IsClosed (N : Set H) := by
    simpa [N, Subgroup.coe_map] using (hRclosed.isCompact.image hφ).isClosed
  have hmap_le :
      R.map φ ≤ proCResidualCore C H :=
    map_proCResidualCore_le_of_hom (C := C) hC.hereditary φ hφ
  have hRle : R ≤ Subgroup.comap φ N := by
    intro x hx
    exact (Subgroup.mem_comap).2 <| (Subgroup.mem_map).2 ⟨x, hx, rfl⟩
  let φₜ : G →ₜ* H :=
    { toMonoidHom := φ
      continuous_toFun := hφ }
  let βₜ : G ⧸ R →ₜ* H ⧸ N := QuotientGroup.mapₜ R N φₜ hRle
  let β : G ⧸ R →* H ⧸ N := βₜ.toMonoidHom
  have hβsurj : Function.Surjective β := by
    have hmkφ_surj : Function.Surjective (QuotientGroup.mk ∘ φ : G → H ⧸ N) := by
      intro y
      rcases QuotientGroup.mk'_surjective N y with ⟨h, rfl⟩
      rcases hφsurj h with ⟨g, rfl⟩
      exact ⟨g, rfl⟩
    exact QuotientGroup.map_surjective_of_surjective (N := R) (M := N) φ hmkφ_surj hRle
  have hNquot : HasOpenNormalBasisInClass C (H ⧸ N) :=
    HasOpenNormalBasisInClass.of_surjective hC.melnikovFormation.formation hcoreQuot βₜ hβsurj
  have hcoreH_le : proCResidualCore C H ≤ N :=
    proCResidualCore_le_of_proCQuotient (C := C) N hNclosed hNquot
  exact le_antisymm hmap_le hcoreH_le