Source: ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.Projection
1import ProCGroups.FoxDifferential.Completed.CoefficientRings.CompletedGroupAlgebraPrimePower.System.Ring.GroupLike
3/-!
4# Fox differential: prime-power completed group algebra — system — ring — projection
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraProjection_natCast`
9 The finite-stage projection preserves natural number casts.
10- `primePowerCompletedGroupAlgebraProjection_intCast`
11 The finite-stage projection preserves integer casts.
12- `primePowerCompletedGroupAlgebraProjection_zero`
13 The finite-stage projection sends \(0\) to \(0\).
14- `primePowerCompletedGroupAlgebraProjection_add`
15 The prime-power finite-stage projection preserves addition.
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 < ℓ)] in
31/-- The finite-stage projection preserves natural number casts. -/
32@[simp]
33theorem primePowerCompletedGroupAlgebraProjection_natCast
34 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℕ) :
35 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
36 (n : PrimePowerCompletedGroupAlgebra ℓ G) = n := by
37 change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
38 rfl
40omit [Fact (0 < ℓ)] in
41/-- The finite-stage projection preserves integer casts. -/
42@[simp]
43theorem primePowerCompletedGroupAlgebraProjection_intCast
44 (i : PrimePowerCompletedGroupAlgebraIndex G) (n : ℤ) :
45 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
46 (n : PrimePowerCompletedGroupAlgebra ℓ G) = n := by
47 change (n : PrimePowerCompletedGroupAlgebraStage ℓ G i) = n
48 rfl
50omit [Fact (0 < ℓ)] in
51/-- The finite-stage projection sends \(0\) to \(0\). -/
52@[simp]
53theorem primePowerCompletedGroupAlgebraProjection_zero
54 (i : PrimePowerCompletedGroupAlgebraIndex G) :
55 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i
56 (0 : PrimePowerCompletedGroupAlgebra ℓ G) = 0 := by
57 change (0 : PrimePowerCompletedGroupAlgebraStage ℓ G i) = 0
58 rfl
60omit [Fact (0 < ℓ)] in
61/-- The prime-power finite-stage projection preserves addition. -/
62@[simp]
63theorem primePowerCompletedGroupAlgebraProjection_add
64 (i : PrimePowerCompletedGroupAlgebraIndex G)
65 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
66 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x + y) =
67 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x +
68 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
69 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x + y).1 i) =
70 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) +
71 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
72 rfl
74omit [Fact (0 < ℓ)] in
75/-- The prime-power finite-stage projection preserves negation. -/
76@[simp]
77theorem primePowerCompletedGroupAlgebraProjection_neg
78 (i : PrimePowerCompletedGroupAlgebraIndex G)
79 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
80 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (-x) =
81 -primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x := by
82 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (-x).1 i) =
83 -(show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i)
84 rfl
86omit [Fact (0 < ℓ)] in
87/-- The prime-power finite-stage projection preserves subtraction. -/
88@[simp]
89theorem primePowerCompletedGroupAlgebraProjection_sub
90 (i : PrimePowerCompletedGroupAlgebraIndex G)
91 (x y : PrimePowerCompletedGroupAlgebra ℓ G) :
92 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i (x - y) =
93 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i x -
94 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) i y := by
95 change (show PrimePowerCompletedGroupAlgebraStage ℓ G i from (x - y).1 i) =
96 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from x.1 i) -
97 (show PrimePowerCompletedGroupAlgebraStage ℓ G i from y.1 i)
98 rfl
100omit [Fact (0 < ℓ)] in
101/--
102Finite-stage prime-power augmentation is compatible with transition maps and coefficient
103reduction.
104-/
105@[simp]
106theorem primePowerCompletedGroupAlgebraStageAugmentation_comp_transition
107 {i j : PrimePowerCompletedGroupAlgebraIndex G} (hij : i ≤ j) :
108 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ i.1) G i.2).comp
109 (primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hij) =
110 (modNCompletedCoeffMap
111 (n := ℓ ^ i.1) (m := ℓ ^ j.1)
112 (primePow_dvd_primePow (ℓ := ℓ) hij.1)).comp
113 (modNCompletedGroupAlgebraStageAugmentation (ℓ ^ j.1) G j.2) := by
114 rw [primePowerCompletedGroupAlgebraTransition_eq]
115 rw [← RingHom.comp_assoc]
116 rw [modNCompletedGroupAlgebraStageAugmentation_comp_coeffMap]
117 rw [RingHom.comp_assoc]
118 rw [modNCompletedGroupAlgebraStageAugmentation_compatible]
120end
122end FoxDifferential