CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/Topology.lean

1import CompletedGroupAlgebra.OpenFiniteQuotientTopology.OpenFiniteLimit.Algebra

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/CompletedGroupAlgebra/OpenFiniteQuotientTopology/OpenFiniteLimit/Topology.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Topology on the open finite quotient limit

13-/

15open scoped Topology

17namespace CompletedGroupAlgebra

19noncomputable section

21open ProCGroups

22open ProCGroups.ProC

23open ProCGroups.InverseSystems

24open ProCGroups.Completion

26universe u v

28variable (R : Type u) [CommRing R] [TopologicalSpace R]

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

31/-- Each two-parameter finite quotient stage is a topological ring for its discrete topology. -/

32theorem completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing

33 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]

34 [TopologicalSpace G] [IsTopologicalGroup G]

35 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :

36 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

37 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K

38 IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by

39 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

40 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K

41 haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

42 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K

43 infer_instance

45/-- Under profiniteness of `R`, each two-parameter quotient stage is a finite discrete profinite

46ring. -/

47theorem completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing

48 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]

49 [TopologicalSpace G] [IsTopologicalGroup G] (hR : IsProfiniteRing R)

50 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :

51 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

52 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K

53 IsProfiniteRing (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) := by

54 classical

55 letI : TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

56 completedGroupAlgebraOpenFiniteQuotientStageTopology R G K

57 haveI : DiscreteTopology (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

58 completedGroupAlgebraOpenFiniteQuotientStage_discrete R G K

59 let I : Ideal R := (OrderDual.ofDual K.1).1

60 have hIopen : IsOpen (I : Set R) := (OrderDual.ofDual K.1).2

61 rcases finite_quotient_of_openIdeal R hR I hIopen with ⟨hIfin⟩

62 letI : Fintype (R ⧸ I) := hIfin

63 letI : Fintype (CompletedGroupAlgebraQuotient G K.2) :=

64 Fintype.ofFinite (CompletedGroupAlgebraQuotient G K.2)

65 letI : Fintype (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

66 Fintype.ofEquiv (CompletedGroupAlgebraQuotient G K.2 → R ⧸ I)

67 Finsupp.equivFunOnFinite.symm

68 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩

70/-- Each open finite quotient stage is finite when the coefficient ring is profinite. -/

71theorem completedGroupAlgebraOpenFiniteQuotientStage_fintype

72 (R : Type u) (G : Type v) [CommRing R] [TopologicalSpace R] [Group G]

73 [TopologicalSpace G] [IsTopologicalGroup G] (hR : IsProfiniteRing R)

74 (K : CompletedGroupAlgebraOpenQuotientIndex R G) :

75 Nonempty (Fintype (CompletedGroupAlgebraOpenFiniteQuotientStage R G K)) := by

76 classical

77 let I : Ideal R := (OrderDual.ofDual K.1).1

78 have hIopen : IsOpen (I : Set R) := (OrderDual.ofDual K.1).2

79 rcases finite_quotient_of_openIdeal R hR I hIopen with ⟨hIfin⟩

80 letI : Fintype (R ⧸ I) := hIfin

81 letI : Fintype (CompletedGroupAlgebraQuotient G K.2) :=

82 Fintype.ofFinite (CompletedGroupAlgebraQuotient G K.2)

83 exact ⟨Fintype.ofEquiv

84 (CompletedGroupAlgebraQuotient G K.2 → R ⧸ I)

85 Finsupp.equivFunOnFinite.symm⟩

87instance instContinuousAddCompletedGroupAlgebraOpenFiniteQuotientLimit :

88 ContinuousAdd (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where

89 continuous_add := by

90 let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G

91 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

92 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

93 fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K

94 have hval : Continuous fun p : A × A =>

95 ((p.1 + p.2 : A) :

96 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →

97 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by

98 change Continuous fun p : A × A =>

99 fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>

100 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.1 +

101 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.2

102 apply continuous_pi

103 intro K

104 letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=

105 completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K

106 exact (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp

107 continuous_fst).add

108 (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp

109 continuous_snd)

110 exact Continuous.subtype_mk hval fun p => (p.1 + p.2).2

111

112instance instContinuousNegCompletedGroupAlgebraOpenFiniteQuotientLimit :

113 ContinuousNeg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where

114 continuous_neg := by

115 let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G

116 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

117 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

118 fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K

119 have hval : Continuous fun x : A =>

120 ((-x : A) :

121 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →

122 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by

123 change Continuous fun x : A =>

124 fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>

125 -completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K x

126 apply continuous_pi

127 intro K

128 letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=

129 completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K

130 exact ((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).neg

131 exact Continuous.subtype_mk hval fun x => (-x).2

132

133instance instContinuousMulCompletedGroupAlgebraOpenFiniteQuotientLimit :

134 ContinuousMul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) where

135 continuous_mul := by

136 let A := CompletedGroupAlgebraOpenFiniteQuotientLimit R G

137 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

138 TopologicalSpace (CompletedGroupAlgebraOpenFiniteQuotientStage R G K) :=

139 fun K => (completedGroupAlgebraOpenFiniteQuotientSystem R G).topologicalSpace K

140 have hval : Continuous fun p : A × A =>

141 ((p.1 * p.2 : A) :

142 (K : CompletedGroupAlgebraOpenQuotientIndex R G) →

143 (completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := by

144 change Continuous fun p : A × A =>

145 fun K : CompletedGroupAlgebraOpenQuotientIndex R G =>

146 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.1 *

147 completedGroupAlgebraOpenFiniteQuotientLimitProjection R G K p.2

148 apply continuous_pi

149 intro K

150 letI : IsTopologicalRing ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) :=

151 completedGroupAlgebraOpenFiniteQuotientStage_isTopologicalRing (R := R) (G := G) K

152 exact (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp

153 continuous_fst).mul

154 (((completedGroupAlgebraOpenFiniteQuotientSystem R G).continuous_projection K).comp

155 continuous_snd)

156 exact Continuous.subtype_mk hval fun p => (p.1 * p.2).2

157

158instance instIsTopologicalRingCompletedGroupAlgebraOpenFiniteQuotientLimit :

159 IsTopologicalRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by

160 letI : ContinuousAdd (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

161 instContinuousAddCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)

162 letI : ContinuousMul (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

163 instContinuousMulCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)

164 letI : ContinuousNeg (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

165 instContinuousNegCompletedGroupAlgebraOpenFiniteQuotientLimit (R := R) (G := G)

166 letI : IsTopologicalSemiring (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

167 IsTopologicalSemiring.mk

168 exact IsTopologicalRing.mk

169

170/-- The open finite quotient limit is compact when the coefficient ring is profinite. -/

171theorem completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace

172 (hR : IsProfiniteRing R) :

173 CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by

174 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

175 CompactSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>

176 (completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.1

177 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

178 T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>

179 (completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.1

180 infer_instance

181

182/-- The open finite quotient limit is Hausdorff when the coefficient ring is profinite. -/

183theorem completedGroupAlgebraOpenFiniteQuotientLimit_t2Space

184 (hR : IsProfiniteRing R) :

185 T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by

186 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

187 T2Space ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>

188 (completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.1

189 exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).t2Space_inverseLimit

190

191/-- The open finite quotient limit is totally disconnected when the coefficient ring is profinite. -/

192theorem completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace

193 (hR : IsProfiniteRing R) :

194 TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by

195 letI : ∀ K : CompletedGroupAlgebraOpenQuotientIndex R G,

196 TotallyDisconnectedSpace ((completedGroupAlgebraOpenFiniteQuotientSystem R G).X K) := fun K =>

197 (completedGroupAlgebraOpenFiniteQuotientStage_isProfiniteRing (R := R) (G := G) hR K).2.2.2

198 exact (completedGroupAlgebraOpenFiniteQuotientSystem R G).totallyDisconnectedSpace_inverseLimit

199

200/-- The two-parameter kernel-neighborhood limit is a profinite ring. -/

201theorem completedGroupAlgebraOpenFiniteQuotientLimit_isProfiniteRing

202 (hR : IsProfiniteRing R) :

203 IsProfiniteRing (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) := by

204 letI : CompactSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

205 completedGroupAlgebraOpenFiniteQuotientLimit_compactSpace (R := R) (G := G) hR

206 letI : T2Space (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

207 completedGroupAlgebraOpenFiniteQuotientLimit_t2Space (R := R) (G := G) hR

208 letI : TotallyDisconnectedSpace (CompletedGroupAlgebraOpenFiniteQuotientLimit R G) :=

209 completedGroupAlgebraOpenFiniteQuotientLimit_totallyDisconnectedSpace (R := R) (G := G) hR

210 exact ⟨inferInstance, inferInstance, inferInstance, inferInstance⟩

211

212end

213

214end CompletedGroupAlgebra