FenchelNielsenZomorrodian/Profinite/CharacteristicClosure.lean
1import FenchelNielsenZomorrodian.Profinite.FGroup
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Profinite/CharacteristicClosure.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Characteristic closure of open normal subgroups
14Turns torsion-free open normal subgroups, and bounded-derived-length quotient data, into characteristic open subgroups using the finite number of open subgroups of fixed index.
15-/
17namespace FenchelNielsen
19universe u
21open scoped Topology
22open ProCGroups.FiniteGeneration
23open ProCGroups.FiniteStepSolvableQuotients
25variable {G : Type u} [Group G] [TopologicalSpace G]
27/-- Pull an open normal subgroup back along a continuous automorphism. -/
28noncomputable def openNormalAutComap (φ : G ≃ₜ* G)
29 (U : OpenNormalSubgroup G) : OpenNormalSubgroup G :=
30 ProCGroups.OpenNormalSubgroup.comap φ.toContinuousMonoidHom.toMonoidHom
31 φ.continuous_toFun U
33@[local simp]
34theorem mem_openNormalAutComap {φ : G ≃ₜ* G}
35 {U : OpenNormalSubgroup G} {x : G} :
36 x ∈ openNormalAutComap φ U ↔ φ x ∈ U :=
37 Iff.rfl
39/-- The automorphic orbit of an open normal subgroup, viewed as ordinary subgroups. -/
40noncomputable def openNormalAutComapOrbitSubgroups
41 (U : OpenNormalSubgroup G) : Set (Subgroup G) :=
42 Set.range fun φ : G ≃ₜ* G =>
43 ((openNormalAutComap φ U : OpenNormalSubgroup G) : Subgroup G)
45variable [IsTopologicalGroup G] [CompactSpace G]
47/-- The automorphic orbit of an open normal subgroup is finite when open subgroups of fixed index
50 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
51 (openNormalAutComapOrbitSubgroups U).Finite := by
52 classical
53 let n := Nat.card (G ⧸ (U : Subgroup G))
55 (G := G) hfin n).subset ?_
56 intro V hV
57 rcases hV with ⟨φ, hφ⟩
58 rw [← hφ]
59 have hopen :
60 IsOpen
61 (((openNormalAutComap φ U : OpenNormalSubgroup G) : Subgroup G) :
62 Set G) :=
63 ProCGroups.openNormalSubgroup_isOpen (G := G) (openNormalAutComap φ U)
64 have hfinite :
65 Finite
66 (G ⧸ ((openNormalAutComap φ U : OpenNormalSubgroup G) :
67 Subgroup G)) :=
68 Subgroup.quotient_finite_of_isOpen _ hopen
69 refine ⟨hopen, hfinite, ?_⟩
70 simpa [openNormalAutComap, Subgroup.index_eq_card, n] using
71 (Subgroup.index_comap_of_surjective
72 (H := (U : Subgroup G)) φ.surjective).le
74/-- The intersection of the automorphic orbit of an open normal subgroup is open. -/
76 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
77 IsOpen ((sInf (openNormalAutComapOrbitSubgroups U) : Subgroup G) :
78 Set G) := by
79 apply ProCGroups.FiniteGeneration.Subgroup.isOpen_sInf_of_finite
80 · exact openNormalAutComapOrbitSubgroups_finite (G := G) hfin U
81 · intro V hV
82 rcases hV with ⟨φ, hφ⟩
83 rw [← hφ]
84 exact ProCGroups.openNormalSubgroup_isOpen (G := G) (openNormalAutComap φ U)
86omit [IsTopologicalGroup G] [CompactSpace G] in
87/-- The intersection of the automorphic orbit of an open normal subgroup is normal. -/
88theorem openNormalAutComapOrbitSubgroups_normal (U : OpenNormalSubgroup G) :
89 (sInf (openNormalAutComapOrbitSubgroups U)).Normal := by
90 rw [sInf_eq_iInf']
91 exact Subgroup.normal_iInf_normal fun V : openNormalAutComapOrbitSubgroups U => by
92 rcases V.2 with ⟨φ, hφ⟩
93 rw [← hφ]
94 exact (openNormalAutComap φ U).isNormal'
96/-- The characteristic closure of an open normal subgroup in a finitely generated profinite group. -/
97noncomputable def openNormalCharacteristicClosure
98 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
99 OpenNormalSubgroup G where
100 toOpenSubgroup :=
101 { toSubgroup := sInf (openNormalAutComapOrbitSubgroups U)
102 isOpen' := openNormalAutComapOrbitSubgroups_open (G := G) hfin U }
103 isNormal' := openNormalAutComapOrbitSubgroups_normal (G := G) U
105/-- The characteristic closure of an open normal subgroup is contained in the original subgroup. -/
107 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
108 (openNormalCharacteristicClosure (G := G) hfin U : Subgroup G) ≤
109 (U : Subgroup G) := by
110 intro x hx
111 have hx' : x ∈ sInf (openNormalAutComapOrbitSubgroups U) := hx
112 rw [Subgroup.mem_sInf] at hx'
113 exact hx' _ ⟨ContinuousMulEquiv.refl G, by ext y; simp only [openNormalAutComap, ContinuousMonoidHom.coe_toMonoidHom,
114 ProCGroups.OpenNormalSubgroup.toSubgroup_comap, Subgroup.mem_comap, MonoidHom.coe_coe,
115 ContinuousMulEquiv.toContinuousMonoidHom_apply, ContinuousMulEquiv.refl_apply, OpenSubgroup.mem_toSubgroup]⟩
117/-- The characteristic closure is topologically characteristic. -/
119 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
121 (openNormalCharacteristicClosure (G := G) hfin U : Subgroup G) := by
122 intro ψ g
123 constructor
124 · intro hg
125 change ψ g ∈ sInf (openNormalAutComapOrbitSubgroups U) at hg
126 change g ∈ sInf (openNormalAutComapOrbitSubgroups U)
127 rw [Subgroup.mem_sInf] at hg ⊢
128 intro V hV
129 rcases hV with ⟨φ, hφ⟩
130 rw [← hφ]
131 have hmem :
132 ψ g ∈ (openNormalAutComap (ψ.symm.trans φ) U :
133 OpenNormalSubgroup G) :=
134 hg _ ⟨ψ.symm.trans φ, rfl⟩
135 simpa [openNormalAutComap] using hmem
136 · intro hg
137 change g ∈ sInf (openNormalAutComapOrbitSubgroups U) at hg
138 change ψ g ∈ sInf (openNormalAutComapOrbitSubgroups U)
139 rw [Subgroup.mem_sInf] at hg ⊢
140 intro V hV
141 rcases hV with ⟨φ, hφ⟩
142 rw [← hφ]
143 have hmem :
144 g ∈ (openNormalAutComap (ψ.trans φ) U : OpenNormalSubgroup G) :=
145 hg _ ⟨ψ.trans φ, rfl⟩
146 simpa [openNormalAutComap] using hmem
148/-- The same closure bundled as a profinite open characteristic subgroup. -/
149noncomputable def profiniteOpenCharacteristicClosure
150 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) :
152 ⟨openNormalCharacteristicClosure (G := G) hfin U,
153 openNormalCharacteristicClosure_characteristic (G := G) hfin U⟩
156 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G)
157 (htf : ProfiniteOpenNormalSubgroupTorsionFree G U) :
159 (profiniteOpenCharacteristicClosure (G := G) hfin U).toOpenNormalSubgroup := by
160 intro x hx hfinord
161 exact htf x (openNormalCharacteristicClosure_le (G := G) hfin U hx) hfinord
164/-- Characteristic-closure existence package: in a finitely generated profinite group, any
165torsion-free open normal subgroup can be replaced by a torsion-free open characteristic subgroup. -/
167 (hfin : HasFiniteOpenSubgroupsOfIndex G)
168 (h : ∃ U : OpenNormalSubgroup G, ProfiniteOpenNormalSubgroupTorsionFree G U) :
169 ∃ U : ProfiniteOpenCharacteristicSubgroup G,
170 ProfiniteOpenNormalSubgroupTorsionFree G U.toOpenNormalSubgroup := by
171 rcases h with ⟨U, htf⟩
172 exact
173 ⟨profiniteOpenCharacteristicClosure (G := G) hfin U,
174 profiniteOpenCharacteristicClosure_torsionFree (G := G) hfin U htf⟩
177 (hfin : HasFiniteOpenSubgroupsOfIndex G) (U : OpenNormalSubgroup G) {m : ℕ}
178 (hquot : ProfiniteOpenNormalQuotientHasDerivedLengthAtMost G U m) :
180 (profiniteOpenCharacteristicClosure (G := G) hfin U) m := by
181 have hDleU : profiniteDerivedSeries G m ≤ (U : Subgroup G) :=
182 ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.topDerived_le U hquot
183 apply ProfiniteOpenNormalQuotientHasDerivedLengthAtMost.of_topDerived_le
184 intro x hx
185 change x ∈ sInf (openNormalAutComapOrbitSubgroups U)
186 rw [Subgroup.mem_sInf]
187 intro V hV
188 rcases hV with ⟨φ, hφ⟩
189 rw [← hφ]
190 change φ x ∈ U
191 exact hDleU ((topDerivedTop_le_comap (f := φ.toContinuousMonoidHom) (m := m)) hx)
195 (hfin : HasFiniteOpenSubgroupsOfIndex G) {m : ℕ}
196 (h :
199 rcases h with ⟨U, htf, hquot⟩
200 refine
201 ⟨profiniteOpenCharacteristicClosure (G := G) hfin U,
202 profiniteOpenCharacteristicClosure_torsionFree (G := G) hfin U htf,
203 profiniteOpenCharacteristicClosure_derivedLength (G := G) hfin U hquot⟩
205end FenchelNielsen