FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/AddCommGroup.lean

1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraModN.System.Basic

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraModN/System/AddCommGroup.lean

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Completed coefficient algebras

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

15-/

16namespace FoxDifferential

18noncomputable section

20open ProCGroups.InverseSystems

21open ProCGroups.ProC

23universe u

26variable (n : ℕ) [Fact (0 < n)]

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

29instance instZeroModNCompletedGroupAlgebra : Zero (ModNCompletedGroupAlgebra n G) where

30 zero := ⟨fun U => (0 : ModNCompletedGroupAlgebraStage n G U), by

31 intro U V hUV

32 change modNCompletedGroupAlgebraTransition n G hUV

33 (0 : ModNCompletedGroupAlgebraStage n G V) = 0

34 exact map_zero (modNCompletedGroupAlgebraTransition n G hUV)⟩

36instance instAddModNCompletedGroupAlgebra : Add (ModNCompletedGroupAlgebra n G) where

37 add x y := ⟨fun U =>

38 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +

39 (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by

40 intro U V hUV

41 calc

42 modNCompletedGroupAlgebraTransition n G hUV

43 ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) +

44 (show ModNCompletedGroupAlgebraStage n G V from y.1 V))

45 =

46 modNCompletedGroupAlgebraTransition n G hUV

47 (show ModNCompletedGroupAlgebraStage n G V from x.1 V) +

48 modNCompletedGroupAlgebraTransition n G hUV

49 (show ModNCompletedGroupAlgebraStage n G V from y.1 V) := by

50 rw [map_add]

51 _ =

52 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +

53 (show ModNCompletedGroupAlgebraStage n G U from y.1 U) := by

54 exact congrArg₂ HAdd.hAdd (x.2 U V hUV) (y.2 U V hUV)⟩

56instance instAddZeroClassModNCompletedGroupAlgebra :

57 AddZeroClass (ModNCompletedGroupAlgebra n G) where

58 zero := 0

59 add := (· + ·)

60 zero_add x := by

61 apply Subtype.ext

62 funext U

63 change (0 : ModNCompletedGroupAlgebraStage n G U) +

64 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) =

65 (show ModNCompletedGroupAlgebraStage n G U from x.1 U)

66 simp only [zero_add]

67 add_zero x := by

68 apply Subtype.ext

69 funext U

70 change (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +

71 (0 : ModNCompletedGroupAlgebraStage n G U) =

72 (show ModNCompletedGroupAlgebraStage n G U from x.1 U)

73 simp only [add_zero]

75instance instNegModNCompletedGroupAlgebra : Neg (ModNCompletedGroupAlgebra n G) where

76 neg x := ⟨fun U => -(show ModNCompletedGroupAlgebraStage n G U from x.1 U), by

77 intro U V hUV

78 change modNCompletedGroupAlgebraTransition n G hUV

79 (-(show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =

80 -(show ModNCompletedGroupAlgebraStage n G U from x.1 U)

81 rw [map_neg]

82 exact congrArg Neg.neg (x.2 U V hUV)⟩

84instance instSubModNCompletedGroupAlgebra : Sub (ModNCompletedGroupAlgebra n G) where

85 sub x y := ⟨fun U =>

86 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -

87 (show ModNCompletedGroupAlgebraStage n G U from y.1 U), by

88 intro U V hUV

89 change modNCompletedGroupAlgebraTransition n G hUV

90 ((show ModNCompletedGroupAlgebraStage n G V from x.1 V) -

91 (show ModNCompletedGroupAlgebraStage n G V from y.1 V)) =

92 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -

93 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)

94 rw [map_sub]

95 exact congrArg₂ HSub.hSub (x.2 U V hUV) (y.2 U V hUV)⟩

97instance instSMulNatModNCompletedGroupAlgebra : SMul ℕ (ModNCompletedGroupAlgebra n G) where

98 smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by

99 intro U V hUV

100 change modNCompletedGroupAlgebraTransition n G hUV

101 (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =

102 m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)

103 rw [map_nsmul]

104 exact congrArg (m • ·) (x.2 U V hUV)⟩

105

106instance instSMulIntModNCompletedGroupAlgebra : SMul ℤ (ModNCompletedGroupAlgebra n G) where

107 smul m x := ⟨fun U => m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U), by

108 intro U V hUV

109 change modNCompletedGroupAlgebraTransition n G hUV

110 (m • (show ModNCompletedGroupAlgebraStage n G V from x.1 V)) =

111 m • (show ModNCompletedGroupAlgebraStage n G U from x.1 U)

112 rw [map_zsmul]

113 exact congrArg (m • ·) (x.2 U V hUV)⟩

114

115instance instAddCommGroupModNCompletedGroupAlgebraStage (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :

116 AddCommGroup ((modNCompletedGroupAlgebraSystem n G).X U) := by

117 dsimp [modNCompletedGroupAlgebraSystem, ModNCompletedGroupAlgebraStage]

118 infer_instance

119

120instance instAddCommGroupModNCompletedGroupAlgebraFamily :

121 AddCommGroup ((i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) :=

122 inferInstance

123

124omit [Fact (0 < n)] in

125/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

126@[simp]

127theorem coe_zero_modNCompletedGroupAlgebra :

128 ((0 : ModNCompletedGroupAlgebra n G) :

129 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) = 0 := by

130 funext U

131 rfl

132

133omit [Fact (0 < n)] in

134/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

135@[simp]

136theorem coe_add_modNCompletedGroupAlgebra

137 (x y : ModNCompletedGroupAlgebra n G) :

138 ((x + y : ModNCompletedGroupAlgebra n G) :

139 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =

140 x + y := by

141 funext U

142 rfl

143

144omit [Fact (0 < n)] in

145/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

146@[simp]

147theorem coe_neg_modNCompletedGroupAlgebra

148 (x : ModNCompletedGroupAlgebra n G) :

149 ((-x : ModNCompletedGroupAlgebra n G) :

150 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =

151 -x := by

152 funext U

153 rfl

154

155omit [Fact (0 < n)] in

156/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

157@[simp]

158theorem coe_sub_modNCompletedGroupAlgebra

159 (x y : ModNCompletedGroupAlgebra n G) :

160 ((x - y : ModNCompletedGroupAlgebra n G) :

161 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =

162 x - y := by

163 funext U

164 rfl

165

166omit [Fact (0 < n)] in

167/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

168@[simp]

169theorem coe_nsmul_modNCompletedGroupAlgebra

170 (m : ℕ) (x : ModNCompletedGroupAlgebra n G) :

171 ((m • x : ModNCompletedGroupAlgebra n G) :

172 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =

173 m • x := by

174 funext U

175 rfl

176

177omit [Fact (0 < n)] in

178/-- 法 n 係数で定めた部分型から基礎にある完備群環への包含が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/

179@[simp]

180theorem coe_zsmul_modNCompletedGroupAlgebra

181 (m : ℤ) (x : ModNCompletedGroupAlgebra n G) :

182 ((m • x : ModNCompletedGroupAlgebra n G) :

183 (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i) =

184 m • x := by

185 funext U

186 rfl

187

188instance instAddCommGroupModNCompletedGroupAlgebra :

189 AddCommGroup (ModNCompletedGroupAlgebra n G) :=

190 Function.Injective.addCommGroup

191 (fun x : ModNCompletedGroupAlgebra n G =>

192 (x : (i : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) → (modNCompletedGroupAlgebraSystem n G).X i))

193 Subtype.val_injective

194 (coe_zero_modNCompletedGroupAlgebra (n := n) (G := G))

195 (coe_add_modNCompletedGroupAlgebra (n := n) (G := G))

196 (coe_neg_modNCompletedGroupAlgebra (n := n) (G := G))

197 (coe_sub_modNCompletedGroupAlgebra (n := n) (G := G))

198 (fun x m => coe_nsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)

199 (fun x m => coe_zsmul_modNCompletedGroupAlgebra (n := n) (G := G) m x)

200

201omit [Fact (0 < n)] in

202/-- 法 n の係数段階で、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/

203@[simp]

204theorem modNCompletedGroupAlgebraProjection_zero (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G) :

205 modNCompletedGroupAlgebraProjection n G U (0 : ModNCompletedGroupAlgebra n G) = 0 := by

206 change (0 : ModNCompletedGroupAlgebraStage n G U) = 0

207 rfl

208

209omit [Fact (0 < n)] in

210/-- 法 n の係数段階で、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/

211@[simp]

212theorem modNCompletedGroupAlgebraProjection_add (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)

213 (x y : ModNCompletedGroupAlgebra n G) :

214 modNCompletedGroupAlgebraProjection n G U (x + y) =

215 modNCompletedGroupAlgebraProjection n G U x +

216 modNCompletedGroupAlgebraProjection n G U y := by

217 change (show ModNCompletedGroupAlgebraStage n G U from (x + y).1 U) =

218 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) +

219 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)

220 rfl

221

222omit [Fact (0 < n)] in

223/-- 法 n の係数段階で、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/

224@[simp]

225theorem modNCompletedGroupAlgebraProjection_neg (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)

226 (x : ModNCompletedGroupAlgebra n G) :

227 modNCompletedGroupAlgebraProjection n G U (-x) =

228 -modNCompletedGroupAlgebraProjection n G U x := by

229 change (show ModNCompletedGroupAlgebraStage n G U from (-x).1 U) =

230 -(show ModNCompletedGroupAlgebraStage n G U from x.1 U)

231 rfl

232

233omit [Fact (0 < n)] in

234/-- 法 n の係数段階で、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/

235@[simp]

236theorem modNCompletedGroupAlgebraProjection_sub (U : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)

237 (x y : ModNCompletedGroupAlgebra n G) :

238 modNCompletedGroupAlgebraProjection n G U (x - y) =

239 modNCompletedGroupAlgebraProjection n G U x -

240 modNCompletedGroupAlgebraProjection n G U y := by

241 change (show ModNCompletedGroupAlgebraStage n G U from (x - y).1 U) =

242 (show ModNCompletedGroupAlgebraStage n G U from x.1 U) -

243 (show ModNCompletedGroupAlgebraStage n G U from y.1 U)

244 rfl

245

246omit [Fact (0 < n)] in

247

248end

249

250end FoxDifferential