Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Multiplicative

1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.AddCommGroup

3/-!

4# Fox differential: prime-power completed group algebra — system — ring — multiplicative

6The principal declarations in this module are:

8- `instRingPrimePowerCompletedGroupAlgebraStage`

9 Each finite prime-power group-algebra stage carries its standard ring structure.

10- `instRingPrimePowerCompletedGroupAlgebraFamily`

11 The dependent family of finite prime-power group-algebra stages carries the pointwise ring

12 structure.

13- `coe_one_primePowerCompletedGroupAlgebra`

14 The multiplicative identity in the prime-power completed group algebra is computed coordinatewise.

15- `coe_mul_primePowerCompletedGroupAlgebra`

16 Multiplication in the prime-power completed group algebra is computed coordinatewise.

17-/

19namespace FoxDifferential

21noncomputable section

23open ProCGroups.InverseSystems

24open ProCGroups.ProC

26universe u

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

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

31attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraStage

32attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebraFamily

33attribute [local instance] instAddCommGroupPrimePowerCompletedGroupAlgebra

35/-- The prime-power completed group algebra has a coordinatewise multiplicative identity. -/

36instance instOnePrimePowerCompletedGroupAlgebra : One (PrimePowerCompletedGroupAlgebra ℓ G) where

37 one := ⟨fun i => (1 : PrimePowerCompletedGroupAlgebraStage ℓ G i), by

38 intro i j hij

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

40 (1 : PrimePowerCompletedGroupAlgebraStage ℓ G j) = 1

41 exact map_one _⟩

43/--

44Multiplication on the completed group algebra is defined coordinatewise through the finite-stage

45group-algebra products.

46-/

47instance instMulPrimePowerCompletedGroupAlgebra : Mul (PrimePowerCompletedGroupAlgebra ℓ G) where

48 mul x y := ⟨fun i =>

49 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) *

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

51 intro i j hij

52 calc

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

54 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *

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

56 =

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

58 (show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) *

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

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

61 rw [map_mul]

62 _ =

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

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

65 exact congrArg₂ HMul.hMul (x.2 i j hij) (y.2 i j hij)⟩

67/-- Natural number casts in the prime-power completed group algebra are computed coordinatewise. -/

68instance instNatCastPrimePowerCompletedGroupAlgebra :

69 NatCast (PrimePowerCompletedGroupAlgebra ℓ G) where

70 natCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by

71 intro i j hij

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

73 (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n

74 exact map_natCast _ _⟩

76/-- Integer casts in the prime-power completed group algebra are computed coordinatewise. -/

77instance instIntCastPrimePowerCompletedGroupAlgebra :

78 IntCast (PrimePowerCompletedGroupAlgebra ℓ G) where

79 intCast n := ⟨fun i => (n : PrimePowerCompletedGroupAlgebraStage ℓ G i), by

80 intro i j hij

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

82 (n : PrimePowerCompletedGroupAlgebraStage ℓ G j) = n

83 exact map_intCast _ _⟩

85/-- Each finite prime-power group-algebra stage carries its standard ring structure. -/

86@[reducible]

87private def instRingPrimePowerCompletedGroupAlgebraStage

88 (i : PrimePowerCompletedGroupAlgebraIndex G) :

89 Ring ((primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

90 dsimp [primePowerCompletedGroupAlgebraSystem, PrimePowerCompletedGroupAlgebraStage]

91 infer_instance

92attribute [local instance] instRingPrimePowerCompletedGroupAlgebraStage

94/--

95The dependent family of finite prime-power group-algebra stages carries the pointwise ring

96structure.

97-/

98@[reducible]

99private def instRingPrimePowerCompletedGroupAlgebraFamily :

100 Ring

101 ((i : PrimePowerCompletedGroupAlgebraIndex G) →

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

103 inferInstance

104attribute [local instance] instRingPrimePowerCompletedGroupAlgebraFamily

105

106/-- Powers in the prime-power completed group algebra are computed coordinatewise. -/

107instance instPowPrimePowerCompletedGroupAlgebra : Pow (PrimePowerCompletedGroupAlgebra ℓ G) ℕ where

108 pow x n := ⟨fun i => (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n, by

109 intro i j hij

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

111 ((show PrimePowerCompletedGroupAlgebraStage ℓ G j from x.1 j) ^ n) =

112 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) ^ n

113 rw [map_pow]

114 exact congrArg (fun t => t ^ n) (x.2 i j hij)⟩

115

116omit [Fact (0 < ℓ)] in

117/--

118The multiplicative identity in the prime-power completed group algebra is computed

119coordinatewise.

120-/

121@[simp]

122theorem coe_one_primePowerCompletedGroupAlgebra :

123 ((1 : PrimePowerCompletedGroupAlgebra ℓ G) :

124 (i : PrimePowerCompletedGroupAlgebraIndex G) →

125 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =

126 (1 :

127 (i : PrimePowerCompletedGroupAlgebraIndex G) →

128 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

129 funext i

130 rfl

131

132omit [Fact (0 < ℓ)] in

133/-- Multiplication in the prime-power completed group algebra is computed coordinatewise. -/

134@[simp]

135theorem coe_mul_primePowerCompletedGroupAlgebra

136 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :

137 ((x * y : PrimePowerCompletedGroupAlgebra ℓ G) :

138 (i : PrimePowerCompletedGroupAlgebraIndex G) →

139 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =

140 (x * y :

141 (i : PrimePowerCompletedGroupAlgebraIndex G) →

142 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

143 funext i

144 rfl

145

146omit [Fact (0 < ℓ)] in

147/-- Natural number casts in the prime-power completed group algebra are computed coordinatewise. -/

148@[simp]

149theorem coe_natCast_primePowerCompletedGroupAlgebra

150 (n : ℕ) :

151 ((n : PrimePowerCompletedGroupAlgebra ℓ G) :

152 (i : PrimePowerCompletedGroupAlgebraIndex G) →

153 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =

154 (n :

155 (i : PrimePowerCompletedGroupAlgebraIndex G) →

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

157 funext i

158 rfl

159

160omit [Fact (0 < ℓ)] in

161/-- Integer casts in the prime-power completed group algebra are computed coordinatewise. -/

162@[simp]

163theorem coe_intCast_primePowerCompletedGroupAlgebra

164 (n : ℤ) :

165 ((n : PrimePowerCompletedGroupAlgebra ℓ G) :

166 (i : PrimePowerCompletedGroupAlgebraIndex G) →

167 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =

168 (n :

169 (i : PrimePowerCompletedGroupAlgebraIndex G) →

170 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

171 funext i

172 rfl

173

174omit [Fact (0 < ℓ)] in

175/-- Powers in the prime-power completed group algebra are computed coordinatewise. -/

176@[simp]

177theorem coe_pow_primePowerCompletedGroupAlgebra

178 (x : PrimePowerCompletedGroupAlgebra ℓ G) (n : ℕ) :

179 ((x ^ n : PrimePowerCompletedGroupAlgebra ℓ G) :

180 (i : PrimePowerCompletedGroupAlgebraIndex G) →

181 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) =

182 (x ^ n :

183 (i : PrimePowerCompletedGroupAlgebraIndex G) →

184 (primePowerCompletedGroupAlgebraSystem ℓ G).X i) := by

185 funext i

186 rfl

187

188/--

189The completed group algebra is a ring because all ring operations and ring axioms are inherited

190coordinatewise from the finite-stage group algebras.

191-/

192instance instRingPrimePowerCompletedGroupAlgebra :

193 Ring (PrimePowerCompletedGroupAlgebra ℓ G) :=

194 Function.Injective.ring

195 (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>

196 (x :

197 (i : PrimePowerCompletedGroupAlgebraIndex G) →

198 (primePowerCompletedGroupAlgebraSystem ℓ G).X i))

199 Subtype.val_injective

200 (coe_zero_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

201 (coe_one_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

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

203 (coe_mul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

204 (coe_neg_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

205 (coe_sub_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G))

206 (fun n x => coe_nsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)

207 (fun n x => coe_zsmul_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n x)

208 (fun x n => coe_pow_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) x n)

209 (by

210 intro n

211 exact coe_natCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) n)

212 (by

213 intro z

214 exact coe_intCast_primePowerCompletedGroupAlgebra (ℓ := ℓ) (G := G) z)

215

216end

217

218end FoxDifferential