Yamaguchi Lean 4 Library
Source: ProCGroups.CrowellExactSequence.Profinite.Exactness
ProCGroups/CrowellExactSequence/Profinite/Exactness/Source

Source: ProCGroups.CrowellExactSequence.Profinite.Exactness

1import ProCGroups.CrowellExactSequence.Profinite.KernelInjectivity
2import ProCGroups.CrowellExactSequence.Profinite.SequenceMaps
3import ProCGroups.FoxDifferential.Completed.Continuous.ClosedGeneratedCoordinates.Comparison
5/-!
6# Profinite Crowell middle exactness
8This file reduces exactness at the separated completed differential module to integration of
9coordinate cycles. It derives the middle image/kernel equality from finite-stage lifts and proves
10the required boundary vanishing under the closed-generator graph hypothesis.
11-/
13namespace CrowellExactSequence
15noncomputable section
17open FoxDifferential
18open ProCGroups.ProC
19open ProCGroups.Completion
20open ProCGroups.InverseSystems
22universe u v
24variable {G H : Type u}
25variable [Group G] [TopologicalSpace G] [IsTopologicalGroup G]
26variable [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
28/-- The separated displayed boundary kills the separated kernel boundary. -/
29theorem presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
30 (C : ProCGroups.FiniteGroupClass.{u})
32 (psi : ContinuousMonoidHom G H)
33 (x : ProfiniteKernelAbelianizationAdd psi) :
34 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
35 (G := G) (H := H) C hC psi
36 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
37 (G := G) (H := H) C psi x) =
38 0 := by
39 change
40 (fun y : ProfiniteKernelAbelianization psi =>
41 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
42 (G := G) (H := H) C hC psi
43 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
44 (G := G) (H := H) C psi (Additive.ofMul y)) =
45 0) (Additive.toMul x)
46 refine QuotientGroup.induction_on (Additive.toMul x) ?_
47 intro n
48 change
49 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
50 (G := G) (H := H) C hC psi
51 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
52 (G := G) (H := H) C psi
53 (Additive.ofMul
54 (QuotientGroup.mk'
55 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
56 0
57 rw [profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of,
58 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_d]
59 exact zcCompletedGroupAlgebraBoundary_eq_zero_of_mem_ker
60 (C := C) (H := H) psi.toMonoidHom n.2
62/--
63Exactness of the separated additive boundary is equivalent to integrability of all separated
64delta cycles.
65-/
66theorem exact_boundaryAddZC_sep_iff_delta_cycles_integrate
67 {C : ProCGroups.FiniteGroupClass.{u}}
69 {psi : ContinuousMonoidHom G H} :
70 Function.Exact
71 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
72 (G := G) (H := H) C psi)
73 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
74 (G := G) (H := H) C hC psi) ↔
75 ∀ a : ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom,
76 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
77 (G := G) (H := H) C hC psi a = 0 →
78 ∃ n : ProfiniteKernelSubgroup psi,
79 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a := by
80 let dN :=
81 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
82 (G := G) (H := H) C psi
83 let delta :=
84 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
85 (G := G) (H := H) C hC psi
86 constructor
87 · intro hexact a ha
88 rcases (hexact a).1 ha with ⟨x, hx⟩
89 revert hx
90 change
91 (fun q : ProfiniteKernelAbelianization psi =>
92 dN (Additive.ofMul q) = a →
93 ∃ n : ProfiniteKernelSubgroup psi,
94 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 = a) (Additive.toMul x)
95 refine QuotientGroup.induction_on (Additive.toMul x) ?_
96 intro n hn
97 refine ⟨n, ?_⟩
98 calc
99 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 =
100 dN
101 (Additive.ofMul
102 (QuotientGroup.mk'
103 (Subgroup.topologicalClosure
104 (commutator (ProfiniteKernelSubgroup psi))) n)) :=
105 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
106 (G := G) (H := H) C psi n).symm
107 _ = a := hn
108 · intro hintegrates a
109 constructor
110 · intro ha
111 rcases hintegrates a ha with ⟨n, hn⟩
112 refine ⟨Additive.ofMul
113 (QuotientGroup.mk'
114 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
115 calc
116 dN
117 (Additive.ofMul
118 (QuotientGroup.mk'
119 (Subgroup.topologicalClosure
120 (commutator (ProfiniteKernelSubgroup psi))) n)) =
121 zcSeparatedUniversalDifferential C psi.toMonoidHom n.1 :=
122 profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of
123 (G := G) (H := H) C psi n
124 _ = a := hn
125 · rintro ⟨x, hx⟩
126 rw [← hx]
127 exact
128 presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
129 (G := G) (H := H) C hC psi x
131/--
132A coordinate lift for each cycle gives exactness of the separated additive boundary sequence.
133-/
134theorem exact_boundaryAddZC_sep_of_coord_cycle_lift
135 (C : ProCGroups.FiniteGroupClass.{u})
137 (psi : ContinuousMonoidHom G H)
138 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
139 (coords :
140 ZCSeparatedCompletedDifferentialModule C psi.toMonoidHom ≃ₗ[
141 ZCCompletedGroupAlgebra C H]
142 ZCFreeFoxCoordinates C (X := X) (H := H))
143 (hcoords_symm :
144 coords.symm.toLinearMap =
145 presentedSeparatedDifferentialFamilyMapProCInteger
146 (G := G) (H := H) C psi family)
147 (Dcoords : G → ZCFreeFoxCoordinates C (X := X) (H := H))
148 (hDcoords_kernel :
149 ∀ n : ProfiniteKernelSubgroup psi,
150 Dcoords n.1 =
151 coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1))
152 (hcycle_lift :
153 ∀ v : ZCFreeFoxCoordinates C (X := X) (H := H),
154 blanchfieldLyndonFiniteFamilyMap
155 (R := ZCCompletedGroupAlgebra C H)
156 (fun i : X =>
157 presentedCompletedDifferentialBoundaryProCInteger
158 (G := G) (H := H) C psi (family i)) v = 0 →
159 ∃ n : ProfiniteKernelSubgroup psi, Dcoords n.1 = v) :
160 Function.Exact
161 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
162 (G := G) (H := H) C psi)
163 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
164 (G := G) (H := H) C hC psi) := by
165 let dN :=
166 profiniteKernelAbelianizationBoundaryAddProCIntegerSep
167 (G := G) (H := H) C psi
168 let delta :=
169 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
170 (G := G) (H := H) C hC psi
171 let blDelta :=
172 blanchfieldLyndonFiniteFamilyMap
173 (R := ZCCompletedGroupAlgebra C H)
174 (fun i : X =>
175 presentedCompletedDifferentialBoundaryProCInteger
176 (G := G) (H := H) C psi (family i))
177 have hblDelta_comp : delta.comp coords.symm.toLinearMap = blDelta := by
178 rw [hcoords_symm]
179 exact
180 presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger_comp_familyMap
181 (G := G) (H := H) C hC psi family
182 have hblDelta_apply (y) : blDelta y = delta (coords.symm y) := by
183 have h := congrArg (fun f => f y) hblDelta_comp
184 change delta (coords.symm y) = blDelta y at h
185 exact h.symm
186 change Function.Exact dN delta
187 intro a
188 constructor
189 · intro ha
190 have hcoord_cycle : blDelta (coords a) = 0 := by
191 calc
192 blDelta (coords a) = delta (coords.symm (coords a)) := hblDelta_apply (coords a)
193 _ = delta a := by rw [coords.symm_apply_apply]
194 _ = 0 := ha
195 rcases hcycle_lift (coords a) hcoord_cycle with ⟨n, hncoords⟩
196 refine ⟨Additive.ofMul
197 (QuotientGroup.mk'
198 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n), ?_⟩
199 apply coords.injective
200 calc
201 coords
202 (dN (Additive.ofMul
203 (QuotientGroup.mk'
204 (Subgroup.topologicalClosure (commutator (ProfiniteKernelSubgroup psi))) n))) =
205 coords (zcSeparatedUniversalDifferential C psi.toMonoidHom n.1) := by
206 rw [profiniteKernelAbelianizationBoundaryAddProCIntegerSep_of]
207 _ = Dcoords n.1 := (hDcoords_kernel n).symm
208 _ = coords a := hncoords
209 · rintro ⟨x, hx⟩
210 rw [← hx]
211 exact
212 presentedSepToZC_profiniteKernelAbelianizationBoundaryAddSep
213 (G := G) (H := H) C hC psi x
215/--
216Agreement of the closed-generated Magnus coordinates with the presented differential
217coordinates forces the completed kernel boundary to kill the closed commutator subgroup.
218-/
219theorem completedBoundaryKillsTopCommZC_of_closedGen_leftGraph
220 [CompactSpace G] [T2Space G] [TotallyDisconnectedSpace G]
221 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
222 (C : ProCGroups.FiniteGroupClass.{u}) (psi : ContinuousMonoidHom G H)
223 {X : Type u} [Fintype X] [DecidableEq X] (family : X → G)
224 [T1Space (ZCFreeFoxCoordinates C (X := X) (H := H))]
225 (hbasis_A :
226 IsPresentedCompletedDifferentialFamilyBasisProCInteger
227 (G := G) (H := H) C psi family)
228 (hfree :
230 (C := C) X G family)
231 (htarget :
232 HasOpenNormalBasisInClass C
233 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
234 (C := C) (fun i : X => psi (family i)) : Subgroup
235 (ZCCompletedFoxSemidirect C X H)))
236 (hφconv :
238 (G :=
239 (freeProCZCCompletedFoxSemidirectClosedGeneratedTarget
240 (C := C) (fun i : X => psi (family i)) : Subgroup
241 (ZCCompletedFoxSemidirect C X H)))
242 (freeProCZCCompletedFoxSemidirectClosedGeneratedGenerator
243 (C := C) (fun i : X => psi (family i))))
244 (hleft_graph_eq :
245 ∀ g : G,
246 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
247 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g =
248 presentedCompletedDifferentialFamilyCoordinatesProCInteger
249 (G := G) (H := H) C psi family hbasis_A
250 (zcUniversalDifferential C psi.toMonoidHom g)) :
251 CompletedBoundaryKillsTopologicalCommutatorProCInteger
252 (G := G) (H := H) C psi := by
253 let Dclosed : G → ZCFreeFoxCoordinates C (X := X) (H := H) :=
254 fun g =>
255 freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
256 (C := C) hfree (fun i : X => psi (family i)) htarget hφconv g
257 refine
258 completedBoundaryKillsTopCommZC_of_continuous_ambient_familyCoords_fintype
259 (G := G) (H := H) C psi family hbasis_A Dclosed ?_ ?_
260 · simpa [Dclosed] using
261 continuous_freeProCZCCompletedFoxDerivativeVectorViaClosedGenerated
262 (C := C) X H hfree (fun i : X => psi (family i)) htarget hφconv
263 · intro n
264 exact hleft_graph_eq n.1
266end
268end CrowellExactSequence