Yamaguchi Lean 4 Library
ProCGroups/Topologies/FullSubgroupTopology/QuotientFormation.lean
ProCGroups/Topologies/FullSubgroupTopology/QuotientFormation/Source

ProCGroups/Topologies/FullSubgroupTopology/QuotientFormation.lean

1import Mathlib.Topology.Algebra.Group.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/ProCGroups/Topologies/FullSubgroupTopology/QuotientFormation.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Topological group constructions
14Topological subgroup, quotient, continuous homomorphism, continuous equivalence, conjugation, and full-subgroup-topology lemmas.
15-/
17open Set
18open scoped Topology
20namespace ProCGroups.Topologies
22universe u
24/--
25A quotient-level encoding of the distinguished open-normal family attached to a pro-`C` topology.
27The intended reading of `C.contains N` is “the quotient `G/N` belongs to the chosen formation”.
28The structure records just the closure properties needed for the basic algebra of the pro-`C`
29topology, without committing to a concrete implementation of quotient classes.
30-/
31structure QuotientFormation where
32 contains : ∀ {G : Type u} [Group G], Subgroup G → Prop
33 top_mem : ∀ {G : Type u} [Group G], contains (G := G) (⊤ : Subgroup G)
34 normal_of_mem : ∀ {G : Type u} [Group G] {N : Subgroup G}, contains (G := G) N → N.Normal
35 upward_closed :
36 ∀ {G : Type u} [Group G] {N K : Subgroup G},
37 contains (G := G) N → N ≤ K → K.Normal → contains (G := G) K
38 inf_closed :
39 ∀ {G : Type u} [Group G] {N K : Subgroup G},
40 contains (G := G) N → contains (G := G) K → contains (G := G) (N ⊓ K)
44variable (C : QuotientFormation)
46/-- A subgroup is open in the pro-`C` topology iff it contains one of the basic kernels. -/
47def IsOpenSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
48 ∃ N : Subgroup G, C.contains N ∧ N ≤ H
50/-- Algebraic closure operator attached to the pro-`C` topology. -/
51def proCClosure {G : Type u} [Group G] (H : Subgroup G) : Subgroup G :=
52 sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}
54/-- Closedness for the pro-`C` topology, formulated algebraically. -/
55def IsClosedSubgroup {G : Type u} [Group G] (H : Subgroup G) : Prop :=
56 C.proCClosure H = H
58/-- Residuality for the pro-`C` topology: the identity is separated by the basic open kernels. -/
59def IsResiduallyC {G : Type u} [Group G] : Prop :=
60 C.proCClosure (⊥ : Subgroup G) = ⊥
62variable {C}
63variable {G : Type u} [Group G]
65/-- The whole group is open for a quotient formation. -/
66@[simp] theorem isOpenSubgroup_top (C : QuotientFormation) :
67 C.IsOpenSubgroup (⊤ : Subgroup G) := by
68 exact ⟨⊤, C.top_mem, le_rfl⟩
70/-- A subgroup above an open subgroup for a quotient formation is open on the left. -/
71theorem isOpenSubgroup_sup_left (C : QuotientFormation) {H K : Subgroup G}
72 (hH : C.IsOpenSubgroup H) :
73 C.IsOpenSubgroup (H ⊔ K) := by
74 rcases hH with ⟨N, hN, hNH⟩
75 exact ⟨N, hN, le_trans hNH le_sup_left⟩
77/-- A subgroup above an open subgroup for a quotient formation is open on the right. -/
78theorem isOpenSubgroup_sup_right (C : QuotientFormation) {H K : Subgroup G}
79 (hK : C.IsOpenSubgroup K) :
80 C.IsOpenSubgroup (H ⊔ K) := by
81 simpa [sup_comm] using
82 (C.isOpenSubgroup_sup_left (H := K) (K := H) hK)
84/-- A subgroup is contained in its pro-`C` closure. -/
85theorem le_proCClosure (C : QuotientFormation) (H : Subgroup G) :
86 H ≤ C.proCClosure H := by
87 change H ≤ sInf {K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}
88 exact le_sInf fun K hK => hK.2
90/-- The pro-`C` closure operation is monotone. -/
91theorem proCClosure_mono (C : QuotientFormation) {H K : Subgroup G}
92 (hHK : H ≤ K) :
93 C.proCClosure H ≤ C.proCClosure K := by
94 change
95 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L} ≤
96 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ K ≤ L}
97 refine le_sInf ?_
98 intro L hL
99 exact sInf_le ⟨hL.1, hHK.trans hL.2⟩
101/-- The pro-`C` closure operation is idempotent. -/
102theorem proCClosure_idem (C : QuotientFormation) (H : Subgroup G) :
103 C.proCClosure (C.proCClosure H) = C.proCClosure H := by
104 refine le_antisymm ?_ (C.proCClosure_mono (C.le_proCClosure H))
105 change
106 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ C.proCClosure H ≤ L} ≤
107 sInf {L : Subgroup G | C.IsOpenSubgroup L ∧ H ≤ L}
108 refine le_sInf ?_
109 intro L hL
110 exact sInf_le ⟨hL.1, sInf_le hL⟩
112/-- Closed subgroups for the quotient formation are exactly those containing the pro-`C` closure of every smaller subgroup. -/
114 C.IsClosedSubgroup H ↔ C.proCClosure H ≤ H := by
115 constructor
116 · intro hH
117 rw [QuotientFormation.IsClosedSubgroup] at hH
118 rw [hH]
119 · intro hH
120 exact le_antisymm hH (C.le_proCClosure H)
122/-- Residual `C`-ness is equivalent to the pro-`C` closure of the bottom subgroup being bottom. -/
124 C.IsResiduallyC (G := G) ↔ C.proCClosure (⊥ : Subgroup G) = ⊥ :=
125 Iff.rfl
127/-- An element outside the pro-`C` closure is separated by an open subgroup in the quotient formation. -/
129 (C : QuotientFormation) {H : Subgroup G} {x : G}
130 (hx : x ∉ C.proCClosure H) :
131 ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ H ≤ K ∧ x ∉ K := by
132 rw [QuotientFormation.proCClosure, Subgroup.mem_sInf] at hx
133 push_neg at hx
134 rcases hx with ⟨K, hK, hxK⟩
135 exact ⟨K, hK.1, hK.2, hxK⟩
137/-- In a residually `C` group, a nontrivial element is excluded by some open subgroup in the quotient formation. -/
139 (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
140 {x : G} (hx : x ≠ 1) :
141 ∃ K : Subgroup G, C.IsOpenSubgroup K ∧ x ∉ K := by
142 have hxbot : x ∉ C.proCClosure (⊥ : Subgroup G) := by
143 rw [hC]
144 simpa using hx
145 rcases C.exists_openSubgroup_not_mem_of_not_mem_proCClosure
146 (H := (⊥ : Subgroup G)) hxbot with ⟨K, hKopen, _hbotK, hxK⟩
147 exact ⟨K, hKopen, hxK⟩
149/-- The normal core of an open subgroup again defines a quotient in the formation. -/
150theorem normalCore_mem_of_open (C : QuotientFormation) {H : Subgroup G}
151 (hH : C.IsOpenSubgroup H) :
152 C.contains H.normalCore := by
153 rcases hH with ⟨N, hN, hNH⟩
154 let _ : N.Normal := C.normal_of_mem hN
155 have hNcore : N ≤ H.normalCore := (Subgroup.normal_le_normalCore).2 hNH
156 exact C.upward_closed hN hNcore inferInstance
158/-- In a residually `C` group, a nontrivial element is excluded by an open normal kernel in the quotient formation. -/
160 (C : QuotientFormation) (hC : C.IsResiduallyC (G := G))
161 {x : G} (hx : x ≠ 1) :
162 ∃ N : Subgroup G, C.contains N ∧ N.Normal ∧ x ∉ N := by
163 rcases C.exists_openSubgroup_not_mem_of_isResiduallyC (G := G) hC hx with
164 ⟨K, hKopen, hxK⟩
165 refine ⟨K.normalCore, C.normalCore_mem_of_open hKopen, ?_, ?_⟩
166 · exact C.normal_of_mem (C.normalCore_mem_of_open hKopen)
167 · intro hxcore
168 exact hxK (Subgroup.normalCore_le K hxcore)
170/-- Closed subgroups are exactly intersections of open subgroups. -/
172 {C : QuotientFormation} {H : Subgroup G} :
173 C.IsClosedSubgroup H ↔
174 ∃ S : Set (Subgroup G), (∀ K ∈ S, C.IsOpenSubgroup K) ∧ H = sInf S := by
175 constructor
176 · intro hH
177 refine ⟨{K : Subgroup G | C.IsOpenSubgroup K ∧ H ≤ K}, ?_, ?_⟩
178 · intro K hK
179 exact hK.1
180 · simpa [QuotientFormation.IsClosedSubgroup, QuotientFormation.proCClosure] using hH.symm
181 · rintro ⟨S, hSopen, hEq⟩
182 rw [QuotientFormation.IsClosedSubgroup]
183 refine le_antisymm ?_ (C.le_proCClosure H)
184 calc
185 C.proCClosure H ≤ sInf S := by
186 refine le_sInf ?_
187 intro K hK
188 have hHK : H ≤ K := by
189 rw [hEq]
190 exact sInf_le hK
191 exact sInf_le ⟨hSopen K hK, hHK⟩
192 _ = H := hEq.symm
196end ProCGroups.Topologies