Source: ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Limit
1import ProCGroups.FoxDifferential.Completed.DifferentialModule.Map.Stage
3/-!
4# Fox differential: completed — differential module — map — limit
6The principal declarations in this module are:
8- `primePowerCompletedGroupAlgebraMap`
9 The ring homomorphism on prime-power completed group algebras induced stagewise by a continuous
10 group homomorphism.
11- `primePowerCompletedGroupAlgebraProjection_map`
12 The finite-stage Fox-differential projection is computed by the prime-power completed
13 group-algebra projection formula.
14- `continuous_primePowerCompletedGroupAlgebraMap`
15 The completed group-algebra map induced by a continuous homomorphism is continuous for the
16 inverse-limit topologies.
17-/
19namespace FoxDifferential
21noncomputable section
23open ProCGroups
24open ProCGroups.ProC
26universe u v
28variable (ℓ : ℕ)
29variable {G : Type u} [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
30variable {H : Type v} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
32/--
33The ring homomorphism on prime-power completed group algebras induced stagewise by a continuous
34group homomorphism.
35-/
36def primePowerCompletedGroupAlgebraMap
37 (ψ : ContinuousMonoidHom G H) :
38 PrimePowerCompletedGroupAlgebra ℓ G →+* PrimePowerCompletedGroupAlgebra ℓ H where
39 toFun x := ⟨fun i =>
40 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
41 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
42 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x), by
43 intro i j hij
44 let hsource :
45 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) ≤
46 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) :=
47 ⟨hij.1, completedGroupAlgebraComapIndex_mono (G := G) (H := H) ψ hij.2⟩
48 have hx := x.2
49 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
50 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2)
51 hsource
52 change
53 primePowerCompletedGroupAlgebraTransition (ℓ := ℓ) (G := G) hsource
54 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
55 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x) =
56 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
57 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x at hx
58 have hcompat := congrFun
59 (congrArg DFunLike.coe
60 (primePowerCompletedGroupAlgebraMapStage_compatible
61 (ℓ := ℓ) (G := G) (H := H) ψ hij))
62 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
63 (j.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ j.2) x)
64 rw [RingHom.comp_apply, RingHom.comp_apply] at hcompat
65 rw [hx] at hcompat
66 simpa [primePowerCompletedGroupAlgebraSystem] using hcompat⟩
67 map_one' := by
68 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
69 intro i
70 change
71 primePowerCompletedGroupAlgebraMapStage
72 (ℓ := ℓ) (G := G) (H := H) ψ i 1 = 1
73 exact map_one _
74 map_mul' := by
75 intro x y
76 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
77 intro i
78 change
79 primePowerCompletedGroupAlgebraMapStage
80 (ℓ := ℓ) (G := G) (H := H) ψ i
81 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
82 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x *
83 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
84 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y) =
85 primePowerCompletedGroupAlgebraMapStage
86 (ℓ := ℓ) (G := G) (H := H) ψ i
87 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
88 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) *
89 primePowerCompletedGroupAlgebraMapStage
90 (ℓ := ℓ) (G := G) (H := H) ψ i
91 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
92 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y)
93 exact map_mul _ _ _
94 map_zero' := by
95 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
96 intro i
97 change
98 primePowerCompletedGroupAlgebraMapStage
99 (ℓ := ℓ) (G := G) (H := H) ψ i 0 = 0
100 exact map_zero _
101 map_add' := by
102 intro x y
103 apply (primePowerCompletedGroupAlgebraSystem ℓ H).ext
104 intro i
105 change
106 primePowerCompletedGroupAlgebraMapStage
107 (ℓ := ℓ) (G := G) (H := H) ψ i
108 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
109 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x +
110 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
111 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y) =
112 primePowerCompletedGroupAlgebraMapStage
113 (ℓ := ℓ) (G := G) (H := H) ψ i
114 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
115 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) +
116 primePowerCompletedGroupAlgebraMapStage
117 (ℓ := ℓ) (G := G) (H := H) ψ i
118 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
119 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) y)
120 exact map_add _ _ _
122/--
123The finite-stage Fox-differential projection is computed by the prime-power completed
124group-algebra projection formula.
125-/
126@[simp]
127theorem primePowerCompletedGroupAlgebraProjection_map
128 (ψ : ContinuousMonoidHom G H) (i : PrimePowerCompletedGroupAlgebraIndex H)
129 (x : PrimePowerCompletedGroupAlgebra ℓ G) :
130 primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := H) i
131 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x) =
132 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
133 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G)
134 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2) x) := rfl
137/--
138The completed group-algebra map induced by a continuous homomorphism is continuous for the
139inverse-limit topologies.
140-/
141theorem continuous_primePowerCompletedGroupAlgebraMap
142 (ψ : ContinuousMonoidHom G H) :
143 Continuous (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ) := by
144 let S := primePowerCompletedGroupAlgebraSystem ℓ H
145 let T := primePowerCompletedGroupAlgebraSystem ℓ G
146 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex H, TopologicalSpace (S.X i) :=
147 fun i => S.topologicalSpace i
148 letI : ∀ i : PrimePowerCompletedGroupAlgebraIndex G, TopologicalSpace (T.X i) :=
149 fun i => T.topologicalSpace i
150 refine Continuous.subtype_mk (continuous_pi fun i => ?_) (fun x =>
151 (primePowerCompletedGroupAlgebraMap (ℓ := ℓ) (G := G) (H := H) ψ x).2)
152 let sourceIndex : PrimePowerCompletedGroupAlgebraIndex G :=
153 (i.1, completedGroupAlgebraComapIndex (G := G) (H := H) ψ i.2)
154 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ G sourceIndex) :=
155 T.topologicalSpace sourceIndex
156 letI : DiscreteTopology (PrimePowerCompletedGroupAlgebraStage ℓ G sourceIndex) := ⟨rfl⟩
157 letI : TopologicalSpace (PrimePowerCompletedGroupAlgebraStage ℓ H i) :=
158 S.topologicalSpace i
159 have hstage :
160 Continuous
161 (primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i) :=
162 continuous_of_discreteTopology
163 change Continuous (fun x : PrimePowerCompletedGroupAlgebra ℓ G =>
164 primePowerCompletedGroupAlgebraMapStage (ℓ := ℓ) (G := G) (H := H) ψ i
165 (primePowerCompletedGroupAlgebraProjection (ℓ := ℓ) (G := G) sourceIndex x))
166 exact hstage.comp (T.continuous_projection sourceIndex)
168end
170end FoxDifferential