feat(Topology/Group/Profinite): Profinite group is limit of finite group (#16992)

Prove that any profinite group is limit of finite groups.

Author: Thmoas-Guan

Mathlib.lean

@@ -5097,6 +5097,7 @@ import Mathlib.Topology.Algebra.Affine
 import Mathlib.Topology.Algebra.Algebra
 import Mathlib.Topology.Algebra.Algebra.Rat
 import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
+import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
 import Mathlib.Topology.Algebra.ClopenNhdofOne
 import Mathlib.Topology.Algebra.ClosedSubgroup
 import Mathlib.Topology.Algebra.ConstMulAction

Mathlib/Algebra/Group/Subgroup/Basic.lean

@@ -849,6 +849,15 @@ theorem inf_subgroupOf_inf_normal_of_left {A' A : Subgroup G} (B : Subgroup G) (
 instance normal_inf_normal (H K : Subgroup G) [hH : H.Normal] [hK : K.Normal] : (H ⊓ K).Normal :=
   ⟨fun n hmem g => ⟨hH.conj_mem n hmem.1 g, hK.conj_mem n hmem.2 g⟩⟩
 
+@[to_additive]
+theorem normal_iInf_normal {ι : Type*} {a : ι → Subgroup G}
+    (norm : ∀ i : ι , (a i).Normal) : (iInf a).Normal := by
+  constructor
+  intro g g_in_iInf h
+  rw [Subgroup.mem_iInf] at g_in_iInf ⊢
+  intro i
+  exact (norm i).conj_mem g (g_in_iInf i) h
+
 @[to_additive]
 theorem SubgroupNormal.mem_comm {H K : Subgroup G} (hK : H ≤ K) [hN : (H.subgroupOf K).Normal]
     {a b : G} (hb : b ∈ K) (h : a * b ∈ H) : b * a ∈ H := by

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Basic.lean

@@ -25,6 +25,14 @@ disconnected.
 
 * `ofClosedSubgroup` : A closed subgroup of a profinite group is profinite.
 
+# TODO
+
+As discussion in `https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/Refactor.20
+Category.20of.20ProfiniteGrp.20and.20ContinuousMulEquiv/near/493290115`
+
+* Refactor the category of `ProfiniteGrp` into one-field structure as in `AlgebraCat`
+
+* Prove `(forget ProfiniteGrp.{u}).ReflectsIsomorphisms` using `profiniteGrpToProfinite`
 -/
 
 universe u v
@@ -68,6 +76,7 @@ instance : CoeSort ProfiniteGrp (Type u) where
 attribute [instance] group topologicalGroup
     ProfiniteAddGrp.addGroup ProfiniteAddGrp.topologicalAddGroup
 
+--TODO: Refactor into one-field structure as in `AlgebraCat`
 @[to_additive]
 instance : Category ProfiniteGrp where
   Hom A B := ContinuousMonoidHom A B

Mathlib/Topology/Algebra/Category/ProfiniteGrp/Limits.lean

@@ -0,0 +1,149 @@
+/-
+Copyright (c) 2024 Nailin Guan. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Nailin Guan, Youle Fang, Jujian Zhang, Yuyang Zhao
+-/
+import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
+import Mathlib.Topology.Algebra.ClopenNhdofOne
+
+/-!
+# A profinite group is the projective limit of finite groups
+
+We define the topological group isomorphism between a profinite group and the projective limit of
+its quotients by open normal subgroups.
+
+## Main definitions
+
+* `toFiniteQuotientFunctor` : The functor from `OpenNormalSubgroup P` to `FiniteGrp`
+  sending an open normal subgroup `U` to `P ⧸ U`, where `P : ProfiniteGrp`.
+
+* `toLimit` : The continuous homomorphism from a profinite group `P` to
+  the projective limit of its quotients by open normal subgroups ordered by inclusion.
+
+* `ContinuousMulEquivLimittoFiniteQuotientFunctor` : The `toLimit` is a
+  `ContinuousMulEquiv`
+
+## Main Statements
+
+* `OpenNormalSubgroupSubClopenNhdsOfOne` : For any open neighborhood of `1` there is an
+  open normal subgroup contained in it.
+
+-/
+
+universe u
+
+open CategoryTheory TopologicalGroup
+
+namespace ProfiniteGrp
+
+instance (P : ProfiniteGrp) : SmallCategory (OpenNormalSubgroup P) :=
+  Preorder.smallCategory (OpenNormalSubgroup ↑P.toProfinite.toTop)
+
+/-- The functor from `OpenNormalSubgroup P` to `FiniteGrp` sending `U` to `P ⧸ U`,
+where `P : ProfiniteGrp`. -/
+def toFiniteQuotientFunctor (P : ProfiniteGrp) : OpenNormalSubgroup P ⥤ FiniteGrp := {
+    obj := fun H => FiniteGrp.of (P ⧸ H.toSubgroup)
+    map := fun fHK => QuotientGroup.map _ _ (.id _) (leOfHom fHK)
+    map_id _ := QuotientGroup.map_id _
+    map_comp f g := (QuotientGroup.map_comp_map
+      _ _ _ (.id _) (.id _) (leOfHom f) (leOfHom g)).symm }
+
+/--The `MonoidHom` from a profinite group `P` to  the projective limit of its quotients by
+open normal subgroups ordered by inclusion.-/
+def toLimit_fun (P : ProfiniteGrp.{u}) : P →*
+    limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp) where
+  toFun p := ⟨fun _ => QuotientGroup.mk p, fun _ => rfl⟩
+  map_one' := Subtype.val_inj.mp rfl
+  map_mul' _ _ := Subtype.val_inj.mp rfl
+
+lemma toLimit_fun_continuous (P : ProfiniteGrp.{u}) : Continuous (toLimit_fun P) := by
+  apply continuous_induced_rng.mpr (continuous_pi _)
+  intro H
+  dsimp only [Functor.comp_obj, CompHausLike.toCompHausLike_obj, CompHausLike.compHausLikeToTop_obj,
+    CompHausLike.coe_of, Functor.comp_map, CompHausLike.toCompHausLike_map,
+    CompHausLike.compHausLikeToTop_map, Set.mem_setOf_eq, toLimit_fun,
+    MonoidHom.coe_mk, OneHom.coe_mk, Function.comp_apply]
+  apply Continuous.mk
+  intro s _
+  rw [← (Set.biUnion_preimage_singleton QuotientGroup.mk s)]
+  refine isOpen_iUnion (fun i ↦ isOpen_iUnion (fun _ ↦ ?_))
+  convert IsOpen.leftCoset H.toOpenSubgroup.isOpen' (Quotient.out i)
+  ext x
+  simp only [Set.mem_preimage, Set.mem_singleton_iff]
+  nth_rw 1 [← QuotientGroup.out_eq' i, eq_comm, QuotientGroup.eq]
+  exact Iff.symm (Set.mem_smul_set_iff_inv_smul_mem)
+
+/-- The morphism in the category of `ProfiniteGrp` from a profinite group `P` to
+the projective limit of its quotients by open normal subgroups ordered by inclusion.-/
+def toLimit (P : ProfiniteGrp.{u}) : P ⟶
+    limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp) := {
+  toLimit_fun P with
+  continuous_toFun := toLimit_fun_continuous P }
+
+/--An auxiliary result, superceded by `toLimit_surjective`.-/
+theorem denseRange_toLimit (P : ProfiniteGrp.{u}) : DenseRange (toLimit P) := by
+  apply dense_iff_inter_open.mpr
+  rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩
+  simp_rw [← hsv, Set.mem_preimage] at uDefaultSpec
+  rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
+  let M := iInf (fun (j : J) => j.1.1.1)
+  have hM : M.Normal := Subgroup.normal_iInf_normal fun j => j.1.isNormal'
+  have hMOpen : IsOpen (M : Set P) := by
+    rw [Subgroup.coe_iInf]
+    exact isOpen_iInter_of_finite fun i => i.1.1.isOpen'
+  let m : OpenNormalSubgroup P := { M with isOpen' := hMOpen }
+  rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩
+  use (toLimit P).toFun origin
+  refine ⟨?_, origin, rfl⟩
+  rw [← hsv]
+  apply hJ2
+  intro a a_in_J
+  let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => j.1.1.1) ⟨a, a_in_J⟩).hom
+  rw [← (P.toLimit.toFun origin).property M_to_Na]
+  show (P.toFiniteQuotientFunctor.map M_to_Na) (QuotientGroup.mk' M origin) ∈ _
+  rw [horigin]
+  exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).2
+
+theorem toLimit_surjective (P : ProfiniteGrp.{u}) : Function.Surjective (toLimit P) := by
+  have : IsClosed (Set.range P.toLimit) :=
+    P.toLimit.continuous_toFun.isClosedMap.isClosed_range
+  rw [← Set.range_eq_univ, ← closure_eq_iff_isClosed.mpr this,
+    Dense.closure_eq (denseRange_toLimit P)]
+
+theorem toLimit_injective (P : ProfiniteGrp.{u}) : Function.Injective (toLimit P) := by
+  show Function.Injective (toLimit P).toMonoidHom
+  rw [← MonoidHom.ker_eq_bot_iff, Subgroup.eq_bot_iff_forall]
+  intro x h
+  by_contra xne1
+  rcases exist_openNormalSubgroup_sub_open_nhd_of_one (isOpen_compl_singleton)
+    (Set.mem_compl_singleton_iff.mpr fun a => xne1 a.symm) with ⟨H, hH⟩
+  exact hH ((QuotientGroup.eq_one_iff x).mp (congrFun (Subtype.val_inj.mpr h) H)) rfl
+
+/-- The topological group isomorphism between a profinite group and the projective limit of
+its quotients by open normal subgroups -/
+noncomputable def continuousMulEquivLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) :
+    P ≃ₜ* (limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp)) := {
+  (Continuous.homeoOfEquivCompactToT2 (f := Equiv.ofBijective _
+  ⟨toLimit_injective P, toLimit_surjective P⟩)
+    P.toLimit.continuous_toFun)
+  with
+  map_mul' := (toLimit P).map_mul' }
+
+--TODO : Refactor using `(forget ProfiniteGrp.{u}).ReflectsIsomorphisms` after it is proved.
+/-- The isomorphism in the category of profinite group between a profinite group and
+the projective limit of its quotients by open normal subgroups -/
+noncomputable def isoLimittoFiniteQuotientFunctor (P : ProfiniteGrp.{u}) :
+    P ≅ (limit (toFiniteQuotientFunctor P ⋙ forget₂ FiniteGrp ProfiniteGrp)) where
+  hom := P.toLimit
+  inv := { (continuousMulEquivLimittoFiniteQuotientFunctor P).symm.toMonoidHom with
+    continuous_toFun := (continuousMulEquivLimittoFiniteQuotientFunctor P).continuous_invFun}
+  hom_inv_id := by
+    ext x
+    exact ContinuousMulEquiv.symm_apply_apply
+      (continuousMulEquivLimittoFiniteQuotientFunctor P) x
+  inv_hom_id := by
+    ext x
+    exact ContinuousMulEquiv.apply_symm_apply
+      (continuousMulEquivLimittoFiniteQuotientFunctor P) x
+
+end ProfiniteGrp

Mathlib/Topology/Algebra/ClopenNhdofOne.lean

@@ -6,6 +6,7 @@ Authors: Nailin Guan, Yi Song, Xuchun Li
 import Mathlib.GroupTheory.Index
 import Mathlib.Topology.Algebra.ClosedSubgroup
 import Mathlib.Topology.Algebra.OpenSubgroup
+import Mathlib.Topology.Separation.Profinite
 /-!
 # Existence of an open normal subgroup in any clopen neighborhood of the neutral element
 
@@ -28,3 +29,15 @@ theorem exist_openNormalSubgroup_sub_clopen_nhd_of_one {G : Type*} [Group G] [To
   exact fun _ b ↦ hH (H.normalCore_le b)
 
 end TopologicalGroup
+
+namespace ProfiniteGrp
+
+theorem exist_openNormalSubgroup_sub_open_nhd_of_one {G : Type*} [Group G] [TopologicalSpace G]
+    [TopologicalGroup G] [CompactSpace G] [TotallyDisconnectedSpace G] {U : Set G}
+    (UOpen : IsOpen U) (einU : 1 ∈ U) : ∃ H : OpenNormalSubgroup G, (H : Set G) ⊆ U := by
+  rcases ((Filter.HasBasis.mem_iff' ((nhds_basis_clopen (1 : G))) U ).mp <|
+    mem_nhds_iff.mpr (by use U)) with ⟨W, hW, h⟩
+  rcases TopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhd_of_one hW.2 hW.1 with ⟨H, hH⟩
+  exact ⟨H, fun _ a ↦ h (hH a)⟩
+
+end ProfiniteGrp

Mathlib/Topology/Algebra/OpenSubgroup.lean

@@ -1,7 +1,7 @@
 /-
 Copyright (c) 2019 Johan Commelin. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: Johan Commelin, Nailin Guan
+Authors: Johan Commelin, Nailin Guan, Yi Song, Xuchun Li
 -/
 import Mathlib.Algebra.Module.Submodule.Lattice
 import Mathlib.RingTheory.Ideal.Defs
@@ -10,7 +10,7 @@ import Mathlib.Topology.Algebra.Ring.Basic
 import Mathlib.Topology.Sets.Opens
 
 /-!
-# Open subgroups of a topological groups
+# Open subgroups of a topological group
 
 This files builds the lattice `OpenSubgroup G` of open subgroups in a topological group `G`,
 and its additive version `OpenAddSubgroup`.  This lattice has a top element, the subgroup of all