Source: ProCGroups.CrowellExactSequence.Profinite.MainTheorem
1import ProCGroups.CrowellExactSequence.Profinite.BlanchfieldLyndon
3/-!
4# Crowell Exact Sequence / Profinite / Main Theorem
6This module packages the separated completed Crowell and
7Blanchfield--Lyndon sequences as `FourTermLinearSequence` values and states
8their exactness theorems under the required formation hypotheses.
9-/
11namespace CrowellExactSequence
13noncomputable section
15open FoxDifferential
16open ProCGroups.ProC
18universe u
20variable {H : Type u} [Group H] [TopologicalSpace H] [IsTopologicalGroup H]
21variable {C : ProCGroups.FiniteGroupClass.{u}}
25/-- The separated completed Crowell sequence over pro-`C` integer coefficients. The additive
26head map and the completed augmentation are viewed canonically as `ℤ`-linear maps. -/
27def profiniteSeparatedCrowellLinearSequence
28 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
30 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
31 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
32 (psi : ContinuousMonoidHom sourceData.carrier H)
33 (hpsi : Function.Surjective psi) :
34 FourTermLinearSequence ℤ
35 (ProfiniteKernelAbelianizationAdd psi)
36 (ZCSeparatedCompletedDifferentialModule
37 C psi.toMonoidHom)
38 (ZCCompletedGroupAlgebra C H)
39 (ZCCoeff C) := by
40 refine FourTermLinearSequence.ofExact
41 ((profiniteKernelAbelianizationBoundaryAddProCIntegerSep
42 (G := sourceData.carrier) (H := H)
43 C psi).toIntLinearMap)
44 ((presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
45 (G := sourceData.carrier) (H := H) C
46 hC.hereditary
47 psi).toAddMonoidHom.toIntLinearMap)
48 ((zcCompletedGroupAlgebraAugmentation
49 C H).toAddMonoidHom.toIntLinearMap) ?_
50 rcases
51 freeProC_presentedSepCrowellZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
52 (H := H) (C := C) hC sourceData hbasis psi hpsi with
53 ⟨hinjective, hexactHead, hexactTail, hsurjective⟩
54 refine ⟨hinjective, hexactHead, ?_, ?_⟩
55 · change Function.Exact
56 (presentedSeparatedDifferentialToCompletedGroupAlgebraProCInteger
57 (G := sourceData.carrier) (H := H) C hC.hereditary psi)
58 (zcCompletedGroupAlgebraAugmentation C H)
59 exact hexactTail
60 · change Function.Surjective (zcCompletedGroupAlgebraAugmentation C H)
61 exact hsurjective
63/--
64The separated completed Crowell exact sequence over pro-\(C\) integer coefficients, packaged as
65the full four-term exact sequence \(N^{\mathrm{ab}}(C)\) \(\to\) \(A_{\psi}(C)\) \(\to\)
66\(\mathbb{Z}_C\llbracket H\rrbracket\) \(\to\) \(\mathbb{Z}_C\).
67-/
68@[simp]
69theorem profiniteSeparatedCrowellLinearSequence_isExact
70 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
72 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
73 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
74 (psi : ContinuousMonoidHom sourceData.carrier H)
75 (hpsi : Function.Surjective psi) :
76 (profiniteSeparatedCrowellLinearSequence
77 (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact := by
78 simp only [profiniteSeparatedCrowellLinearSequence,
79 FourTermLinearSequence.ofExact_isExact]
81/-- The separated Blanchfield--Lyndon head map in the universe-lifted coordinates, bundled as
82an integer-linear map. -/
83def profiniteSeparatedBlanchfieldLyndonBoundaryLinear
84 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
86 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
87 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
88 (psi : ContinuousMonoidHom sourceData.carrier H)
89 (hpsi : Function.Surjective psi) :
90 ProfiniteKernelAbelianizationAdd psi →ₗ[ℤ]
91 ZCFreeFoxCoordinates C
92 (X := ULift.{u} (Fin r)) (H := H) :=
93 ((freeProCChosenULift_sepCoordinateEquiv
94 (H := H) (C := C) hC sourceData hbasis psi hpsi).toLinearMap.toAddMonoidHom.comp
95 (profiniteKernelAbelianizationBoundaryAddProCIntegerSep
96 (G := sourceData.carrier) (H := H)
97 C psi)).toIntLinearMap
99/-- The canonical separated Blanchfield--Lyndon sequence in the universe-lifted coordinate
100basis. -/
101def profiniteSeparatedBlanchfieldLyndonLinearSequence
102 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
104 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
105 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
106 (psi : ContinuousMonoidHom sourceData.carrier H)
107 (hpsi : Function.Surjective psi) :
108 FourTermLinearSequence ℤ
109 (ProfiniteKernelAbelianizationAdd psi)
110 (ZCFreeFoxCoordinates C
111 (X := ULift.{u} (Fin r)) (H := H))
112 (ZCCompletedGroupAlgebra C H)
113 (ZCCoeff C) := by
114 refine FourTermLinearSequence.ofExact
115 (profiniteSeparatedBlanchfieldLyndonBoundaryLinear
116 (H := H) (C := C) hC sourceData hbasis psi hpsi)
117 ((blanchfieldLyndonFiniteFamilyMap
118 (R := ZCCompletedGroupAlgebra C H)
119 (fun i : ULift.{u} (Fin r) =>
120 presentedCompletedDifferentialBoundaryProCInteger
121 (G := sourceData.carrier) (H := H) C psi
122 ((freeProCChosenULiftFamilyOfBasisCard
123 (C := C) sourceData hbasis) i))).toAddMonoidHom.toIntLinearMap)
124 ((zcCompletedGroupAlgebraAugmentation
125 C H).toAddMonoidHom.toIntLinearMap) ?_
126 rcases
127 freeProC_presentedSepBLZC_of_continuousMagnus_zcBiAllStages_of_psi_surj
128 (H := H) (C := C) hC sourceData hbasis psi hpsi with
129 ⟨hinjective, hexactHead, hexactTail, hsurjective⟩
130 refine ⟨?_, ?_, ?_, ?_⟩
131 · change Function.Injective
132 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
133 (H := H) (C := C) hC sourceData hbasis psi hpsi)
134 exact hinjective
135 · change Function.Exact
136 (freeProCSeparatedBlanchfieldLyndonBoundaryProCInteger
137 (H := H) (C := C) hC sourceData hbasis psi hpsi)
138 (blanchfieldLyndonFiniteFamilyMap
139 (R := ZCCompletedGroupAlgebra C H)
140 (fun i : ULift.{u} (Fin r) =>
141 presentedCompletedDifferentialBoundaryProCInteger
142 (G := sourceData.carrier) (H := H) C psi
143 ((freeProCChosenULiftFamilyOfBasisCard
144 (C := C) sourceData hbasis) i)))
145 exact hexactHead
146 · change Function.Exact
147 (blanchfieldLyndonFiniteFamilyMap
148 (R := ZCCompletedGroupAlgebra C H)
149 (fun i : ULift.{u} (Fin r) =>
150 presentedCompletedDifferentialBoundaryProCInteger
151 (G := sourceData.carrier) (H := H) C psi
152 ((freeProCChosenULiftFamilyOfBasisCard
153 (C := C) sourceData hbasis) i)))
154 (zcCompletedGroupAlgebraAugmentation C H)
155 exact hexactTail
156 · change Function.Surjective (zcCompletedGroupAlgebraAugmentation C H)
157 exact hsurjective
159/--
160The separated completed Blanchfield--Lyndon exact sequence in the universe-lifted finite
161coordinate basis, packaged as the full four-term exact sequence.
162-/
163@[simp]
164theorem profiniteSeparatedBlanchfieldLyndonLinearSequence_isExact
165 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
167 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
168 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
169 (psi : ContinuousMonoidHom sourceData.carrier H)
170 (hpsi : Function.Surjective psi) :
171 (profiniteSeparatedBlanchfieldLyndonLinearSequence
172 (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact := by
173 simp only [profiniteSeparatedBlanchfieldLyndonLinearSequence,
174 FourTermLinearSequence.ofExact_isExact]
176/-- The integer-linear coordinate equivalence from concrete `Fin r` coordinates to the
177universe-lifted coordinates used by the epimorphic generated-target lifting property. -/
178def finULiftCompletedGroupAlgebraCoordinateLinearEquiv (r : Nat) :
179 (Fin r → ZCCompletedGroupAlgebra C H) ≃ₗ[ℤ]
180 (ULift.{u} (Fin r) → ZCCompletedGroupAlgebra C H) :=
181 (piReindexLinearEquiv
182 (R := ZCCompletedGroupAlgebra C H)
183 (finULiftEquiv r)).toAddEquiv.toIntLinearEquiv
185/-- The canonical concrete-coordinate BL sequence, obtained by reindexing the bundled
186universe-lifted sequence once at sequence level. -/
187def profiniteSeparatedBlanchfieldLyndonFinLinearSequence
188 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
190 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
191 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
192 (psi : ContinuousMonoidHom sourceData.carrier H)
193 (hpsi : Function.Surjective psi) :
194 FourTermLinearSequence ℤ
195 (ProfiniteKernelAbelianizationAdd psi)
196 (Fin r → ZCCompletedGroupAlgebra C H)
197 (ZCCompletedGroupAlgebra C H)
198 (ZCCoeff C) :=
199 (profiniteSeparatedBlanchfieldLyndonLinearSequence
200 (H := H) (C := C) hC sourceData hbasis psi hpsi).reindexMiddle
201 (finULiftCompletedGroupAlgebraCoordinateLinearEquiv
202 (H := H) (C := C) r)
204/--
205The separated completed Blanchfield--Lyndon exact sequence in the concrete \(\operatorname{Fin}
206r\) coordinate basis, packaged as the full four-term exact sequence.
207-/
208@[simp]
209theorem profiniteSeparatedBlanchfieldLyndonFinLinearSequence_isExact
210 [CompactSpace H] [T2Space H] [TotallyDisconnectedSpace H]
212 (sourceData : ProCGroups.FreeProC.EpimorphicallyFreeProCGroupOnConvergingSetData.{u, u} C)
213 {r : Nat} (hbasis : Cardinal.mk sourceData.basis = r)
214 (psi : ContinuousMonoidHom sourceData.carrier H)
215 (hpsi : Function.Surjective psi) :
216 (profiniteSeparatedBlanchfieldLyndonFinLinearSequence
217 (H := H) (C := C) hC sourceData hbasis psi hpsi).IsExact :=
218 FourTermLinearSequence.reindexMiddle_isExact
219 (profiniteSeparatedBlanchfieldLyndonLinearSequence
220 (H := H) (C := C) hC sourceData hbasis psi hpsi)
221 (finULiftCompletedGroupAlgebraCoordinateLinearEquiv
222 (H := H) (C := C) r)
223 (profiniteSeparatedBlanchfieldLyndonLinearSequence_isExact
224 (H := H) (C := C) hC sourceData hbasis psi hpsi)
226end
228end CrowellExactSequence