CompletedGroupAlgebra/Basic/AllFinite/Index.lean
1import CompletedGroupAlgebra.Basic.InClass.Topology
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/CompletedGroupAlgebra/Basic/AllFinite/Index.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14This module defines the all-finite index category of open normal finite quotients and relates it to class-indexed completed group algebras.
15-/
17open scoped Topology
19namespace CompletedGroupAlgebra
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
25open ProCGroups.InverseSystems
27universe u v w
30variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
32/-- The index set for the book §5.3 completed group algebra tower, ordered so that
34abbrev CompletedGroupAlgebraIndex :=
35 OrderDual (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G)
37/-- The finite quotient `G/U` attached to one index of the completed-group-algebra
38tower. -/
39abbrev CompletedGroupAlgebraQuotient (U : CompletedGroupAlgebraIndex G) : Type v :=
43 (U : CompletedGroupAlgebraIndex G) :
44 Finite (CompletedGroupAlgebraQuotient G U) :=
45 (OrderDual.ofDual U).2
47/-- The whole group `G`, as a subgroup, used for the terminal quotient `G/G`. -/
48def terminalCompletedGroupAlgebraSubgroup : Subgroup G where
49 carrier := Set.univ
50 one_mem' := by simp only [Set.mem_univ]
51 mul_mem' := by intro a b ha hb; simp only [Set.mem_univ]
52 inv_mem' := by intro a ha; simp only [Set.mem_univ]
54/-- The whole group `G`, as an open subgroup. -/
55def terminalCompletedGroupAlgebraOpenSubgroup : OpenSubgroup G :=
56 OpenSubgroup.mk (terminalCompletedGroupAlgebraSubgroup G) isOpen_univ
58/-- The whole group `G`, as an open normal subgroup. -/
59def terminalCompletedGroupAlgebraOpenNormalSubgroup : OpenNormalSubgroup G :=
60 OpenNormalSubgroup.mk (terminalCompletedGroupAlgebraOpenSubgroup G)
61 (Subgroup.Normal.mk (by
62 intro n hn g
63 simp only [terminalCompletedGroupAlgebraOpenSubgroup, terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk,
64 Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_univ]))
66omit [IsTopologicalGroup G] in
67/-- The terminal all-finite open normal subgroup has underlying subgroup equal to the top subgroup. -/
68@[simp]
70 ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G) =
71 ⊤ := by
72 ext g
73 simp only [terminalCompletedGroupAlgebraOpenNormalSubgroup, terminalCompletedGroupAlgebraOpenSubgroup,
74 terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_univ,
75 Subgroup.mem_top]
78 Subsingleton
79 (G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
80 Subgroup G)) := by
81 rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]
82 constructor
83 intro x y
84 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩
85 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩
86 exact (QuotientGroup.eq).2 (by simp only [Subgroup.mem_top])
88/-- The terminal open normal subgroup belongs to the finite-quotient indexing family. -/
91 refine ⟨terminalCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩
92 letI : Subsingleton
93 (G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :
94 Subgroup G)) :=
96 exact Finite.of_subsingleton
98/-- The terminal all-finite index, corresponding to the quotient `G/G`. -/
100 OrderDual.toDual (terminalCompletedGroupAlgebraSubgroupInClass G)
102instance instNonemptyCompletedGroupAlgebraIndex :
103 Nonempty (CompletedGroupAlgebraIndex G) :=
106omit [IsTopologicalGroup G] in
107/-- The terminal all-finite index is below every all-finite completed-group-algebra index. -/
108theorem terminalCompletedGroupAlgebraIndex_le (U : CompletedGroupAlgebraIndex G) :
109 terminalCompletedGroupAlgebraIndex G ≤ U := by
110 change ((OrderDual.ofDual U).1 : Subgroup G) ≤
111 ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G)
112 rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]
113 intro g hg
114 simp only [Subgroup.mem_top]
116/-- A finite-only class-indexed quotient is also an all-finite quotient. -/
118 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
119 (U : CompletedGroupAlgebraIndexInClass G C) : CompletedGroupAlgebraIndex G :=
120 OrderDual.toDual ⟨(OrderDual.ofDual U).1, hC (OrderDual.ofDual U).2⟩
122omit [IsTopologicalGroup G] in
123/-- The comparison of all-finite and class-indexed indices is monotone. -/
125 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
126 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :
127 completedGroupAlgebraIndexInClassToAllFinite G C hC U ≤
128 completedGroupAlgebraIndexInClassToAllFinite G C hC V := by
129 change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)
130 exact hUV
132/-- For a pro-`C` group over a formation, every all-finite open-normal quotient is a `C`-quotient. -/
134 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
135 (hG : IsProCGroup C G)
136 (U : CompletedGroupAlgebraIndex G) : CompletedGroupAlgebraIndexInClass G C :=
137 OrderDual.toDual ⟨(OrderDual.ofDual U).1,
138 IsProCGroup.quotient_mem (C := C) hForm hG
139 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩
141/-- The comparison of all-finite and class-indexed indices is monotone. -/
143 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)
144 (hG : IsProCGroup C G)
145 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :
146 completedGroupAlgebraIndexToInClass G C hForm hG U ≤
147 completedGroupAlgebraIndexToInClass G C hForm hG V := by
148 change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)
149 exact hUV
151/-- Basic all-finite completed group algebra lemma completedGroupAlgebraIndexInClassToAllFinite_indexToInClass. -/
152@[simp]
154 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
155 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
156 (U : CompletedGroupAlgebraIndex G) :
158 (completedGroupAlgebraIndexToInClass G C hForm hG U) = U := by
159 change (⟨(OrderDual.ofDual U).1,
160 hC (IsProCGroup.quotient_mem (C := C) hForm hG
161 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))⟩ :
162 OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) = OrderDual.ofDual U
163 exact Subtype.ext rfl
165/-- Basic all-finite completed group algebra lemma completedGroupAlgebraIndexToInClass_indexInClassToAllFinite. -/
166@[simp]
168 (C : ProCGroups.FiniteGroupClass.{v}) (hC : ProCGroups.FiniteGroupClass.FiniteOnly C)
169 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : IsProCGroup C G)
170 (U : CompletedGroupAlgebraIndexInClass G C) :
171 completedGroupAlgebraIndexToInClass G C hForm hG
172 (completedGroupAlgebraIndexInClassToAllFinite G C hC U) = U := by
173 change (⟨(OrderDual.ofDual U).1,
174 IsProCGroup.quotient_mem (C := C) hForm hG
175 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩ :
176 OpenNormalSubgroupInClass C G) = OrderDual.ofDual U
177 exact Subtype.ext rfl
179end