FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/Projection.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/System/Ring/Projection.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]
28omit [Fact (0 < ℓ)] in
29/-- 素冪係数で定めた 有限段階射影が自然数の標準像を各有限段階で同じ自然数の標準像として計算することを述べる。 -/
30@[simp]
32 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
33 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
34 (n : PrimePowerCompletedGroupAlgebra ℓ G) = n := by
35 change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
36 rfl
38omit [Fact (0 < ℓ)] in
39/-- 素冪係数で定めた 有限段階射影が整数の標準像を各有限段階で同じ整数の標準像として計算することを述べる。 -/
40@[simp]
42 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
43 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
44 (n : PrimePowerCompletedGroupAlgebra ℓ G) = n := by
45 change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
46 rfl
48omit [Fact (0 < ℓ)] in
49/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
50@[simp]
52 (i : PrimePowerCompletedGroupAlgebraIndex G) :
53 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
54 (0 : PrimePowerCompletedGroupAlgebra ℓ G) = 0 := by
55 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
56 rfl
58omit [Fact (0 < ℓ)] in
59/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
60@[simp]
63 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
64 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y) =
65 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x +
66 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
67 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x + y).1 i) =
68 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
69 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
70 rfl
72omit [Fact (0 < ℓ)] in
73/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
74@[simp]
77 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
78 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (-x) =
79 -primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x := by
80 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (-x).1 i) =
81 -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
82 rfl
84omit [Fact (0 < ℓ)] in
85/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
86@[simp]
89 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
90 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x - y) =
91 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x -
92 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
93 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x - y).1 i) =
94 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
95 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
96 rfl
98omit [Fact (0 < ℓ)] in
99/-- Composition lemma primePowerCompletedGroupAlgebraStageAugmentation_comp_transition. -/
100@[simp]
102 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
103 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2).comp
104 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) =
106 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
107 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
108 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2) := by
110 rw [← RingHom.comp_assoc]
112 rw [RingHom.comp_assoc]
115end
117end FoxDifferential