FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/AddCommGroup.lean

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

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/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

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

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

28instance instZeroPrimePowerCompletedGroupAlgebra : Zero (PrimePowerCompletedGroupAlgebra ℓ G) where

29 zero := ⟨fun i => (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by

30 intro i j hij

31 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

32 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 0

33 exact map_zero _⟩

35instance instAddPrimePowerCompletedGroupAlgebra : Add (PrimePowerCompletedGroupAlgebra ℓ G) where

36 add x y := ⟨fun i =>

37 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +

38 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by

39 intro i j hij

40 calc

41 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

42 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +

43 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j))

44 =

45 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

46 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) +

47 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

48 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j) := by

49 rw [map_add]

50 _ =

51 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +

52 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i) := by

53 exact congrArg₂ HAdd.hAdd (x.2 i j hij) (y.2 i j hij)⟩

55instance instAddZeroClassPrimePowerCompletedGroupAlgebra :

56 AddZeroClass (PrimePowerCompletedGroupAlgebra ℓ G) where

57 zero := 0

58 add := (· + ·)

59 zero_add x := by

60 apply Subtype.ext

61 funext i

62 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) +

63 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) =

64 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

65 simp only [zero_add]

66 add_zero x := by

67 apply Subtype.ext

68 funext i

69 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +

70 (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) =

71 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

72 simp only [add_zero]

74instance instNegPrimePowerCompletedGroupAlgebra : Neg (PrimePowerCompletedGroupAlgebra ℓ G) where

75 neg x := ⟨fun i => -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by

76 intro i j hij

77 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

78 (-(show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =

79 -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

80 rw [map_neg]

81 exact congrArg Neg.neg (x.2 i j hij)⟩

83instance instSubPrimePowerCompletedGroupAlgebra : Sub (PrimePowerCompletedGroupAlgebra ℓ G) where

84 sub x y := ⟨fun i =>

85 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -

86 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i), by

87 intro i j hij

88 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

89 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) -

90 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from y.1 j)) =

91 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -

92 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)

93 rw [map_sub]

94 exact congrArg₂ HSub.hSub (x.2 i j hij) (y.2 i j hij)⟩

96instance instSMulNatPrimePowerCompletedGroupAlgebra :

97 SMul ℕ (PrimePowerCompletedGroupAlgebra ℓ G) where

98 smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by

99 intro i j hij

100 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

101 (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =

102 m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

103 rw [map_nsmul]

104 exact congrArg (m • ·) (x.2 i j hij)⟩

105

106instance instSMulIntPrimePowerCompletedGroupAlgebra :

107 SMul ℤ (PrimePowerCompletedGroupAlgebra ℓ G) where

108 smul m x := ⟨fun i => m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i), by

109 intro i j hij

110 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij

111 (m • (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j)) =

112 m • (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)

113 rw [map_zsmul]

114 exact congrArg (m • ·) (x.2 i j hij)⟩

115

116instance instAddCommGroupPrimePowerCompletedGroupAlgebraStage

117 (i : PrimePowerCompletedGroupAlgebraIndex G) :

118 AddCommGroup ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

119 dsimp [primePowerCompletedGroupAlgebraSystem, PrimePowerCompletedGroupAlgebraStage]

120 infer_instance

121

122instance instAddCommGroupPrimePowerCompletedGroupAlgebraFamily :

123 AddCommGroup

124 ((i : PrimePowerCompletedGroupAlgebraIndex G) →

125 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) :=

126 inferInstance

127

128omit [Fact (0 < ℓ)] in

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

130@[simp]

131theorem coe_zero_primePowerCompletedGroupAlgebra :

132 ((0 : PrimePowerCompletedGroupAlgebra ℓ G) :

133 (i : PrimePowerCompletedGroupAlgebraIndex G) →

134 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = 0 := by

135 funext i

136 rfl

137

138omit [Fact (0 < ℓ)] in

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

140@[simp]

141theorem coe_add_primePowerCompletedGroupAlgebra

142 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :

143 ((x + y : PrimePowerCompletedGroupAlgebra ℓ G) :

144 (i : PrimePowerCompletedGroupAlgebraIndex G) →

145 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x + y := by

146 funext i

147 rfl

148

149omit [Fact (0 < ℓ)] in

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

151@[simp]

152theorem coe_neg_primePowerCompletedGroupAlgebra

153 (x : PrimePowerCompletedGroupAlgebra ℓ G) :

154 ((-x : PrimePowerCompletedGroupAlgebra ℓ G) :

155 (i : PrimePowerCompletedGroupAlgebraIndex G) →

156 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = -x := by

157 funext i

158 rfl

159

160omit [Fact (0 < ℓ)] in

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

162@[simp]

163theorem coe_sub_primePowerCompletedGroupAlgebra

164 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :

165 ((x - y : PrimePowerCompletedGroupAlgebra ℓ G) :

166 (i : PrimePowerCompletedGroupAlgebraIndex G) →

167 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = x - y := by

168 funext i

169 rfl

170

171omit [Fact (0 < ℓ)] in

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

173@[simp]

174theorem coe_nsmul_primePowerCompletedGroupAlgebra

175 (m : ℕ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :

176 ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :

177 (i : PrimePowerCompletedGroupAlgebraIndex G) →

178 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x := by

179 funext i

180 rfl

181

182omit [Fact (0 < ℓ)] in

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

184@[simp]

185theorem coe_zsmul_primePowerCompletedGroupAlgebra

186 (m : ℤ) (x : PrimePowerCompletedGroupAlgebra ℓ G) :

187 ((m • x : PrimePowerCompletedGroupAlgebra ℓ G) :

188 (i : PrimePowerCompletedGroupAlgebraIndex G) →

189 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) = m • x := by

190 funext i

191 rfl

192

193instance instAddCommGroupPrimePowerCompletedGroupAlgebra :

194 AddCommGroup (PrimePowerCompletedGroupAlgebra ℓ G) :=

195 Function.Injective.addCommGroup

196 (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>

197 (x :

198 (i : PrimePowerCompletedGroupAlgebraIndex G) →

199 (primePowerCompletedGroupAlgebraSystem ℓ G).X i))

200 Subtype.val_injective

201 (coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

202 (coe_add_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

203 (coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

204 (coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

205 (fun x m => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)

206 (fun x m => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) m x)

207

208end

209

210end FoxDifferential