Source: ProCGroups.CompletedGroupAlgebra.UniversalProperty.FiniteQuotient

1import ProCGroups.CompletedGroupAlgebra.UniversalProperty.Basic

3/-!

4# Lifts to finite and discrete quotients

6Maps from the algebraic group algebra that factor through a finite stage extend uniquely from the

7completion. This file constructs those lifts, specializes them to discrete modules, and proves

8joint injectivity of the finite-stage projections.

9-/

11open scoped Topology

13namespace CompletedGroupAlgebra

15noncomputable section

17open ProCGroups

18open ProCGroups.ProC

19open ProCGroups.InverseSystems

20open ProCGroups.Completion

22universe u v w

24variable (R : Type u) [CommRing R] [TopologicalSpace R] [IsTopologicalRing R]

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

26 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]

28/--

29Finite-quotient construction used in Lemma 5.3.5(d): a map on one finite quotient \(G/U\)

30extends linearly and continuously from \(\widehat{R[G]}\).

31-/

32def completedGroupAlgebraLiftOfFiniteQuotient

33 (U : CompletedGroupAlgebraIndex G) (N : Type w)

34 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]

35 [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) :

36 CompletedGroupAlgebraCarrier R G →L[R] N := by

37 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

38 (completedGroupAlgebraSystem R G).topologicalSpace U

39 exact (finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f).comp

40 (completedGroupAlgebraProjectionContinuousLinearMap R G U)

42omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

43/-- The finite-quotient lift has the prescribed value on completed group-like elements. -/

44@[simp]

45theorem completedGroupAlgebraLiftOfFiniteQuotient_apply_of

46 (U : CompletedGroupAlgebraIndex G) (N : Type w)

47 [AddCommGroup N] [TopologicalSpace N] [Module R N] [ContinuousAdd N]

48 [ContinuousSMul R N] (f : CompletedGroupAlgebraQuotient G U → N) (g : G) :

49 completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N f

50 (completedGroupAlgebraOf R G g) =

51 f (openNormalSubgroupInClassProj

52 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) := by

53 letI : TopologicalSpace (CompletedGroupAlgebraStage R G U) :=

54 (completedGroupAlgebraSystem R G).topologicalSpace U

55 change finiteGroupAlgebraLift R (CompletedGroupAlgebraQuotient G U) N f

56 (completedGroupAlgebraProjection R G U (completedGroupAlgebraOf R G g)) =

57 f (openNormalSubgroupInClassProj

58 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)

59 rw [completedGroupAlgebraProjection_of]

60 exact finiteGroupAlgebraLift_apply_of R (CompletedGroupAlgebraQuotient G U) N f

61 (openNormalSubgroupInClassProj

62 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g)

64omit [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G] in

65/--

66If a continuous target map already factors through one finite quotient \(G/U\), the

67finite-quotient construction gives the required unique continuous linear extension.

68-/

69theorem completedGroupAlgebra_existsUnique_lift_of_factors

70 (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]

71 [ContinuousAdd N] [ContinuousSMul R N] [T2Space N]

72 (U : CompletedGroupAlgebraIndex G) (f : G → N)

73 (fbar : CompletedGroupAlgebraQuotient G U → N)

74 (hfac : ∀ g : G,

75 fbar (openNormalSubgroupInClassProj

76 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g) :

77 ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,

78 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by

79 let F := completedGroupAlgebraLiftOfFiniteQuotient (R := R) (G := G) U N fbar

80 refine ⟨F, ?_, ?_⟩

81 · intro g

82 rw [completedGroupAlgebraLiftOfFiniteQuotient_apply_of, hfac]

83 · intro K hK

84 apply completedGroupAlgebraContinuousLinearMap_ext_of_basis (R := R) (G := G)

85 intro g

86 rw [completedGroupAlgebraLiftOfFiniteQuotient_apply_of, hfac, hK]

88omit [T2Space G] in

89/--

90A continuous map from a profinite group to a discrete space is unchanged on the cosets of some

91finite open normal quotient, providing the topological factorization input for Lemma 5.3.5(d).

92-/

93theorem exists_completedGroupAlgebraIndex_factor_continuous_discrete

94 (N : Type w) [TopologicalSpace N] [DiscreteTopology N]

95 (f : G → N) (hf : Continuous f) :

96 ∃ U : CompletedGroupAlgebraIndex G, ∃ fbar : CompletedGroupAlgebraQuotient G U → N,

97 ∀ g : G,

98 fbar (openNormalSubgroupInClassProj

99 (C := ProCGroups.FiniteGroupClass.allFinite) (G := G) U g) = f g := by

100 let T : Set (G × G) := {p | f p.1 = f p.2}

101 have hTopen : IsOpen T := by

102 have hpair : Continuous fun p : G × G => (f p.1, f p.2) :=

103 (hf.comp continuous_fst).prodMk (hf.comp continuous_snd)

104 change IsOpen ((fun p : G × G => (f p.1, f p.2)) ⁻¹'

105 {q : N × N | q.1 = q.2})

106 exact hpair.isOpen_preimage _ (isOpen_discrete _)

107 let A : Set (G × G) := {p | f p.1 = f (p.1 * p.2)}

108 have hAopen : IsOpen A := by

109 have hmul : Continuous fun p : G × G => (p.1, p.1 * p.2) :=

110 continuous_fst.prodMk (continuous_fst.mul continuous_snd)

111 change IsOpen ((fun p : G × G => (p.1, p.1 * p.2)) ⁻¹' T)

112 exact hTopen.preimage hmul

113 have hcontains : (Set.univ : Set G) ×ˢ ({1} : Set G) ⊆ A := by

114 rintro ⟨g, u⟩ ⟨_hg, hu⟩

115 change u = 1 at hu

116 change f g = f (g * u)

117 rw [hu, mul_one]

118 rcases generalized_tube_lemma (s := (Set.univ : Set G)) isCompact_univ

119 (t := ({1} : Set G)) isCompact_singleton hAopen hcontains with

120 ⟨W, V, _hWopen, hVopen, hWuniv, h1V, hWV⟩

121 have hVone : (1 : G) ∈ V := h1V (by simp only [Set.mem_singleton_iff])

122 rcases ProCGroups.ProC.exists_openNormalSubgroup_sub_open_nhds_of_one

123 (G := G) hVopen hVone with

124 ⟨U0, hU0V⟩

125 let U : CompletedGroupAlgebraIndex G := OrderDual.toDual

126 ⟨U0, ProCGroups.openNormalSubgroup_finiteQuotient (G := G) U0⟩

127 let fbar : CompletedGroupAlgebraQuotient G U → N := Quotient.lift f (by

128 intro a b hab

129 have habU : a⁻¹ * b ∈ (U0.1 : Subgroup G) :=

130 (QuotientGroup.leftRel_apply).1 hab

131 have habV : a⁻¹ * b ∈ V := hU0V habU

132 have hA : (a, a⁻¹ * b) ∈ A :=

133 hWV ⟨hWuniv (Set.mem_univ a), habV⟩

134 simpa [A, mul_assoc] using hA)

135 refine ⟨U, fbar, ?_⟩

136 intro g

137 rfl

138

139omit [T2Space G] in

140/--

141Discrete-target form of Lemma 5.3.5(d): a continuous map from the profinite group \(G\) to a

142discrete \(R\)-module extends uniquely to a continuous \(R\)-linear map out of

143\(\widehat{R[G]}\).

144-/

145theorem completedGroupAlgebra_existsUnique_lift_to_discreteModule

146 (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]

147 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]

148 (f : G → N) (hf : Continuous f) :

149 ∃! F : CompletedGroupAlgebraCarrier R G →L[R] N,

150 ∀ g : G, F (completedGroupAlgebraOf R G g) = f g := by

151 letI : T2Space N := inferInstance

152 rcases exists_completedGroupAlgebraIndex_factor_continuous_discrete

153 (G := G) N f hf with

154 ⟨U, fbar, hfac⟩

155 exact completedGroupAlgebra_existsUnique_lift_of_factors (R := R) (G := G) N

156 U f fbar hfac

157

158/-- The discrete-target extension used in Lemma 5.3.5(d). -/

159def completedGroupAlgebraLiftToDiscreteModule

160 (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]

161 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]

162 (f : G → N) (hf : Continuous f) :

163 CompletedGroupAlgebraCarrier R G →L[R] N :=

164 Classical.choose

165 (completedGroupAlgebra_existsUnique_lift_to_discreteModule

166 (R := R) (G := G) N f hf)

167

168omit [T2Space G] in

169/-- The chosen discrete-target lift has the prescribed value on completed group-like elements. -/

170@[simp]

171theorem completedGroupAlgebraLiftToDiscreteModule_apply_of

172 (N : Type w) [AddCommGroup N] [TopologicalSpace N] [Module R N]

173 [ContinuousAdd N] [ContinuousSMul R N] [DiscreteTopology N]

174 (f : G → N) (hf : Continuous f) (g : G) :

175 completedGroupAlgebraLiftToDiscreteModule

176 (R := R) (G := G) N f hf

177 (completedGroupAlgebraOf R G g) = f g := by

178 exact (Classical.choose_spec

179 (completedGroupAlgebra_existsUnique_lift_to_discreteModule

180 (R := R) (G := G) N f hf)).1 g

181

182namespace CompletedGroupAlgebraModel

183

184variable {R : ProfiniteCommRing.{u}} {G : ProfiniteGrp.{v}}

185

186/-- Elements of a bundled completed-group-algebra model are determined by all of their finite-stage

187projections. This is the public finite-quotient extensionality principle for arbitrary models, not

188only for the concrete compatible-family carrier. -/

189theorem ext_of_stageProjection_eq (M : CompletedGroupAlgebraModel R G)

190 {x y : M.carrier}

191 (h : ∀ U : CompletedGroupAlgebraIndex G,

192 M.stageProjection U x = M.stageProjection U y) :

193 x = y := by

194 apply M.comparisonRingEquiv.injective

195 apply completedGroupAlgebra_ext (R := R) (G := G)

196 intro U

197 simpa using h U

198

199/-- The family of finite-stage projections of any bundled model is jointly injective. -/

200theorem stageProjection_jointly_injective (M : CompletedGroupAlgebraModel R G) :

201 Function.Injective (fun x : M.carrier => fun U => M.stageProjection U x) := by

202 intro x y hxy

203 apply M.ext_of_stageProjection_eq

204 intro U

205 exact congrFun hxy U

206

207end CompletedGroupAlgebraModel

208

209end

210

211end CompletedGroupAlgebra