FoxDifferential/Discrete/KernelBoundary/Quotient.lean
1import FoxDifferential.Discrete.KernelBoundary.Basic
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/KernelBoundary/Quotient.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Kernel-boundary quotient and augmentation exactness
14The quotient of the relative differential module by the kernel-boundary image maps to the
15identity differential module and to the augmentation ideal. The result is the algebraic
16head-exactness bridge used by Crowell exact sequences.
18This file contains the quotient/exactness bridge for the discrete Crowell sequence and the
19kernel-side group-homology infrastructure used to prove injectivity of the head map.
20-/
22namespace FoxDifferential
24noncomputable section
26open FoxDifferential
28variable {H G : Type*} [Group H] [Group G]
30/-- The quotient of `A_ψ` by the image of the head map. -/
31abbrev HeadQuotientOfSurjective (ψ : G →* H) (hψ : Function.Surjective ψ) : Type _ :=
34/-- The canonical map from `A_ψ` to the derived module of the identity on `H`. -/
35def toIdentityDifferentialModule (ψ : G →* H) :
36 DifferentialModule ψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
37 lift ψ (fun g => universalDifferential (MonoidHom.id H) (ψ g)) (by
38 intro g₁ g₂
39 simpa [map_mul] using universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂))
41@[simp]
42theorem toIdentityDifferentialModule_d (ψ : G →* H) (g : G) :
43 toIdentityDifferentialModule ψ (universalDifferential ψ g) = universalDifferential (MonoidHom.id H) (ψ g) := by
44 simpa [toIdentityDifferentialModule] using
45 lift_d (A := DifferentialModule (MonoidHom.id H)) ψ
46 (fun g => universalDifferential (MonoidHom.id H) (ψ g)) (by
47 intro g₁ g₂
48 simpa [map_mul] using universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂)) g
51 (ψ : G →* H) :
52 (toAugmentationIdeal (H := H) (MonoidHom.id H)).comp (toIdentityDifferentialModule ψ) =
53 toAugmentationIdeal (H := H) ψ := by
54 apply hom_ext ψ
55 intro g
56 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, LinearMap.coe_comp, Function.comp_apply,
57 toIdentityDifferentialModule_d, toAugmentationIdeal_d, augmentationBoundary, groupRingBoundary, MonoidHom.id_apply,
58 MonoidAlgebra.of_apply]
60@[simp]
62 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
64 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0 := by
65 letI := kernelAbelianizationModuleOfSurjective ψ hψ
67 change
68 (fun y : Abelianization ψ.ker =>
69 toIdentityDifferentialModule ψ (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) = 0)
70 (Additive.toMul x)
71 refine QuotientGroup.induction_on (Additive.toMul x) ?_
72 intro n
73 change toIdentityDifferentialModule ψ
74 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) = 0
75 have hinner :
77 (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) =
78 toIdentityDifferentialModule ψ (universalDifferential ψ n.1) := by
79 exact congrArg (toIdentityDifferentialModule ψ) (kernelAbelianizationBoundaryAdd_of ψ n)
80 rw [hinner, toIdentityDifferentialModule_d, n.2, universalDifferential_one]
83 (ψ : G →* H) (hψ : Function.Surjective ψ) :
85 LinearMap.ker (toIdentityDifferentialModule ψ) := by
86 intro y hy
87 rcases hy with ⟨x, rfl⟩
88 simpa [LinearMap.mem_ker] using
91/-- The quotient map `A_ψ / im(head) → A_id`. -/
93 (ψ : G →* H) (hψ : Function.Surjective ψ) :
94 HeadQuotientOfSurjective ψ hψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
95 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).liftQ
99@[simp]
101 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
103 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
104 toIdentityDifferentialModule ψ x := by
105 rfl
107/-- A section of `ψ`, viewed as a differential map into the head quotient. -/
109 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
110 HeadQuotientOfSurjective ψ hψ :=
111 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ
112 (universalDifferential ψ (Function.surjInv hψ h))
115 (ψ : G →* H) (hψ : Function.Surjective ψ) :
116 IsDifferentialMap (A := HeadQuotientOfSurjective ψ hψ) (MonoidHom.id H)
117 (headQuotientSectionOfSurjective ψ hψ) := by
118 intro h₁ h₂
119 let s : H → G := Function.surjInv hψ
120 let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
122 have hs12 : ψ (s (h₁ * h₂)) = h₁ * h₂ := by
123 simpa [s] using Function.surjInv_eq hψ (h₁ * h₂)
124 let n : ψ.ker := ⟨s (h₁ * h₂) * (s h₁ * s h₂)⁻¹, by
125 calc
126 ψ (s (h₁ * h₂) * (s h₁ * s h₂)⁻¹)
128 _ = (h₁ * h₂) * (h₂⁻¹ * h₁⁻¹) := by
129 rw [hs12]
131 _ = 1 := by simp only [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
132 have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
133 have hn_mem : universalDifferential ψ n.1 ∈ q := by
134 letI := kernelAbelianizationModuleOfSurjective ψ hψ
135 rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
136 exact LinearMap.mem_range_self _ _
137 exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
138 have hs :
139 universalDifferential ψ (s (h₁ * h₂)) = universalDifferential ψ n.1 + universalDifferential ψ (s h₁ * s h₂) := by
140 have hmul := universalDifferential_mul ψ n.1 (s h₁ * s h₂)
142 rw [n.2, groupRing_of_one (H := H)]
143 rw [hψn, one_smul] at hmul
144 simpa [n, s, mul_assoc] using hmul
145 have hq :
146 q.mkQ (universalDifferential ψ (s (h₁ * h₂))) = q.mkQ (universalDifferential ψ (s h₁ * s h₂)) := by
147 have hq' := congrArg q.mkQ hs
149 calc
150 headQuotientSectionOfSurjective ψ hψ (h₁ * h₂)
151 = q.mkQ (universalDifferential ψ (s (h₁ * h₂))) := rfl
152 _ = q.mkQ (universalDifferential ψ (s h₁ * s h₂)) := hq
153 _ = q.mkQ (universalDifferential ψ (s h₁) + (MonoidAlgebra.of ℤ H (ψ (s h₁))) • universalDifferential ψ (s h₂)) := by
155 _ = headQuotientSectionOfSurjective ψ hψ h₁ +
157 headQuotientSectionOfSurjective ψ hψ h₂ := by
158 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Function.surjInv_eq hψ h₁,
159 MonoidAlgebra.of_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_add, Submodule.Quotient.mk_smul,
162/-- The inverse-direction map `A_id → A_ψ / im(head)` induced by a surjective section of `ψ`. -/
164 (ψ : G →* H) (hψ : Function.Surjective ψ) :
165 DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] HeadQuotientOfSurjective ψ hψ :=
166 lift (MonoidHom.id H) (headQuotientSectionOfSurjective ψ hψ)
169@[simp]
171 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
172 fromIdentityDifferentialModuleOfSurjective ψ hψ (universalDifferential (MonoidHom.id H) h) =
173 headQuotientSectionOfSurjective ψ hψ h := by
174 simpa [fromIdentityDifferentialModuleOfSurjective] using
175 lift_d (A := HeadQuotientOfSurjective ψ hψ) (MonoidHom.id H)
180 (ψ : G →* H) (hψ : Function.Surjective ψ) :
181 (headQuotientToIdentityDifferentialModule ψ hψ).comp
183 LinearMap.id := by
184 apply hom_ext (ψ := MonoidHom.id H)
185 intro h
186 rw [LinearMap.comp_apply, fromIdentityDifferentialModuleOfSurjective_d,
189 simp only [Function.surjInv_eq hψ h, relationSubmodule_eq_crossedDifferentialRelationSubmodule,
190 LinearMap.id_coe, id_eq]
193 (ψ : G →* H) (hψ : Function.Surjective ψ) :
194 (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
196 (kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ := by
197 apply hom_ext (ψ := ψ)
198 intro g
199 let s : H → G := Function.surjInv hψ
200 let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
202 let n : ψ.ker := ⟨g * (s (ψ g))⁻¹, by
203 simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g), mul_inv_cancel, s]⟩
204 have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
205 have hn_mem : universalDifferential ψ n.1 ∈ q := by
206 letI := kernelAbelianizationModuleOfSurjective ψ hψ
207 rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
208 exact LinearMap.mem_range_self _ _
209 exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
210 have hgdecomp : universalDifferential ψ g = universalDifferential ψ n.1 + universalDifferential ψ (s (ψ g)) := by
211 have hmul := universalDifferential_mul ψ n.1 (s (ψ g))
213 rw [n.2, groupRing_of_one (H := H)]
214 rw [hψn, one_smul] at hmul
215 simpa [n, s, mul_assoc] using hmul
216 have hq : q.mkQ (universalDifferential ψ g) = q.mkQ (universalDifferential ψ (s (ψ g))) := by
217 have hq' := congrArg q.mkQ hgdecomp
219 calc
222 = q.mkQ (universalDifferential ψ (s (ψ g))) := by
225 _ = q.mkQ (universalDifferential ψ g) := hq.symm
227/-- The quotient `A_ψ / im(head)` is canonically identified with the derived module of `id_H`. -/
229 (ψ : G →* H) (hψ : Function.Surjective ψ) :
230 HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
231 toLinearMap := headQuotientToIdentityDifferentialModule ψ hψ
232 invFun := fromIdentityDifferentialModuleOfSurjective ψ hψ
233 left_inv := by
234 intro x
235 have hcomp :
236 (fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
238 LinearMap.id := by
239 apply Submodule.linearMap_qext _
240 simpa using
242 exact LinearMap.congr_fun hcomp x
243 right_inv := by
244 intro x
245 exact LinearMap.congr_fun
248/-- For a surjective `ψ`, the Crowell head quotient is the augmentation ideal. -/
250 (ψ : G →* H) (hψ : Function.Surjective ψ) :
251 HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] augmentationIdeal H :=
252 by
253 classical
254 exact
258@[simp]
260 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
262 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
263 toAugmentationIdeal (H := H) ψ x := by
265 rw [LinearEquiv.trans_apply]
266 change (FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal (H := H))
268 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x)) = _
270 have hid := congrArg
271 (fun f : DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] augmentationIdeal H =>
272 f (toIdentityDifferentialModule ψ x))
274 exact hid.trans <|
275 LinearMap.congr_fun (toAugmentationIdeal_id_comp_toIdentityDifferentialModule (H := H) ψ) x
278 (ψ : G →* H) (hψ : Function.Surjective ψ) :
280 LinearMap.ker (toAugmentationIdeal (H := H) ψ) := by
281 apply le_antisymm
282 · intro y hy
283 rcases hy with ⟨x, rfl⟩
284 change toAugmentationIdeal (H := H) ψ
285 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0
286 apply Subtype.ext
287 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
288 · intro y hy
289 have hy0 : toAugmentationIdeal (H := H) ψ y = 0 := by
290 simpa [LinearMap.mem_ker] using hy
291 have hq0 :
293 ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y) = 0 := by
295 exact hy0
296 have hq : ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y :
297 HeadQuotientOfSurjective ψ hψ) = 0 := by
298 exact (headQuotientEquivAugmentationIdealOfSurjective ψ hψ).injective
299 (by simpa using hq0)
300 exact (Submodule.Quotient.mk_eq_zero (p := kernelAbelianizationBoundaryRangeOfSurjective ψ hψ)
301 (x := y)).1 hq
303/-- Exactness at `A_ψ`, formulated against the augmentation ideal. -/
305 (ψ : G →* H) (hψ : Function.Surjective ψ) :
306 Function.Exact
308 (toAugmentationIdeal (H := H) ψ) := by
309 intro y
310 constructor
311 · intro hy
312 have hyker : y ∈ LinearMap.ker (toAugmentationIdeal (H := H) ψ) := by
313 simpa [LinearMap.mem_ker] using hy
315 (H := H) (ψ := ψ) hψ] at hyker
316 exact hyker
317 · rintro ⟨x, rfl⟩
318 apply Subtype.ext
319 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
321/-- Exactness at `A_ψ`, against the usual map `A_ψ → ℤ[H]`. -/
323 (ψ : G →* H) (hψ : Function.Surjective ψ) :
324 Function.Exact
326 (toGroupRing ψ) := by
327 intro y
328 constructor
329 · intro hy
330 have hy' : toAugmentationIdeal (H := H) ψ y = 0 := by
331 apply Subtype.ext
332 exact hy
334 (H := H) ψ hψ y).1 hy'
335 · rintro ⟨x, rfl⟩
336 exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
337end
339end FoxDifferential