Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Projection
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.Coeff.Ring
3/-!
4# Fox differential: coefficient rings — prime-power completed group algebra — coeff — projection
6The principal declarations in this module are:
8- `primePowerCompletedCoeffProjection_one`
9 The finite-stage projection sends \(1\) to \(1\).
10- `primePowerCompletedCoeffProjection_mul`
11 The finite-stage projection preserves multiplication.
12- `primePowerCompletedCoeffProjection_natCast`
13 The finite-stage projection preserves natural number casts.
14- `primePowerCompletedCoeffProjection_intCast`
15 The finite-stage projection preserves integer casts.
16-/
18namespace FoxDifferential
20noncomputable section
22open ProCGroups.InverseSystems
23open ProCGroups.ProC
25universe u
27variable (ℓ : ℕ) [Fact (0 < ℓ)]
28variable (G : Type u) [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
31/-- The finite-stage projection sends \(1\) to \(1\). -/
32@[simp]
33theorem primePowerCompletedCoeffProjection_one
34 (i : PrimePowerCompletedGroupAlgebraIndex G) :
35 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
36 (1 : PrimePowerCompletedCoeff ℓ G) = 1 := by
37 change (1 : ZMod (ℓ ^ i.1)) = 1
38 rfl
40omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
41/-- The finite-stage projection preserves multiplication. -/
42@[simp]
43theorem primePowerCompletedCoeffProjection_mul
44 (i : PrimePowerCompletedGroupAlgebraIndex G)
45 (x y : PrimePowerCompletedCoeff ℓ G) :
46 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x * y) =
47 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x *
48 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
49 change (show ZMod (ℓ ^ i.1) from (x * y).1 i) =
50 (show ZMod (ℓ ^ i.1) from x.1 i) * (show ZMod (ℓ ^ i.1) from y.1 i)
51 rfl
53omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
54/-- The finite-stage projection preserves natural number casts. -/
55@[simp]
56theorem primePowerCompletedCoeffProjection_natCast
57 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
58 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
59 (n : PrimePowerCompletedCoeff ℓ G) = n := by
60 change (n : ZMod (ℓ ^ i.1)) = n
61 rfl
63omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
64/-- The finite-stage projection preserves integer casts. -/
65@[simp]
66theorem primePowerCompletedCoeffProjection_intCast
67 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
68 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
69 (n : PrimePowerCompletedCoeff ℓ G) = n := by
70 change (n : ZMod (ℓ ^ i.1)) = n
71 rfl
73omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
74/-- The finite-stage projection sends \(0\) to \(0\). -/
75@[simp]
76theorem primePowerCompletedCoeffProjection_zero
77 (i : PrimePowerCompletedGroupAlgebraIndex G) :
78 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i
79 (0 : PrimePowerCompletedCoeff ℓ G) = 0 := by
80 change (0 : ZMod (ℓ ^ i.1)) = 0
81 rfl
83omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
84/-- The prime-power coefficient projection preserves addition. -/
85@[simp]
86theorem primePowerCompletedCoeffProjection_add
87 (i : PrimePowerCompletedGroupAlgebraIndex G)
88 (x y : PrimePowerCompletedCoeff ℓ G) :
89 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x + y) =
90 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x +
91 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
92 change (show ZMod (ℓ ^ i.1) from (x + y).1 i) =
93 (show ZMod (ℓ ^ i.1) from x.1 i) + (show ZMod (ℓ ^ i.1) from y.1 i)
94 rfl
96omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
97/-- The prime-power coefficient projection preserves negation. -/
98@[simp]
99theorem primePowerCompletedCoeffProjection_neg
100 (i : PrimePowerCompletedGroupAlgebraIndex G)
101 (x : PrimePowerCompletedCoeff ℓ G) :
102 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (-x) =
103 -primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x := by
104 change (show ZMod (ℓ ^ i.1) from (-x).1 i) =
105 -(show ZMod (ℓ ^ i.1) from x.1 i)
106 rfl
108omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
109/-- The prime-power coefficient projection preserves subtraction. -/
110@[simp]
111theorem primePowerCompletedCoeffProjection_sub
112 (i : PrimePowerCompletedGroupAlgebraIndex G)
113 (x y : PrimePowerCompletedCoeff ℓ G) :
114 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i (x - y) =
115 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i x -
116 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) i y := by
117 change (show ZMod (ℓ ^ i.1) from (x - y).1 i) =
118 (show ZMod (ℓ ^ i.1) from x.1 i) - (show ZMod (ℓ ^ i.1) from y.1 i)
119 rfl
121omit [Fact (0 < ℓ)] [IsTopologicalGroup G] in
122/--
123Coefficient projections with the same prime-power exponent do not depend on the finite-quotient
124component of the group-algebra index. The second index component synchronizes coefficients and
125group-algebra stages in one inverse system.
126-/
127theorem primePowerCompletedCoeffProjection_eq_of_same_exponent
128 (a : ℕ) (U V : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G)
129 (z : PrimePowerCompletedCoeff ℓ G) :
130 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
131 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z := by
132 let T : _root_.CompletedGroupAlgebra.CompletedGroupAlgebraIndex G :=
133 _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex G
134 let hTU : (a, T) ≤ (a, U) :=
135 ⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) U⟩
136 let hTV : (a, T) ≤ (a, V) :=
137 ⟨le_rfl, _root_.CompletedGroupAlgebra.terminalCompletedGroupAlgebraIndex_le (G := G) V⟩
138 have hTU_coeff :
139 modNCompletedCoeffMap
140 (n := ℓ ^ a) (m := ℓ ^ a)
141 (primePow_dvd_primePow (ℓ := ℓ) hTU.1) = RingHom.id _ := by
142 have hproof :
143 primePow_dvd_primePow (ℓ := ℓ) hTU.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
144 Subsingleton.elim _ _
145 rw [hproof]
146 exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
147 have hTV_coeff :
148 modNCompletedCoeffMap
149 (n := ℓ ^ a) (m := ℓ ^ a)
150 (primePow_dvd_primePow (ℓ := ℓ) hTV.1) = RingHom.id _ := by
151 have hproof :
152 primePow_dvd_primePow (ℓ := ℓ) hTV.1 = (dvd_rfl : ℓ ^ a ∣ ℓ ^ a) :=
153 Subsingleton.elim _ _
154 rw [hproof]
155 exact modNCompletedCoeffMap_rfl (n := ℓ ^ a)
156 have hU := z.2 (a, T) (a, U) hTU
157 have hV := z.2 (a, T) (a, V) hTV
158 have hU' :
159 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, U) z =
160 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
161 simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTU_coeff] using
162 hU
163 have hV' :
164 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, V) z =
165 primePowerCompletedCoeffProjection (ℓ := ℓ) (G := G) (a, T) z := by
166 simpa [primePowerCompletedCoeffProjection, primePowerCompletedCoeffSystem, hTV_coeff] using
167 hV
168 exact hU'.trans hV'.symm
170end
172end FoxDifferential