Source: ProCGroups.CompletedGroupAlgebra.Basic.AllFinite.Index

1import ProCGroups.CompletedGroupAlgebra.Basic.InClass.Index

3/-!

4# Completed Group Algebra / Basic / All Finite / Index

6This module defines the reverse-ordered finite-quotient indices for the all-finite completion,

7their quotient groups and quotient projections, and the mutually inverse conversions with

8\(C\)-indexed quotients when a formation contains all finite quotients of the group.

9-/

11open scoped Topology

13namespace CompletedGroupAlgebra

15noncomputable section

17open ProCGroups

18open ProCGroups.ProC

19open ProCGroups.InverseSystems

21universe u v w

24variable (G : Type v) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

26/--

27The index set for the Section 5.3 completed group algebra tower, ordered so that larger indices

28give finer finite quotients.

29-/

30abbrev CompletedGroupAlgebraIndex :=

31 OrderDual (OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G)

33/-- The finite quotient \(G/U\) attached to one index of the completed-group-algebra tower. -/

34abbrev CompletedGroupAlgebraQuotient (U : CompletedGroupAlgebraIndex G) : Type v :=

35 (openNormalSubgroupInClassSystem ProCGroups.FiniteGroupClass.allFinite G).X U

37/-- The finite completed group-algebra quotient is finite. -/

38instance instFiniteCompletedGroupAlgebraQuotient

39 (U : CompletedGroupAlgebraIndex G) :

40 Finite (CompletedGroupAlgebraQuotient G U) :=

41 (OrderDual.ofDual U).2

43/-- The whole group \(G\), as a subgroup, used for the terminal quotient \(G/G\). -/

44def terminalCompletedGroupAlgebraSubgroup : Subgroup G where

45 carrier := Set.univ

46 one_mem' := by simp only [Set.mem_univ]

47 mul_mem' := by intro a b ha hb; simp only [Set.mem_univ]

48 inv_mem' := by intro a ha; simp only [Set.mem_univ]

50/-- The whole group \(G\) is an open subgroup. -/

51def terminalCompletedGroupAlgebraOpenSubgroup : OpenSubgroup G :=

52 OpenSubgroup.mk (terminalCompletedGroupAlgebraSubgroup G) isOpen_univ

54/-- The whole group \(G\) is an open normal subgroup. -/

55def terminalCompletedGroupAlgebraOpenNormalSubgroup : OpenNormalSubgroup G :=

56 OpenNormalSubgroup.mk (terminalCompletedGroupAlgebraOpenSubgroup G)

57 (Subgroup.Normal.mk (by

58 intro n hn g

59 simp only [terminalCompletedGroupAlgebraOpenSubgroup,

60 terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk,

61 Submonoid.mem_mk, Subsemigroup.mem_mk, Set.mem_univ]))

63omit [IsTopologicalGroup G] in

64/--

65The terminal all-finite open normal subgroup has underlying subgroup equal to the top subgroup.

66-/

67@[simp]

68theorem terminalCompletedGroupAlgebraOpenNormalSubgroup_coe :

69 ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G) =

70 ⊤ := by

71 ext g

72 simp only [terminalCompletedGroupAlgebraOpenNormalSubgroup,

73 terminalCompletedGroupAlgebraOpenSubgroup,

74 terminalCompletedGroupAlgebraSubgroup, Subgroup.mem_mk, Submonoid.mem_mk, Subsemigroup.mem_mk,

75 Set.mem_univ,

76 Subgroup.mem_top]

78/--

79The terminal completed group-algebra quotient is a subsingleton, since it is the quotient by the

80whole group.

81-/

82instance terminalCompletedGroupAlgebraQuotient_subsingleton :

83 Subsingleton

84 (G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :

85 Subgroup G)) := by

86 rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]

87 constructor

88 intro x y

89 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) x with ⟨a, rfl⟩

90 rcases QuotientGroup.mk'_surjective (⊤ : Subgroup G) y with ⟨b, rfl⟩

91 exact (QuotientGroup.eq).2 (by simp only [Subgroup.mem_top])

93/-- The terminal open normal subgroup belongs to the finite-quotient indexing family. -/

94def terminalCompletedGroupAlgebraSubgroupInClass :

95 OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G := by

96 refine ⟨terminalCompletedGroupAlgebraOpenNormalSubgroup G, ?_⟩

97 letI : Subsingleton

98 (G ⧸ ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) :

99 Subgroup G)) :=

100 terminalCompletedGroupAlgebraQuotient_subsingleton (G := G)

101 exact Finite.of_subsingleton

102

103/-- The terminal all-finite index, corresponding to the quotient \(G/G\). -/

104def terminalCompletedGroupAlgebraIndex : CompletedGroupAlgebraIndex G :=

105 OrderDual.toDual (terminalCompletedGroupAlgebraSubgroupInClass G)

106

107/--

108The completed group algebra is nonempty, with the terminal quotient or canonical base object as

109witness.

110-/

111instance instNonemptyCompletedGroupAlgebraIndex :

112 Nonempty (CompletedGroupAlgebraIndex G) :=

113 ⟨terminalCompletedGroupAlgebraIndex G⟩

114

115omit [IsTopologicalGroup G] in

116/-- The terminal all-finite index is below every all-finite completed-group-algebra index. -/

117theorem terminalCompletedGroupAlgebraIndex_le (U : CompletedGroupAlgebraIndex G) :

118 terminalCompletedGroupAlgebraIndex G ≤ U := by

119 change ((OrderDual.ofDual U).1 : Subgroup G) ≤

120 ((terminalCompletedGroupAlgebraOpenNormalSubgroup G : OpenNormalSubgroup G) : Subgroup G)

121 rw [terminalCompletedGroupAlgebraOpenNormalSubgroup_coe (G := G)]

122 intro g hg

123 simp only [Subgroup.mem_top]

124

125/-- A quotient indexed by a finite quotient class is also an all-finite quotient. -/

126def completedGroupAlgebraIndexInClassToAllFinite

127 (C : ProCGroups.FiniteGroupClass.{v})

128 (U : CompletedGroupAlgebraIndexInClass G C) : CompletedGroupAlgebraIndex G :=

129 OrderDual.toDual

130 ⟨(OrderDual.ofDual U).1, C.finite (OrderDual.ofDual U).property⟩

131

132omit [IsTopologicalGroup G] in

133/-- The comparison of all-finite and class-indexed indices is monotone. -/

134theorem completedGroupAlgebraIndexInClassToAllFinite_le

135 (C : ProCGroups.FiniteGroupClass.{v})

136 {U V : CompletedGroupAlgebraIndexInClass G C} (hUV : U ≤ V) :

137 completedGroupAlgebraIndexInClassToAllFinite G C U ≤

138 completedGroupAlgebraIndexInClassToAllFinite G C V := by

139 change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)

140 exact hUV

141

142/--

143For a pro-\(C\) group over a formation, every all-finite open-normal quotient is a

144\(C\)-quotient.

145-/

146def completedGroupAlgebraIndexToInClass

147 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)

148 (hG : HasOpenNormalBasisInClass C G)

149 (U : CompletedGroupAlgebraIndex G) : CompletedGroupAlgebraIndexInClass G C :=

150 OrderDual.toDual ⟨(OrderDual.ofDual U).1,

151 HasOpenNormalBasisInClass.quotient_mem (C := C) hForm hG

152 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩

153

154omit [IsTopologicalGroup G] in

155/-- The comparison of all-finite and class-indexed indices is monotone. -/

156theorem completedGroupAlgebraIndexToInClass_le

157 (C : ProCGroups.FiniteGroupClass.{v}) (hForm : ProCGroups.FiniteGroupClass.Formation C)

158 (hG : HasOpenNormalBasisInClass C G)

159 {U V : CompletedGroupAlgebraIndex G} (hUV : U ≤ V) :

160 completedGroupAlgebraIndexToInClass G C hForm hG U ≤

161 completedGroupAlgebraIndexToInClass G C hForm hG V := by

162 change ((OrderDual.ofDual V).1 : Subgroup G) ≤ ((OrderDual.ofDual U).1 : Subgroup G)

163 exact hUV

164

165omit [IsTopologicalGroup G] in

166/--

167For a pro-\(C\) group, converting an all-finite completed-group-algebra index to the

168\(C\)-indexed tower and then back to the all-finite tower returns the original index.

169-/

170@[simp]

171theorem completedGroupAlgebraIndexInClassToAllFinite_indexToInClass

172 (C : ProCGroups.FiniteGroupClass.{v})

173 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)

174 (U : CompletedGroupAlgebraIndex G) :

175 completedGroupAlgebraIndexInClassToAllFinite G C

176 (completedGroupAlgebraIndexToInClass G C hForm hG U) = U := by

177 change (⟨(OrderDual.ofDual U).1,

178 C.finite (HasOpenNormalBasisInClass.quotient_mem (C := C) hForm hG

179 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G))⟩ :

180 OpenNormalSubgroupInClass ProCGroups.FiniteGroupClass.allFinite G) = OrderDual.ofDual U

181 exact Subtype.ext rfl

182

183omit [IsTopologicalGroup G] in

184/--

185For a pro-\(C\) group, converting a \(C\)-indexed completed-group-algebra index to the

186all-finite tower and then back to the \(C\)-indexed tower returns the original index.

187-/

188@[simp]

189theorem completedGroupAlgebraIndexToInClass_indexInClassToAllFinite

190 (C : ProCGroups.FiniteGroupClass.{v})

191 (hForm : ProCGroups.FiniteGroupClass.Formation C) (hG : HasOpenNormalBasisInClass C G)

192 (U : CompletedGroupAlgebraIndexInClass G C) :

193 completedGroupAlgebraIndexToInClass G C hForm hG

194 (completedGroupAlgebraIndexInClassToAllFinite G C U) = U := by

195 change (⟨(OrderDual.ofDual U).1,

196 HasOpenNormalBasisInClass.quotient_mem (C := C) hForm hG

197 ((OrderDual.ofDual U).1 : OpenNormalSubgroup G)⟩ :

198 OpenNormalSubgroupInClass C G) = OrderDual.ofDual U

199 exact Subtype.ext rfl

200

201end

202

203end CompletedGroupAlgebra