FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/LimitEquiv.lean
1import FoxDifferential.Completed.CoefficientRings.AugmentationIdealPrimePower.Module
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/AugmentationIdealPrimePower/LimitEquiv.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/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
31 (i : PrimePowerCompletedGroupAlgebraIndex G) :
32 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i
33 (0 : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) = 0 := by
34 rfl
36omit [Fact (0 < ℓ)] in
37/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
38@[simp]
41 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
42 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x + y) =
43 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x +
44 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y := by
45 rfl
47omit [Fact (0 < ℓ)] in
48/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
49@[simp]
52 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
53 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (-x) =
54 -primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
55 rfl
57omit [Fact (0 < ℓ)] in
58/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
59@[simp]
62 (x y : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
63 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (x - y) =
64 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x -
65 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i y := by
66 rfl
68omit [Fact (0 < ℓ)] in
69/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は自然数倍と両立する。 -/
70@[simp]
73 (m : ℕ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
74 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
75 m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
76 rfl
78omit [Fact (0 < ℓ)] in
79/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は整数倍と両立する。 -/
80@[simp]
83 (m : ℤ) (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
84 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (m • x) =
85 m • primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
86 rfl
88omit [Fact (0 < ℓ)] in
89/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影はスカラー倍と両立する。 -/
90@[simp]
93 (a : PrimePowerCompletedCoeff ℓ G)
94 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
95 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i (a • x) =
96 (primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i a) •
97 primePowerCompletedGroupAlgebraAugmentationIdealProjection (ℓ := ℓ) (G := G) i x := by
98 rfl
100/-- A prime-power augmentation-kernel point determines a compatible family in the finite-stage
101augmentation ideals. -/
103 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) →
105 intro x
106 refine ⟨fun i => ⟨primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1, ?_⟩, ?_⟩
108 (ℓ := ℓ) (G := G) (i := i)
109 (x := primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1)).2
111 (ℓ := ℓ) (G := G) (x := x.1)).1 x.2 i)
112 · intro i j hij
113 apply Subtype.ext
114 exact (primePowerCompletedGroupAlgebraSystem ℓ G).projection_compatible x.1 i j hij
116omit [Fact (0 < ℓ)] in
117/-- 素冪係数で定めた 有限段階射影がaugmentation ideal の元を基礎にある完備群環へ戻す写像の値を記述することを述べる。 -/
118@[simp]
120 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G))
121 (i : PrimePowerCompletedGroupAlgebraIndex G) :
123 (ℓ := ℓ) (G := G) i
124 (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x)) :
125 PrimePowerCompletedGroupAlgebraStage ℓ G i) =
126 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x.1 := rfl
128/-- A compatible family of prime-power finite-stage augmentation-ideal elements determines a
129prime-power augmentation-kernel point. -/
132 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) := by
133 intro x
134 let y : PrimePowerCompletedGroupAlgebra ℓ G := ⟨fun i => (x.1 i).1, by
135 intro i j hij
136 exact congrArg Subtype.val (x.2 i j hij)⟩
137 refine ⟨y, ?_⟩
139 (ℓ := ℓ) (G := G) (x := y)).2 (fun i =>
141 (ℓ := ℓ) (G := G) (i := i) (x := (x.1 i).1)).1 (x.1 i).2)
143omit [Fact (0 < ℓ)] in
144/-- 素冪係数で定めた 有限段階射影が対応する有限段階・係数段階・augmentation 構造と両立することを述べる。 -/
145@[simp]
148 (i : PrimePowerCompletedGroupAlgebraIndex G) :
149 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
151 (ℓ := ℓ) (G := G) x).1 =
153 (ℓ := ℓ) (G := G) i x) :
154 PrimePowerCompletedGroupAlgebraStage ℓ G i) := rfl
156omit [Fact (0 < ℓ)] in
157/-- 素冪係数で定めた augmentation または augmentation ideal への標準写像がaugmentation ideal の元を基礎にある完備群環へ戻す写像の値を記述することを述べる。 -/
158@[simp]
160 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
161 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
162 (toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x := by
163 apply Subtype.ext
164 apply (primePowerCompletedGroupAlgebraSystem ℓ G).ext
165 intro i
166 rfl
168omit [Fact (0 < ℓ)] in
169/-- Evaluation formula for toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of. -/
170@[simp]
172 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
173 toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
174 (ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x) = x := by
175 apply (primePowerCompletedGroupAlgebraAugmentationIdealSystem ℓ G).ext
176 intro i
177 apply Subtype.ext
178 rfl
180/-- The prime-power completed augmentation kernel is canonically equivalent to the inverse limit of
181the prime-power finite-stage augmentation ideals. -/
183 PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G) ≃
185 toFun := toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
186 invFun := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G)
187 left_inv := ofPrimePowerCompletedGroupAlgebraAugmentationIdeal_to (ℓ := ℓ) (G := G)
188 right_inv := toPrimePowerCompletedGroupAlgebraAugmentationIdeal_of (ℓ := ℓ) (G := G)
190omit [Fact (0 < ℓ)] in
191/-- Evaluation formula for primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_apply. -/
192@[simp]
194 (x : PrimePowerCompletedGroupAlgebraAugmentationKernel (ℓ := ℓ) (G := G)) :
196 (ℓ := ℓ) (G := G) x =
197 toPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x := rfl
199omit [Fact (0 < ℓ)] in
200/-- Evaluation formula for primePowerCompletedGroupAlgebraAugmentationKernelEquivInverseLimit_symm_apply. -/
201@[simp]
203 (x : PrimePowerCompletedGroupAlgebraAugmentationIdeal ℓ G) :
205 (ℓ := ℓ) (G := G)).symm x =
206 ofPrimePowerCompletedGroupAlgebraAugmentationIdeal (ℓ := ℓ) (G := G) x := rfl
208end
210end FoxDifferential