Skip to content

Commit 66cbf96

Browse files
adamtopazpre-commit-ci-lite[bot]
adamtopaz
and
pre-commit-ci-lite[bot]
committed
feat: Profinite completion of groups (#34893)
Co-authored-by: pre-commit-ci-lite[bot] <117423508+pre-commit-ci-lite[bot]@users.noreply.github.com>
1 parent e8bd29a commit 66cbf96

File tree

6 files changed

+395
-18
lines changed

6 files changed

+395
-18
lines changed

‎Mathlib.lean‎

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -4400,6 +4400,7 @@ public import Mathlib.GroupTheory.EckmannHilton
44004400
public import Mathlib.GroupTheory.Exponent
44014401
public import Mathlib.GroupTheory.FiniteAbelian.Basic
44024402
public import Mathlib.GroupTheory.FiniteAbelian.Duality
4403+
public import Mathlib.GroupTheory.FiniteIndexNormalSubgroup
44034404
public import Mathlib.GroupTheory.Finiteness
44044405
public import Mathlib.GroupTheory.FixedPointFree
44054406
public import Mathlib.GroupTheory.Frattini
@@ -6954,6 +6955,7 @@ public import Mathlib.Topology.Algebra.Algebra.Equiv
69546955
public import Mathlib.Topology.Algebra.Algebra.Rat
69556956
public import Mathlib.Topology.Algebra.AsymptoticCone
69566957
public import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
6958+
public import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Completion
69576959
public import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
69586960
public import Mathlib.Topology.Algebra.ClopenNhdofOne
69596961
public import Mathlib.Topology.Algebra.ConstMulAction

‎Mathlib/GroupTheory/FiniteIndexNormalSubgroup.lean‎

Lines changed: 155 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,155 @@
1+
/-
2+
Copyright (c) 2026 Adam Topaz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Adam Topaz
5+
-/
6+
module
7+
8+
public import Mathlib.GroupTheory.Index
9+
10+
/-!
11+
# Finite-index normal subgroups
12+
13+
This file builds the lattice `FiniteIndexNormalSubgroup G` of finite-index normal subgroups of a
14+
group `G`, and its additive version `FiniteIndexNormalAddSubgroup`.
15+
16+
This is used primarily in the definition of the profinite completion of a group.
17+
-/
18+
19+
@[expose] public section
20+
21+
section
22+
23+
/-- The type of finite-index normal subgroups of a group. -/
24+
@[ext]
25+
structure FiniteIndexNormalSubgroup (G : Type*) [Group G] extends Subgroup G where
26+
isNormal' : toSubgroup.Normal := by infer_instance
27+
isFiniteIndex' : toSubgroup.FiniteIndex := by infer_instance
28+
29+
/-- The type of finite-index normal additive subgroups of an additive group. -/
30+
@[ext]
31+
structure FiniteIndexNormalAddSubgroup (G : Type*) [AddGroup G] extends AddSubgroup G where
32+
isNormal' : toAddSubgroup.Normal := by infer_instance
33+
isFiniteIndex' : toAddSubgroup.FiniteIndex := by infer_instance
34+
35+
attribute [to_additive] FiniteIndexNormalSubgroup
36+
37+
namespace FiniteIndexNormalSubgroup
38+
39+
variable {G : Type*} [Group G]
40+
41+
@[to_additive]
42+
theorem toSubgroup_injective : Function.Injective
43+
(fun H ↦ H.toSubgroup : FiniteIndexNormalSubgroup G → Subgroup G) :=
44+
fun A B h ↦ by
45+
ext
46+
dsimp at h
47+
rw [h]
48+
49+
@[to_additive]
50+
instance : SetLike (FiniteIndexNormalSubgroup G) G where
51+
coe U := U.1
52+
coe_injective' _ _ h := toSubgroup_injective <| SetLike.ext' h
53+
54+
@[to_additive]
55+
instance : PartialOrder (FiniteIndexNormalSubgroup G) := .ofSetLike (FiniteIndexNormalSubgroup G) G
56+
57+
@[to_additive]
58+
instance : SubgroupClass (FiniteIndexNormalSubgroup G) G where
59+
mul_mem := Subsemigroup.mul_mem' _
60+
one_mem U := U.one_mem'
61+
inv_mem := Subgroup.inv_mem' _
62+
63+
@[to_additive]
64+
instance : Coe (FiniteIndexNormalSubgroup G) (Subgroup G) where
65+
coe H := H.toSubgroup
66+
67+
@[to_additive]
68+
instance (H : FiniteIndexNormalSubgroup G) : H.toSubgroup.Normal := H.isNormal'
69+
70+
@[to_additive]
71+
instance (H : FiniteIndexNormalSubgroup G) : H.toSubgroup.FiniteIndex := H.isFiniteIndex'
72+
73+
@[to_additive]
74+
instance instPartialOrderFiniteIndexNormalSubgroup : PartialOrder (FiniteIndexNormalSubgroup G) :=
75+
inferInstance
76+
77+
@[to_additive]
78+
instance instInfFiniteIndexNormalSubgroup : Min (FiniteIndexNormalSubgroup G) :=
79+
⟨fun U V ↦ {
80+
toSubgroup := U.toSubgroup ⊓ V.toSubgroup
81+
isNormal' := Subgroup.normal_inf_normal U.toSubgroup V.toSubgroup
82+
}⟩
83+
84+
@[to_additive]
85+
instance instSemilatticeInfFiniteIndexNormalSubgroup :
86+
SemilatticeInf (FiniteIndexNormalSubgroup G) :=
87+
SetLike.coe_injective.semilatticeInf ((↑) : FiniteIndexNormalSubgroup G → Set G) fun _ _ ↦ rfl
88+
89+
@[to_additive]
90+
instance : Max (FiniteIndexNormalSubgroup G) :=
91+
⟨fun U V ↦ {
92+
toSubgroup := U.toSubgroup ⊔ V.toSubgroup
93+
isNormal' := Subgroup.sup_normal U.toSubgroup V.toSubgroup
94+
isFiniteIndex' := Subgroup.finiteIndex_of_le
95+
(H := U.toSubgroup) (K := U.toSubgroup ⊔ V.toSubgroup) le_sup_left
96+
}⟩
97+
98+
@[to_additive]
99+
instance instSemilatticeSupFiniteIndexNormalSubgroup :
100+
SemilatticeSup (FiniteIndexNormalSubgroup G) :=
101+
toSubgroup_injective.semilatticeSup _ (fun _ _ ↦ rfl)
102+
103+
@[to_additive]
104+
instance : Lattice (FiniteIndexNormalSubgroup G) where
105+
106+
/-- Bundle a subgroup with typeclass assumptions of normality and finite index. -/
107+
@[to_additive
108+
/-- Bundle an additive subgroup with typeclass assumptions of normality and finite index. -/]
109+
def ofSubgroup (H : Subgroup G) [H.Normal] [H.FiniteIndex] : FiniteIndexNormalSubgroup G :=
110+
{ toSubgroup := H }
111+
112+
@[to_additive (attr := simp)]
113+
theorem toSubgroup_ofSubgroup (H : Subgroup G) [H.Normal] [H.FiniteIndex] :
114+
((ofSubgroup H : FiniteIndexNormalSubgroup G) : Subgroup G) = H :=
115+
rfl
116+
117+
section Comap
118+
119+
variable {H : Type*} {N : Type*} [Group H] [Group N]
120+
121+
/-- The preimage of a finite-index normal subgroup under a group homomorphism. -/
122+
@[to_additive
123+
/-- The preimage of a finite-index normal additive subgroup under an additive homomorphism. -/]
124+
def comap (f : G →* H) (K : FiniteIndexNormalSubgroup H) : FiniteIndexNormalSubgroup G where
125+
toSubgroup := K.toSubgroup.comap f
126+
isFiniteIndex' := by
127+
let g : G →* (H ⧸ K.toSubgroup) := (QuotientGroup.mk' K.toSubgroup).comp f
128+
have hker : K.toSubgroup.comap f = g.ker := by
129+
simpa using MonoidHom.comap_ker (g := QuotientGroup.mk' K.toSubgroup) (f := f)
130+
simpa [hker] using (inferInstance : g.ker.FiniteIndex)
131+
132+
@[to_additive (attr := simp)]
133+
theorem toSubgroup_comap (f : G →* H) (K : FiniteIndexNormalSubgroup H) :
134+
((comap f K : FiniteIndexNormalSubgroup G) : Subgroup G) = (K : Subgroup H).comap f :=
135+
rfl
136+
137+
@[to_additive]
138+
theorem comap_mono (f : G →* H) {K L : FiniteIndexNormalSubgroup H} (h : K ≤ L) :
139+
comap f K ≤ comap f L :=
140+
fun _ hx ↦ h hx
141+
142+
@[to_additive (attr := simp)]
143+
theorem comap_id (K : FiniteIndexNormalSubgroup G) : comap (MonoidHom.id G) K = K := by
144+
rfl
145+
146+
@[to_additive (attr := simp)]
147+
theorem comap_comp (f : G →* H) (g : H →* N) (K : FiniteIndexNormalSubgroup N) :
148+
comap (g.comp f) K = comap f (comap g K) := by
149+
rfl
150+
151+
end Comap
152+
153+
end FiniteIndexNormalSubgroup
154+
155+
end

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

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -227,13 +227,19 @@ def ofFiniteGrp (G : FiniteGrp) : ProfiniteGrp :=
227227
letI : IsTopologicalGroup G := {}
228228
of G
229229

230+
/-- A morphism of `FiniteGrp` induces a morphism of the associated profinite groups. -/
231+
@[to_additive /-- A morphism of `FiniteAddGrp` induces a morphism of the associated profinite
232+
additive groups. -/]
233+
def ofFiniteGrpHom {G H : FiniteGrp.{u}} (f : G ⟶ H) : ofFiniteGrp G ⟶ ofFiniteGrp H :=
234+
ConcreteCategory.ofHom ⟨f.hom.hom, by continuity⟩
235+
230236
set_option backward.privateInPublic true in
231237
set_option backward.privateInPublic.warn false in
232238
@[to_additive]
233239
instance : HasForget₂ FiniteGrp ProfiniteGrp where
234240
forget₂ :=
235241
{ obj := ofFiniteGrp
236-
map f := ⟨f.hom.hom, by continuity⟩ }
242+
map := ofFiniteGrpHom }
237243

238244
@[to_additive]
239245
instance : HasForget₂ ProfiniteGrp GrpCat where

‎Mathlib/Topology/Algebra/Category/ProfiniteGrp/Completion.lean‎

Lines changed: 196 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,196 @@
1+
/-
2+
Copyright (c) 2026 Adam Topaz. All rights reserved.
3+
Released under Apache 2.0 license as described in the file LICENSE.
4+
Authors: Adam Topaz
5+
-/
6+
module
7+
8+
public import Mathlib.GroupTheory.FiniteIndexNormalSubgroup
9+
public import Mathlib.Topology.Algebra.Category.ProfiniteGrp.Limits
10+
11+
/-!
12+
# Profinite completion of groups
13+
14+
We define the profinite completion of a group as the limit of its finite quotients,
15+
and prove its universal property.
16+
-/
17+
18+
@[expose] public section
19+
20+
namespace OpenNormalSubgroup
21+
22+
variable {G : Type*} [Group G] [TopologicalSpace G]
23+
24+
/-- An open normal subgroup of a compact topological group has finite index. -/
25+
@[to_additive
26+
/-- An open normal additive subgroup of a compact topological additive group has finite index. -/]
27+
def toFiniteIndexNormalSubgroup [CompactSpace G] [ContinuousMul G]
28+
(H : OpenNormalSubgroup G) : FiniteIndexNormalSubgroup G :=
29+
letI : H.toSubgroup.FiniteIndex := Subgroup.finiteIndex_of_finite_quotient
30+
FiniteIndexNormalSubgroup.ofSubgroup H.toSubgroup
31+
32+
@[to_additive]
33+
theorem toFiniteIndexNormalSubgroup_mono [CompactSpace G] [ContinuousMul G]
34+
{H K : OpenNormalSubgroup G} (h : H ≤ K) :
35+
H.toFiniteIndexNormalSubgroup ≤ K.toFiniteIndexNormalSubgroup :=
36+
fun _ hx ↦ h hx
37+
38+
@[to_additive]
39+
theorem toFiniteIndexNormalSubgroup_injective [CompactSpace G] [ContinuousMul G] :
40+
Function.Injective (toFiniteIndexNormalSubgroup (G := G)) := by
41+
intro H K h
42+
apply toSubgroup_injective
43+
exact congrArg (fun L : FiniteIndexNormalSubgroup G ↦ (L : Subgroup G)) h
44+
45+
end OpenNormalSubgroup
46+
47+
namespace ProfiniteGrp
48+
49+
open CategoryTheory
50+
51+
universe u
52+
53+
namespace ProfiniteCompletion
54+
55+
variable (G : GrpCat.{u})
56+
57+
/-- The diagram of finite quotients indexed by finite-index normal subgroups of `G`. -/
58+
def finiteGrpDiagram : FiniteIndexNormalSubgroup G ⥤ FiniteGrp.{u} where
59+
obj H := FiniteGrp.of <| G ⧸ H.toSubgroup
60+
map f := FiniteGrp.ofHom <| QuotientGroup.map _ _ (MonoidHom.id _) f.le
61+
map_id H := by ext ⟨x⟩; rfl
62+
map_comp f g := by ext ⟨x⟩; rfl
63+
64+
/-- The finite-quotient diagram viewed in `ProfiniteGrp`. -/
65+
def diagram : FiniteIndexNormalSubgroup G ⥤ ProfiniteGrp.{u} :=
66+
finiteGrpDiagram _ ⋙ forget₂ _ _
67+
68+
/-- The profinite completion of `G` as a projective limit. -/
69+
def completion : ProfiniteGrp.{u} := limit (diagram G)
70+
71+
/-- The canonical map from `G` to its profinite completion, as a function. -/
72+
def etaFn (x : G) : completion G := ⟨fun _ => QuotientGroup.mk x, fun _ _ _ => rfl⟩
73+
74+
/-- The canonical morphism from `G` to its profinite completion. -/
75+
def eta : G ⟶ GrpCat.of (completion G) := GrpCat.ofHom {
76+
toFun := etaFn G
77+
map_one' := rfl
78+
map_mul' _ _ := rfl
79+
}
80+
81+
lemma denseRange : DenseRange (etaFn G) := by
82+
apply dense_iff_inter_open.mpr
83+
rintro U ⟨s, hsO, hsv⟩ ⟨⟨spc, hspc⟩, uDefaultSpec⟩
84+
rw [← hsv, Set.mem_preimage] at uDefaultSpec
85+
rcases (isOpen_pi_iff.mp hsO) _ uDefaultSpec with ⟨J, fJ, hJ1, hJ2⟩
86+
let M : Subgroup G := iInf fun (j : J) => j.val
87+
have hM : M.Normal := Subgroup.normal_iInf_normal fun j => inferInstance
88+
have hMFinite : M.FiniteIndex := by
89+
apply Subgroup.finiteIndex_iInf
90+
infer_instance
91+
let m : FiniteIndexNormalSubgroup G := { toSubgroup := M }
92+
rcases QuotientGroup.mk'_surjective M (spc m) with ⟨origin, horigin⟩
93+
use etaFn G origin
94+
refine ⟨?_, origin, rfl⟩
95+
rw [← hsv]
96+
apply hJ2
97+
intro a a_in_J
98+
let M_to_Na : m ⟶ a := (iInf_le (fun (j : J) => (j.val.toSubgroup)) ⟨a, a_in_J⟩).hom
99+
rw [← (etaFn G origin).property M_to_Na]
100+
dsimp [etaFn] at ⊢ horigin
101+
rw [horigin]
102+
exact Set.mem_of_eq_of_mem (hspc M_to_Na) (hJ1 a a_in_J).right
103+
104+
variable {G}
105+
variable {P : ProfiniteGrp.{u}}
106+
107+
/-- The preimage of an open normal subgroup under a morphism to a profinite group. -/
108+
def preimage (f : G ⟶ GrpCat.of P) (H : OpenNormalSubgroup P) : FiniteIndexNormalSubgroup G :=
109+
H.toFiniteIndexNormalSubgroup.comap f.hom
110+
111+
lemma preimage_le {f : G ⟶ GrpCat.of P} {H K : OpenNormalSubgroup P}
112+
(h : H ≤ K) : preimage f H ≤ preimage f K :=
113+
FiniteIndexNormalSubgroup.comap_mono _ h
114+
115+
/-- The induced map on finite quotients coming from a morphism to `P`. -/
116+
def quotientMap (f : G ⟶ GrpCat.of P) (H : OpenNormalSubgroup P) :
117+
FiniteGrp.of (G ⧸ (preimage f H).toSubgroup) ⟶ FiniteGrp.of (P ⧸ H.toSubgroup) :=
118+
FiniteGrp.ofHom <| QuotientGroup.map _ _ f.hom <| fun _ h => h
119+
120+
/-- The universal morphism from the profinite completion to `P`. -/
121+
noncomputable
122+
def lift (f : G ⟶ GrpCat.of P) : completion G ⟶ P :=
123+
P.isLimitCone.lift ⟨_, {
124+
app H := (limitCone (diagram G)).π.app _ ≫ (ofFiniteGrpHom <| quotientMap f H)
125+
naturality := by
126+
intro X Y g
127+
ext ⟨x, hx⟩
128+
-- TODO: `dsimp` should handle this `change`; investigate missing simp lemmas in the
129+
-- `ProfiniteGrp` / `CompHausLike` API.
130+
change quotientMap f Y (x <| preimage f Y) =
131+
P.diagram.map g (quotientMap _ _ <| x <| preimage f X)
132+
have := hx <| preimage_le (f := f) g.le |>.hom
133+
obtain ⟨t, ht⟩ : ∃ g : G, QuotientGroup.mk g = x (preimage f X) :=
134+
QuotientGroup.mk_surjective (x (preimage f X))
135+
rw [← this, ← ht]
136+
have := P.cone.π.naturality g
137+
apply_fun fun q => q (f t) at this
138+
exact this
139+
}⟩
140+
141+
@[reassoc (attr := simp)]
142+
lemma lift_eta (f : G ⟶ GrpCat.of P) : eta G ≫ (forget₂ _ _).map (lift f) = f := by
143+
let e := isoLimittoFiniteQuotientFunctor P
144+
rw [← (forget₂ ProfiniteGrp GrpCat).mapIso e |>.cancel_iso_hom_right]
145+
dsimp
146+
rw [Category.assoc, ← (forget₂ ProfiniteGrp GrpCat).map_comp (lift f) e.hom]
147+
change eta G ≫ ((forget₂ _ _).map ((_ ≫ e.inv) ≫ e.hom)) = _
148+
simp only [Category.assoc, Iso.inv_hom_id]
149+
rfl
150+
151+
lemma lift_unique (f g : completion G ⟶ P)
152+
(h : eta G ≫ (forget₂ _ _).map f = eta G ≫ (forget₂ _ _).map g) : f = g := by
153+
ext x
154+
apply congrFun
155+
refine (denseRange (G := G)).equalizer f.hom.continuous_toFun g.hom.continuous_toFun ?_
156+
funext y
157+
simpa [GrpCat.comp_apply] using (ConcreteCategory.congr_hom h y)
158+
159+
end ProfiniteCompletion
160+
161+
/-- The profinite completion functor. -/
162+
@[simps]
163+
noncomputable def profiniteCompletion : GrpCat.{u} ⥤ ProfiniteGrp.{u} where
164+
obj G := ProfiniteCompletion.completion G
165+
map f := ProfiniteCompletion.lift <| f ≫ ProfiniteCompletion.eta _
166+
map_id G := by
167+
apply ProfiniteCompletion.lift_unique
168+
cat_disch
169+
map_comp f g := by
170+
apply ProfiniteCompletion.lift_unique
171+
cat_disch
172+
173+
namespace ProfiniteCompletion
174+
175+
/-- The hom-set equivalence exhibiting the adjunction. -/
176+
noncomputable
177+
def homEquiv (G : GrpCat.{u}) (P : ProfiniteGrp.{u}) :
178+
(completion G ⟶ P) ≃ (G ⟶ GrpCat.of P) where
179+
toFun f := eta G ≫ (forget₂ _ _).map f
180+
invFun f := lift f
181+
left_inv f := by apply lift_unique; simp
182+
right_inv f := by simp
183+
184+
/-- The profinite completion is left adjoint to the forgetful functor. -/
185+
noncomputable
186+
def adjunction : profiniteCompletion ⊣ forget₂ _ _ :=
187+
Adjunction.mkOfHomEquiv {
188+
homEquiv := homEquiv
189+
homEquiv_naturality_left_symm f g := by
190+
apply lift_unique
191+
simp [homEquiv]
192+
}
193+
194+
end ProfiniteCompletion
195+
196+
end ProfiniteGrp

0 commit comments

Comments
 (0)