Source: ProCGroups.CrowellExactSequence.Basic
1import ProCGroups.FoxDifferential.Common.FiniteFamilyLinearMap
2import Mathlib.Topology.Basic
4/-!
5# `ProCGroups.CrowellExactSequence.Basic`
7Crowell exact sequences / Basic.
9This module contains the common four-term linear-sequence interface, exactness transport
10lemmas, and the finite Blanchfield--Lyndon coordinate map used by the discrete and profinite
11theories.
12-/
14namespace CrowellExactSequence
16noncomputable section
18open scoped BigOperators
19open FoxDifferential
21section BlanchfieldLyndonFiniteFamilyMap
23variable {R : Type*} [Semiring R]
24variable {M : Type*} [AddCommMonoid M] [Module R M]
25variable {X : Type*} [Fintype X] [DecidableEq X]
27/-- The Blanchfield--Lyndon finite-family map associated to a chosen boundary-generating family. -/
28abbrev blanchfieldLyndonFiniteFamilyMap (generators : X → M) :
29 (X → R) →ₗ[R] M :=
30 finiteFamilyLinearMap (R := R) generators
32omit [DecidableEq X] in
33/--
34The Blanchfield--Lyndon finite-family boundary map is evaluated on the canonical generators and
35then extended linearly to the coordinate module.
36-/
37theorem blanchfieldLyndonFiniteFamilyMap_apply (generators : X → M) (x : X → R) :
38 blanchfieldLyndonFiniteFamilyMap (R := R) generators x = ∑ i, x i • generators i := rfl
40/-- A Blanchfield--Lyndon finite-family map sends a coordinate basis vector to its generator. -/
41@[simp]
42theorem blanchfieldLyndonFiniteFamilyMap_single (generators : X → M) (i : X) :
43 blanchfieldLyndonFiniteFamilyMap (R := R) generators (Pi.single i 1) = generators i :=
44 finiteFamilyLinearMap_single (R := R) generators i
46end BlanchfieldLyndonFiniteFamilyMap
48/-- A bundled four-term sequence of linear maps. It records the three morphisms and both
49consecutive-composition equations together.
50Exactness is imposed separately by `FourTermLinearSequence.IsExact`, so the same sequence can be
51constructed before its exactness proof is available. -/
52structure FourTermLinearSequence (R : Type*) [Semiring R]
53 (A B C D : Type*)
54 [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
55 [Module R A] [Module R B] [Module R C] [Module R D] where
56 /-- The first linear map, from \(A\) to \(B\). -/
57 head : A →ₗ[R] B
58 /-- The middle linear map, from \(B\) to \(C\). -/
59 middle : B →ₗ[R] C
60 /-- The final linear map, from \(C\) to \(D\). -/
61 tail : C →ₗ[R] D
62 /-- The middle map vanishes after the head map. -/
63 middle_comp_head : middle.comp head = 0
64 /-- The tail map vanishes after the middle map. -/
65 tail_comp_middle : tail.comp middle = 0
67namespace FourTermLinearSequence
69variable {R A B C D : Type*} [Semiring R]
70variable [AddCommMonoid A] [AddCommMonoid B] [AddCommMonoid C] [AddCommMonoid D]
71variable [Module R A] [Module R B] [Module R C] [Module R D]
73/--
74A four-term exact sequence, formulated at the function level. This packages injectivity of
75\(f\), exactness at the two middle terms, and surjectivity of the final map.
76-/
77def IsExact (S : FourTermLinearSequence R A B C D) : Prop :=
78 Function.Injective S.head ∧ Function.Exact S.head S.middle ∧
79 Function.Exact S.middle S.tail ∧ Function.Surjective S.tail
82/-- Bundle three linear maps once their four exactness assertions are known. -/
83def ofExact (f : A →ₗ[R] B) (g : B →ₗ[R] C) (h : C →ₗ[R] D)
84 (hexact : Function.Injective f ∧ Function.Exact f g ∧
85 Function.Exact g h ∧ Function.Surjective h) :
86 FourTermLinearSequence R A B C D where
87 head := f
88 middle := g
89 tail := h
90 middle_comp_head := by
91 ext x
92 have hx : g (f x) = 0 := (hexact.2.1 (f x)).2 ⟨x, rfl⟩
93 simpa using hx
94 tail_comp_middle := by
95 ext x
96 have hx : h (g x) = 0 := (hexact.2.2.1 (g x)).2 ⟨x, rfl⟩
97 simpa using hx
99/-- The sequence assembled from exact maps retains the supplied injectivity,
100exactness, and surjectivity witnesses. -/
101@[simp]
102theorem ofExact_isExact (f : A →ₗ[R] B) (g : B →ₗ[R] C) (h : C →ₗ[R] D)
103 (hexact : Function.Injective f ∧ Function.Exact f g ∧
104 Function.Exact g h ∧ Function.Surjective h) :
105 (ofExact f g h hexact).IsExact :=
106 hexact
108end FourTermLinearSequence
110section LinearEquivTransport
112variable {R : Type*} [Semiring R]
113variable {A B B' C D : Type*}
114variable [AddCommMonoid B] [Module R B]
115variable [AddCommMonoid B'] [Module R B']
116variable [Zero C] [Zero D]
118/-- Transport function exactness across a linear equivalence on the middle type. -/
119theorem Function.Exact.linearEquiv_symm_comp_comp
120 (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C}
121 (hexact : Function.Exact f g) :
122 Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y)) := by
123 intro y
124 constructor
125 · intro hy
126 rcases (hexact (e y)).1 hy with ⟨x, hx⟩
127 exact ⟨x, by simp only [hx, LinearEquiv.symm_apply_apply]⟩
128 · rintro ⟨x, hx⟩
129 have hxy : f x = e y := by
130 have hcongr := congrArg e hx
131 simpa using hcongr
132 exact (hexact (e y)).2 ⟨x, hxy⟩
134/--
135Transporting exactness through a linear equivalence is equivalent to composing with the
136equivalence and its inverse.
137-/
138theorem Function.Exact.linearEquiv_symm_comp_comp_iff
139 (e : B ≃ₗ[R] B') {f : A → B'} {g : B' → C} :
140 Function.Exact (fun x : A => e.symm (f x)) (fun y : B => g (e y)) ↔
141 Function.Exact f g := by
142 constructor
143 · intro hexact
144 simpa using
145 (Function.Exact.linearEquiv_symm_comp_comp
146 (e := e.symm)
147 (f := fun x : A => e.symm (f x))
148 (g := fun y : B => g (e y))
149 hexact)
150 · exact Function.Exact.linearEquiv_symm_comp_comp e
152omit [Zero C] in
153/--
154Exactness is preserved when the tail map of an exact pair is composed with a linear equivalence
155on the middle term.
156-/
157theorem Function.Exact.comp_linearEquiv
158 (e : B ≃ₗ[R] B') {g : B' → C} {h : C → D}
159 (hexact : Function.Exact g h) :
160 Function.Exact (fun y : B => g (e y)) h := by
161 intro z
162 constructor
163 · intro hz
164 rcases (hexact z).1 hz with ⟨y', hy'⟩
165 rcases e.surjective y' with ⟨y, rfl⟩
166 exact ⟨y, hy'⟩
167 · rintro ⟨y, hy⟩
168 exact (hexact z).2 ⟨e y, hy⟩
170end LinearEquivTransport
172namespace FourTermLinearSequence
174variable {R : Type*} [Semiring R]
175variable {A B B' C D : Type*}
176variable [AddCommMonoid A] [Module R A]
177variable [AddCommMonoid B] [Module R B]
178variable [AddCommMonoid B'] [Module R B']
179variable [AddCommMonoid C] [Module R C]
180variable [AddCommMonoid D] [Module R D]
182/-- Reindex the first middle object of a bundled four-term sequence along a linear
183equivalence. Both adjacent maps are transported together, so their composition-zero
184equations remain part of the resulting object. -/
185def reindexMiddle (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B') :
186 FourTermLinearSequence R A B C D where
187 head := e.symm.toLinearMap.comp S.head
188 middle := S.middle.comp e.toLinearMap
189 tail := S.tail
190 middle_comp_head := by
191 ext x
192 have hx := congrArg (fun f : A →ₗ[R] C => f x) S.middle_comp_head
193 simpa using hx
194 tail_comp_middle := by
195 ext x
196 have hx := congrArg (fun f : B' →ₗ[R] D => f (e x)) S.tail_comp_middle
197 simpa using hx
199/-- Exactness is preserved when the first middle object of a bundled sequence is
200reindexed by a linear equivalence. -/
201theorem reindexMiddle_isExact
202 (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B')
203 (hexact : S.IsExact) : (S.reindexMiddle e).IsExact := by
204 refine ⟨?_, ?_, ?_, hexact.2.2.2⟩
205 · intro x y hxy
206 exact hexact.1 (e.symm.injective hxy)
207 · exact Function.Exact.linearEquiv_symm_comp_comp e hexact.2.1
208 · exact Function.Exact.comp_linearEquiv e hexact.2.2.1
210/-- Reindexing a middle object does not change whether a bundled sequence is exact. -/
211theorem reindexMiddle_isExact_iff
212 (S : FourTermLinearSequence R A B' C D) (e : B ≃ₗ[R] B') :
213 (S.reindexMiddle e).IsExact ↔ S.IsExact := by
214 constructor
215 · intro hexact
216 refine ⟨?_, ?_, ?_, hexact.2.2.2⟩
217 · intro x y hxy
218 apply hexact.1
219 change e.symm (S.head x) = e.symm (S.head y)
220 exact congrArg e.symm hxy
221 · intro y
222 constructor
223 · intro hy
224 have hy' : (S.reindexMiddle e).middle (e.symm y) = 0 := by
225 change S.middle (e (e.symm y)) = 0
226 simpa using hy
227 rcases (hexact.2.1 (e.symm y)).1 hy' with ⟨x, hx⟩
228 refine ⟨x, ?_⟩
229 simpa [reindexMiddle] using congrArg (fun z : B => e z) hx
230 · rintro ⟨x, rfl⟩
231 have hx := congrArg (fun f : A →ₗ[R] C => f x) S.middle_comp_head
232 simpa using hx
233 · intro z
234 constructor
235 · intro hz
236 rcases (hexact.2.2.1 z).1 hz with ⟨y, hy⟩
237 exact ⟨e y, by simpa [reindexMiddle] using hy⟩
238 · rintro ⟨y, rfl⟩
239 have hy := congrArg (fun f : B' →ₗ[R] D => f y) S.tail_comp_middle
240 simpa using hy
241 · exact S.reindexMiddle_isExact e
243end FourTermLinearSequence
245end
247end CrowellExactSequence