FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/Module.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Additive
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/Module.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
22universe u
25variable (ℓ : ℕ) [Fact (0 < ℓ)]
26variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
28omit [Fact (0 < ℓ)] in
29/-- 素冪係数段階で、有限段階間の遷移写像はスカラー倍と両立する。 -/
30@[simp 900]
32 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j)
33 (a : ZMod (ℓ ^ j.1))
34 (x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
36 (ℓ := ℓ) (G := G) hij (a • x) =
38 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
39 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
41 (ℓ := ℓ) (G := G) hij x := by
42 apply Subtype.ext
43 change primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij
44 ((a • x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
45 PrimePowerCompletedGroupAlgebraStage ℓ G j) =
47 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
48 (primePow_dvd_primePow (ℓ := ℓ) hij.1) a) •
50 (ℓ := ℓ) (G := G) hij x :
51 primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i) :
53 simpa using
55 (ℓ := ℓ) (G := G) hij a
56 ((x : primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j) :
60 CommRing (PrimePowerCompletedCoeff ℓ G) := by
61 infer_instance
64 SMul (PrimePowerCompletedCoeff ℓ G)
65 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
66 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
67 smul a x := fun i =>
68 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
69 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x i)
71instance instModulePpCoeffPpGAAugIdealFamily :
72 Module (PrimePowerCompletedCoeff ℓ G)
73 ((i : PrimePowerCompletedGroupAlgebraIndex G) →
74 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) where
75 one_smul x := by
76 funext i
77 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
78 (1 : PrimePowerCompletedCoeff ℓ G)) •
80 (ℓ := ℓ) (G := G) i from x i) =
82 (ℓ := ℓ) (G := G) i from x i)
83 rw [primePowerCompletedCoeffProjection_one, one_smul]
84 mul_smul a b x := by
85 funext i
86 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a * b)) •
88 (ℓ := ℓ) (G := G) i from x i) =
89 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
90 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
92 (ℓ := ℓ) (G := G) i from x i))
93 rw [primePowerCompletedCoeffProjection_mul, mul_smul]
94 smul_zero a := by
95 funext i
96 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
98 (ℓ := ℓ) (G := G) i) = 0
99 rw [smul_zero]
100 smul_add a x y := by
101 funext i
102 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
104 (ℓ := ℓ) (G := G) i from x i) +
106 (ℓ := ℓ) (G := G) i from y i)) =
107 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
109 (ℓ := ℓ) (G := G) i from x i) +
110 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
112 (ℓ := ℓ) (G := G) i from y i)
113 rw [smul_add]
114 add_smul a b x := by
115 funext i
116 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (a + b)) •
118 (ℓ := ℓ) (G := G) i from x i) =
119 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
121 (ℓ := ℓ) (G := G) i from x i) +
122 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i b) •
124 (ℓ := ℓ) (G := G) i from x i)
125 rw [primePowerCompletedCoeffProjection_add, add_smul]
126 zero_smul x := by
127 funext i
128 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
129 (0 : PrimePowerCompletedCoeff ℓ G)) •
131 (ℓ := ℓ) (G := G) i from x i) = 0
132 rw [primePowerCompletedCoeffProjection_zero, zero_smul]
135 SMul (PrimePowerCompletedCoeff ℓ G)
136 (PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) where
137 smul a x := ⟨fun i =>
138 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
140 (ℓ := ℓ) (G := G) i from x.1 i), by
141 intro i j hij
142 calc
144 (ℓ := ℓ) (G := G) hij
145 ((primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a) •
146 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
147 from x.1 j)) =
149 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
150 (primePow_dvd_primePow (ℓ := ℓ) hij.1)
151 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)) •
153 (ℓ := ℓ) (G := G) hij
154 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) j
155 from x.1 j) := by
156 exact
158 (ℓ := ℓ) (G := G) hij
159 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) j a)
161 (ℓ := ℓ) (G := G) j from x.1 j)
162 _ =
163 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
165 (ℓ := ℓ) (G := G) i from x.1 i) := by
166 exact congrArg₂ HSMul.hSMul (a.2 i j hij) (x.2 i j hij)⟩
168omit [Fact (0 < ℓ)] in
169/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
170@[simp]
172 (a : PrimePowerCompletedCoeff ℓ G)
173 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
175 (ℓ := ℓ) (G := G)
176 ((a • x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
177 (i : PrimePowerCompletedGroupAlgebraIndex G) →
179 a • (x :
180 (i : PrimePowerCompletedGroupAlgebraIndex G) →
181 (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).X i) := by
182 funext i
183 change (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
184 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i) =
185 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
186 (show primePowerCompletedGroupAlgebraStageAugmentationIdeal (ℓ := ℓ) (G := G) i from x.1 i)
187 rfl
189instance instModulePpCoeffPpGAAugIdeal :
190 Module (PrimePowerCompletedCoeff ℓ G)
192 Function.Injective.module (PrimePowerCompletedCoeff ℓ G)
193 { toFun := Subtype.val
194 map_zero' := rfl
195 map_add' := fun _ _ => rfl }
196 Subtype.val_injective
197 (coe_smul_primePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G))
200end
202end FoxDifferential