FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/Projection.lean
1import FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/CoefficientRings/CompletedGroupAlgebraPrimePower/Coeff/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 < ℓ)] [IsTopologicalGroup G] in
29/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は単位元を単位元へ送る。 -/
30@[simp]
32 (i : PrimePowerCompletedGroupAlgebraIndex G) :
33 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
34 (1 : PrimePowerCompletedCoeff ℓ G) = 1 := by
35 change (1 : ZMod (ℓ ^ i.1)) = 1
36 rfl
38omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
39/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は積を積へ送る。 -/
40@[simp]
43 (x y : PrimePowerCompletedCoeff ℓ G) :
44 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x * y) =
45 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x *
46 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
47 change (show ZMod (ℓ ^ i.1) from (x * y).1 i) =
48 (show ZMod (ℓ ^ i.1) from x.1 i) * (show ZMod (ℓ ^ i.1) from y.1 i)
49 rfl
51omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
52/-- 素冪係数で定めた 有限段階射影が自然数の標準像を各有限段階で同じ自然数の標準像として計算することを述べる。 -/
53@[simp]
55 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
56 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
57 (n : PrimePowerCompletedCoeff ℓ G) = n := by
58 change (n : ZMod (ℓ ^ i.1)) = n
59 rfl
61omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
62/-- 素冪係数で定めた 有限段階射影が整数の標準像を各有限段階で同じ整数の標準像として計算することを述べる。 -/
63@[simp]
65 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
66 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
67 (n : PrimePowerCompletedCoeff ℓ G) = n := by
68 change (n : ZMod (ℓ ^ i.1)) = n
69 rfl
71omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
72/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は零元を零元へ送る。 -/
73@[simp]
75 (i : PrimePowerCompletedGroupAlgebraIndex G) :
76 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
77 (0 : PrimePowerCompletedCoeff ℓ G) = 0 := by
78 change (0 : ZMod (ℓ ^ i.1)) = 0
79 rfl
81omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
82/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は和を和へ送る。 -/
83@[simp]
86 (x y : PrimePowerCompletedCoeff ℓ G) :
87 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x + y) =
88 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x +
89 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
90 change (show ZMod (ℓ ^ i.1) from (x + y).1 i) =
91 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
92 rfl
94omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
95/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は負元を負元へ送る。 -/
96@[simp]
99 (x : PrimePowerCompletedCoeff ℓ G) :
100 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (-x) =
101 -primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x := by
102 change (show ZMod (ℓ ^ i.1) from (-x).1 i) =
103 -(show ZMod (ℓ ^ i.1) from x.1 i)
104 rfl
106omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
107/-- 素冪係数段階で、完備群環またはその augmentation ideal の有限段階射影は差を差へ送る。 -/
108@[simp]
111 (x y : PrimePowerCompletedCoeff ℓ G) :
112 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x - y) =
113 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x -
114 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
115 change (show ZMod (ℓ ^ i.1) from (x - y).1 i) =
116 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
117 rfl
119omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
120/-- Coefficient projections with the same prime-power exponent do not depend on the
124 (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
125 (z : PrimePowerCompletedCoeff ℓ G) :
126 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
127 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z := by
128 let T : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G := _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G
129 let hTU : (a, T) ≤ (a, U) :=
130 ⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) U⟩
131 let hTV : (a, T) ≤ (a, V) :=
132 ⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) V⟩
133 have hTU_coeff :
135 (n := ℓ ^ a) (m := ℓ ^ a)
136 (primePow_dvd_primePow (ℓ := ℓ) hTU.1) = RingHom.id _ := by
137 have hproof :
138 primePow_dvd_primePow (ℓ := ℓ) hTU.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
139 Subsingleton.elim _ _
140 rw [hproof]
141 exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
142 have hTV_coeff :
144 (n := ℓ ^ a) (m := ℓ ^ a)
145 (primePow_dvd_primePow (ℓ := ℓ) hTV.1) = RingHom.id _ := by
146 have hproof :
147 primePow_dvd_primePow (ℓ := ℓ) hTV.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
148 Subsingleton.elim _ _
149 rw [hproof]
150 exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
151 have hU := z.2 (a, T) (a, U) hTU
152 have hV := z.2 (a, T) (a, V) hTV
153 have hU' :
154 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
155 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
156 simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTU_coeff] using
157 hU
158 have hV' :
159 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z =
160 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
161 simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTV_coeff] using
162 hV
163 exact hU'.trans hV'.symm
165end
167end FoxDifferential