FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Basic/Augmentation.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.AugmentationIdeal

2import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Basic.StageCoeffMap.AllFinite

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Basic/Augmentation.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Completed coefficient algebras

15Coefficient algebras, residue stages, and completed group-algebra maps are kept as the scalar layer for completed Fox calculus.

16-/

17namespace FoxDifferential

19noncomputable section

21open ProCGroups.InverseSystems

22open ProCGroups.ProC

24universe u

27variable {n m k : ℕ}

28variable [Fact (0 < n)] [Fact (0 < m)] [Fact (0 < k)]

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

31/-- The modulus-direction map on residue-coefficient completed group algebras. -/

32def modNCompletedGroupAlgebraCoeffMap (hnm : n ∣ m) :

33 ModNCompletedGroupAlgebra m G → ModNCompletedGroupAlgebra n G := by

34 intro x

35 refine ⟨fun U =>

36 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U), ?_⟩

37 intro U V hUV

38 calc

39 modNCompletedGroupAlgebraTransition n G hUV

40 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) V hnm (x.1 V))

41 =

42 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm

43 (modNCompletedGroupAlgebraTransition m G hUV (x.1 V)) := by

44 symm

45 exact congrFun

46 (congrArg DFunLike.coe

47 (modNCompletedGroupAlgebraStageCoeffMap_compatible

48 (n := n) (m := m) (G := G) hUV hnm)) (x.1 V)

49 _ =

50 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm (x.1 U) := by

51 exact congrArg

52 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)

53 (x.2 U V hUV)

55omit [Fact (0 < n)] [Fact (0 < m)] in

56/-- 法 n 係数で定めた有限段階射影が関手的写像が有限段階射影と両立することを述べる。 -/

57@[simp]

58theorem modNCompletedGroupAlgebraProjection_coeffMap

59 (hnm : n ∣ m) (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)

60 (x : ModNCompletedGroupAlgebra m G) :

61 modNCompletedGroupAlgebraProjection n G U

62 (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =

63 modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm

64 (modNCompletedGroupAlgebraProjection m G U x) := by

65 unfold modNCompletedGroupAlgebraProjection modNCompletedGroupAlgebraCoeffMap

66 rfl

68omit [Fact (0 < n)] [Fact (0 < m)] in

69/-- Composition lemma modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap. -/

70@[simp 900]

71theorem modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap

72 (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) (hnm : n ∣ m) :

73 (modNCompletedGroupAlgebraStageAugmentation n G U).comp

74 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm) =

75 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp

76 (modNCompletedGroupAlgebraStageAugmentation m G U) := by

77 apply RingHom.ext

78 intro x

79 refine MonoidAlgebra.induction_on

80 (p := fun x =>

81 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

82 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm)) x =

83 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

84 (modNCompletedGroupAlgebraStageAugmentation m G U)) x)

85 x ?_ ?_ ?_

86 · intro q

87 rw [RingHom.comp_apply, RingHom.comp_apply, modNCompletedGroupAlgebraStageCoeffMap_of,

88 modNCompletedGroupAlgebraStageAugmentation_of,

89 modNCompletedGroupAlgebraStageAugmentation_of]

90 simpa [modNCompletedCoeffMap] using

91 (map_one (modNCompletedCoeffMap (n := n) (m := m) hnm)).symm

92 · intro x y hx hy

93 simp only [RingHom.map_add, hx, RingHom.coe_comp, Function.comp_apply, hy]

94 · intro a x hx

95 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=

96 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm

97 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]

98 have hcoeff :

99 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

100 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm))

101 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =

102 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

103 (modNCompletedGroupAlgebraStageAugmentation m G U))

104 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) := by

105 have hleft :

106 ((modNCompletedGroupAlgebraStageAugmentation n G U).comp

107 (modNCompletedGroupAlgebraStageCoeffMap (n := n) (m := m) (G := G) U hnm))

108 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =

109 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by

110 simp only [modNCompletedGroupAlgebraStageAugmentation, modNCompletedGroupAlgebraStageCoeffMap,

111 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,

112 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe, MonoidAlgebra.lift_single,

113 MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.single_mul_single, mul_one,

114 MonoidHom.one_apply]

115 have hright :

116 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

117 (modNCompletedGroupAlgebraStageAugmentation m G U))

118 (algebraMap (ModNCompletedCoeff m) (ModNCompletedGroupAlgebraStage m G U) a) =

119 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by

120 simp only [modNCompletedGroupAlgebraStageAugmentation, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,

121 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe, MonoidAlgebra.lift_single,

122 MonoidHom.one_apply, smul_eq_mul, mul_one]

123 rfl

124 exact hleft.trans hright.symm

125 rw [hcoeff]

126

127omit [Fact (0 < n)] [Fact (0 < m)] in

128/-- Composition lemma modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap. -/

129@[simp 900]

130theorem modNCompletedGroupAlgebraStageAugmentationInClass_comp_coeffMap

131 (C : ProCGroups.FiniteGroupClass.{u}) (U : CompletedGroupAlgebraIndexInClass G C) (hnm : n ∣ m) :

132 (modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp

133 (modNCompletedGroupAlgebraStageCoeffMapInClass

134 (n := n) (m := m) (G := G) C U hnm) =

135 (modNCompletedCoeffMap (n := n) (m := m) hnm).comp

136 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U) := by

137 apply RingHom.ext

138 intro x

139 refine MonoidAlgebra.induction_on

140 (p := fun x =>

141 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp

142 (modNCompletedGroupAlgebraStageCoeffMapInClass

143 (n := n) (m := m) (G := G) C U hnm)) x =

144 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

145 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U)) x)

146 x ?_ ?_ ?_

147 · intro q

148 rw [RingHom.comp_apply, RingHom.comp_apply, modNCompletedGroupAlgebraStageCoeffMapInClass_of,

149 modNCompletedGroupAlgebraStageAugmentationInClass_of,

150 modNCompletedGroupAlgebraStageAugmentationInClass_of]

151 simpa [modNCompletedCoeffMap] using

152 (map_one (modNCompletedCoeffMap (n := n) (m := m) hnm)).symm

153 · intro x y hx hy

154 simp only [RingHom.map_add, hx, RingHom.coe_comp, Function.comp_apply, hy]

155 · intro a x hx

156 letI : Algebra (ModNCompletedCoeff m) (ModNCompletedCoeff n) :=

157 ZMod.algebra' (R := ModNCompletedCoeff n) (m := n) (n := m) hnm

158 rw [Algebra.smul_def, RingHom.map_mul, RingHom.map_mul, hx]

159 have hcoeff :

160 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp

161 (modNCompletedGroupAlgebraStageCoeffMapInClass

162 (n := n) (m := m) (G := G) C U hnm))

163 (algebraMap (ModNCompletedCoeff m)

164 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =

165 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

166 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U))

167 (algebraMap (ModNCompletedCoeff m)

168 (ModNCompletedGroupAlgebraStageInClass m G C U) a) := by

169 have hleft :

170 ((modNCompletedGroupAlgebraStageAugmentationInClass n G C U).comp

171 (modNCompletedGroupAlgebraStageCoeffMapInClass

172 (n := n) (m := m) (G := G) C U hnm))

173 (algebraMap (ModNCompletedCoeff m)

174 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =

175 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by

176 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, modNCompletedGroupAlgebraStageCoeffMapInClass,

177 modNCompletedGroupRingCoeffMap, AlgHom.toRingHom_eq_coe, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self,

178 RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe, MonoidAlgebra.lift_single,

179 MonoidAlgebra.of_apply, Algebra.smul_def, MonoidAlgebra.single_mul_single, mul_one,

180 MonoidHom.one_apply]

181 have hright :

182 ((modNCompletedCoeffMap (n := n) (m := m) hnm).comp

183 (modNCompletedGroupAlgebraStageAugmentationInClass m G C U))

184 (algebraMap (ModNCompletedCoeff m)

185 (ModNCompletedGroupAlgebraStageInClass m G C U) a) =

186 algebraMap (ModNCompletedCoeff m) (ModNCompletedCoeff n) a := by

187 simp only [modNCompletedGroupAlgebraStageAugmentationInClass, MonoidAlgebra.coe_algebraMap,

188 Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq, RingHom.comp_apply, RingHom.coe_coe,

189 MonoidAlgebra.lift_single, MonoidHom.one_apply, smul_eq_mul, mul_one]

190 rfl

191 exact hleft.trans hright.symm

192 rw [hcoeff]

193

194omit [Fact (0 < n)] [Fact (0 < m)] in

195/-- 法 n 係数で定めた augmentation または augmentation ideal への標準写像が関手的写像が有限段階射影と両立することを述べる。 -/

196@[simp]

197theorem modNCompletedGroupAlgebraAugmentation_coeffMap

198 (hnm : n ∣ m) (x : ModNCompletedGroupAlgebra m G) :

199 modNCompletedGroupAlgebraAugmentation n G

200 (modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x) =

201 modNCompletedCoeffMap (n := n) (m := m) hnm

202 (modNCompletedGroupAlgebraAugmentation m G x) := by

203 unfold modNCompletedGroupAlgebraAugmentation modNCompletedGroupAlgebraAugmentationAt

204 rw [modNCompletedGroupAlgebraProjection_coeffMap]

205 exact congrFun

206 (congrArg DFunLike.coe

207 (modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap

208 (n := n) (m := m) (G := G) (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) hnm))

209 (modNCompletedGroupAlgebraProjection m G (_root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G) x)

210

211/-- The modulus-direction map on augmentation kernels. -/

212def modNCompletedGroupAlgebraAugmentationKernelCoeffMap

213 (hnm : n ∣ m) :

214 ModNCompletedGroupAlgebraAugmentationKernel m G →

215 ModNCompletedGroupAlgebraAugmentationKernel n G := by

216 intro x

217 refine ⟨modNCompletedGroupAlgebraCoeffMap (n := n) (m := m) (G := G) hnm x.1, ?_⟩

218 rw [mem_modNCompletedGroupAlgebraAugmentationKernel_iff,

219 modNCompletedGroupAlgebraAugmentation_coeffMap]

220 simpa [map_zero, modNCompletedCoeffMap] using

221 congrArg (modNCompletedCoeffMap (n := n) (m := m) hnm) x.2

222

223/-- The standard divisibility relation between prime powers with the same base. -/

224theorem primePow_dvd_primePow

225 (ℓ : ℕ) {a b : ℕ} (hab : a ≤ b) :

226 ℓ ^ a ∣ ℓ ^ b := by

227 exact Nat.pow_dvd_pow ℓ hab

228

229/-- The modulus-direction completed map specialized to prime-power stages. -/

230def primePowCompletedGroupAlgebraCoeffMap

231 (ℓ : ℕ) {a b : ℕ}

232 (hab : a ≤ b) :

233 ModNCompletedGroupAlgebra (ℓ ^ b) G → ModNCompletedGroupAlgebra (ℓ ^ a) G :=

234 modNCompletedGroupAlgebraCoeffMap (n := ℓ ^ a) (m := ℓ ^ b) (G := G)

235 (primePow_dvd_primePow (ℓ := ℓ) hab)

236

237/-- The modulus-direction augmentation-kernel map specialized to prime-power stages. -/

238def primePowCompletedGroupAlgebraAugmentationKernelCoeffMap

239 (ℓ : ℕ) {a b : ℕ}

240 (hab : a ≤ b) :

241 ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ b) G →

242 ModNCompletedGroupAlgebraAugmentationKernel (ℓ ^ a) G :=

243 modNCompletedGroupAlgebraAugmentationKernelCoeffMap

244 (n := ℓ ^ a) (m := ℓ ^ b) (G := G)

245 (primePow_dvd_primePow (ℓ := ℓ) hab)

246

247

248variable (ℓ : ℕ) [Fact (0 < ℓ)]

249variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]

250

251/-- The two-parameter index `(a, U)` for the prime-power residue-coefficient stages. -/

252abbrev PrimePowerCompletedGroupAlgebraIndex :=

253 ℕ × _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G

254

255/-- The two-parameter index `(a, U)` for prime-power stages over a quotient class `C`. -/

256abbrev PrimePowerCompletedGroupAlgebraIndexInClass (C : ProCGroups.FiniteGroupClass.{u}) :=

257 ℕ × CompletedGroupAlgebraIndexInClass G C

258end

259

260end FoxDifferential