FoxDifferential/Discrete/KernelBoundary/Basic.lean
1import FoxDifferential.Discrete.KernelBoundary.IdentityAugmentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/KernelBoundary/Basic.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 map for discrete differential modules
14The kernel of a surjective homomorphism maps to the relative differential module by the
15universal differential. This module packages the induced boundary on the abelianization of
16the kernel and the module action needed by the discrete Fox exactness argument.
19and the induced `Z[H]`-module action in the surjective case.
20-/
22namespace FoxDifferential
24noncomputable section
27variable {H G : Type*} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
29abbrev KernelAbelianizationAdd (ψ : G →* H) : Type _ :=
30 Additive (Abelianization ψ.ker)
32omit [DecidableEq H] [DecidableEq G] in
33/-- The Crowell boundary map lands in the kernel of the augmentation map. -/
34theorem augmentation_toGroupRing_eq_zero (ψ : G →* H) (x : DifferentialModule ψ) :
35 augmentation H (toGroupRing ψ x) = 0 := by
36 exact (mem_augmentationIdeal_iff (H := H) (x := toGroupRing ψ x)).1
37 (toGroupRing_mem_augmentationIdeal (H := H) ψ x)
39omit [DecidableEq H] in
40/-- The augmentation map `ℤ[H] → ℤ` is surjective. -/
41theorem augmentation_surjective : Function.Surjective (augmentation H) := by
42 intro n
44 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, map_intCast, Int.cast_eq]
46omit [DecidableEq H] [DecidableEq G] in
47/-- Tail exactness of the discrete Crowell sequence:
48`A_ψ → ℤ[H] → ℤ` is exact when `ψ` is surjective. -/
49theorem exact_toGroupRing_augmentation (ψ : G →* H) (hψ : Function.Surjective ψ) :
50 Function.Exact (fun x => toGroupRing ψ x) (augmentation H) := by
51 intro y
52 constructor
53 · intro hy
54 have hy_mem : y ∈ augmentationIdeal H := (mem_augmentationIdeal_iff (H := H) (x := y)).2 hy
55 let y' : augmentationIdeal H := ⟨y, hy_mem⟩
56 rcases toAugmentationIdeal_surjective (H := H) ψ hψ y' with ⟨x, hx⟩
57 refine ⟨x, ?_⟩
58 exact congrArg Subtype.val hx
59 · rintro ⟨x, rfl⟩
60 exact augmentation_toGroupRing_eq_zero (H := H) ψ x
62/-- The kernel of `ψ` maps multiplicatively into the additive differential module via `d`. -/
63def kernelBoundary (ψ : G →* H) : ψ.ker →* Multiplicative (DifferentialModule ψ) where
64 toFun g := Multiplicative.ofAdd (universalDifferential ψ g.1)
65 map_one' := by
66 apply congrArg Multiplicative.ofAdd
67 simp only [OneMemClass.coe_one, universalDifferential_one]
68 map_mul' g₁ g₂ := by
69 apply congrArg Multiplicative.ofAdd
70 have h := universalDifferential_mul ψ g₁.1 g₂.1
72 rw [g₁.2, groupRing_of_one (H := H)]
73 rw [hψ, one_smul] at h
74 simpa using h
76/-- The kernel boundary factors through the abelianization of `ker ψ`. -/
77def kernelAbelianizationBoundary (ψ : G →* H) :
78 Abelianization ψ.ker →* Multiplicative (DifferentialModule ψ) :=
79 Abelianization.lift (kernelBoundary ψ)
81/-- Additive form of the kernel-to-differential-module map. -/
82def kernelAbelianizationBoundaryAdd (ψ : G →* H) :
83 Additive (Abelianization ψ.ker) →+ DifferentialModule ψ where
84 toFun x := Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))
85 map_zero' := by
86 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, toMul_zero, map_one, toAdd_one]
87 map_add' x y := by
88 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, toMul_add, map_mul, toAdd_mul]
90omit [DecidableEq H] [DecidableEq G] in
91@[simp 900]
92theorem kernelAbelianizationBoundaryAdd_of (ψ : G →* H) (g : ψ.ker) :
93 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of g)) = universalDifferential ψ g.1 := by
94 change Multiplicative.toAdd (Multiplicative.ofAdd (universalDifferential ψ g.1)) = universalDifferential ψ g.1
95 rfl
97/-!
98The next Crowell exact-sequence library layer packages the conjugation action on `ker ψ`, its descent to
100-/
102/-- Conjugation by `G` on `ker ψ`, transported to the abelianization of `ker ψ`. -/
103def kernelAbelianizationConj (ψ : G →* H) :
104 G →* MulAut (Abelianization ψ.ker) where
105 toFun g := (MulAut.conjNormal (H := ψ.ker) g).abelianizationCongr
106 map_one' := by
107 ext x
108 refine QuotientGroup.induction_on x ?_
109 intro n
110 have hconj : MulAut.conjNormal (H := ψ.ker) (1 : G) = 1 := by
111 ext m
113 rw [hconj]
114 rfl
115 map_mul' g₁ g₂ := by
116 ext x
117 refine QuotientGroup.induction_on x ?_
118 intro n
119 let e₁ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₁
120 let e₂ : MulAut ψ.ker := MulAut.conjNormal (H := ψ.ker) g₂
121 have hconj : MulAut.conjNormal (H := ψ.ker) (g₁ * g₂) = e₁ * e₂ := by
122 ext m
124 rw [hconj]
125 calc
126 (e₁ * e₂).abelianizationCongr (Abelianization.of n)
127 = Abelianization.of ((e₁ * e₂) n) := by
128 exact abelianizationCongr_of (e := e₁ * e₂) n
129 _ = e₁.abelianizationCongr (Abelianization.of (e₂ n)) := by
130 exact (abelianizationCongr_of (e := e₁) (e₂ n)).symm
131 _ = e₁.abelianizationCongr (e₂.abelianizationCongr (Abelianization.of n)) := by
132 rw [abelianizationCongr_of (e := e₂) n]
133 _ = (e₁.abelianizationCongr * e₂.abelianizationCongr) (Abelianization.of n) := by
134 rfl
136omit [DecidableEq H] [DecidableEq G] in
137@[simp]
138theorem kernelAbelianizationConj_of (ψ : G →* H) (g : G) (n : ψ.ker) :
139 kernelAbelianizationConj ψ g (Abelianization.of n) =
140 Abelianization.of (MulAut.conjNormal (H := ψ.ker) g n) := by
141 rfl
143omit [DecidableEq H] [DecidableEq G] in
144@[simp]
145theorem kernelAbelianizationConj_eq_one_of_mem_ker (ψ : G →* H) (n : ψ.ker) :
146 kernelAbelianizationConj ψ n = 1 := by
147 ext x
148 refine QuotientGroup.induction_on x ?_
149 intro k
150 calc
151 kernelAbelianizationConj ψ n (Abelianization.of k)
152 = Abelianization.of ((MulAut.conjNormal (H := ψ.ker) (n : G)) k) := by
153 exact abelianizationCongr_of (e := MulAut.conjNormal (H := ψ.ker) (n : G)) k
154 _ = Abelianization.of (n * k * n⁻¹) := by
155 congr 1
156 _ = Abelianization.of k := by
159omit [DecidableEq H] [DecidableEq G] in
160theorem ker_le_kernelAbelianizationConj_ker (ψ : G →* H) :
161 ψ.ker ≤ (kernelAbelianizationConj ψ).ker := by
162 intro n hn
163 change kernelAbelianizationConj ψ n = 1
164 simpa using kernelAbelianizationConj_eq_one_of_mem_ker (ψ := ψ) ⟨n, hn⟩
166/-- The conjugation action on `ker ψ` abelianized factors through `G / ker ψ`. -/
167def quotientKernelAbelianizationConj (ψ : G →* H) :
168 G ⧸ ψ.ker →* MulAut (Abelianization ψ.ker) :=
169 QuotientGroup.lift ψ.ker (kernelAbelianizationConj ψ) (ker_le_kernelAbelianizationConj_ker ψ)
171omit [DecidableEq H] [DecidableEq G] in
172/-- If `ψ` is surjective, the conjugation action on `ker ψ` abelianized is expressed directly
173as an action of `H`. -/
175 (ψ : G →* H) (hψ : Function.Surjective ψ) :
176 H →* MulAut (Abelianization ψ.ker) :=
177 (quotientKernelAbelianizationConj ψ).comp
178 (QuotientGroup.quotientKerEquivOfSurjective (φ := ψ) hψ).symm.toMonoidHom
180omit [DecidableEq H] [DecidableEq G] in
181@[simp 900]
183 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
184 kernelAbelianizationConjOfSurjective ψ hψ h =
185 kernelAbelianizationConj ψ (Function.surjInv hψ h) := by
186 let g₁ : G := hψ.hasRightInverse.choose h
187 let g₂ : G := Function.surjInv hψ h
188 have hg₁ : ψ g₁ = h := hψ.hasRightInverse.choose_spec h
189 have hg₂ : ψ g₂ = h := Function.surjInv_eq hψ h
190 have hker : ψ (g₁ * g₂⁻¹) = 1 := by
192 have htriv :
193 kernelAbelianizationConj ψ (g₁ * g₂⁻¹) = 1 := by
194 simpa using kernelAbelianizationConj_eq_one_of_mem_ker (ψ := ψ) ⟨g₁ * g₂⁻¹, hker⟩
195 have hsame :
196 kernelAbelianizationConj ψ g₁ = kernelAbelianizationConj ψ g₂ := by
197 have hmul :
198 kernelAbelianizationConj ψ g₁ *
199 (kernelAbelianizationConj ψ g₂)⁻¹ = 1 := by
201 have hmul' := congrArg (fun u : MulAut (Abelianization ψ.ker) =>
202 u * kernelAbelianizationConj ψ g₂) hmul
203 simpa [mul_assoc] using hmul'
204 unfold kernelAbelianizationConjOfSurjective QuotientGroup.quotientKerEquivOfSurjective
205 QuotientGroup.quotientKerEquivOfRightInverse
206 simpa [g₁, g₂, quotientKernelAbelianizationConj] using hsame
208/-- Surjective-case conjugation action, rewritten additively. -/
210 (ψ : G →* H) (hψ : Function.Surjective ψ) :
211 H →* AddAut (KernelAbelianizationAdd ψ) :=
212 (AddAutAdditive (Abelianization ψ.ker)).symm.toMonoidHom.comp
215omit [DecidableEq H] [DecidableEq G] in
216/-- The surjective-case action as a hom into `ℤ`-linear endomorphisms. -/
217def kernelAbelianizationAddAutToModuleEnd (ψ : G →* H) :
218 AddAut (KernelAbelianizationAdd ψ) →* Module.End ℤ (KernelAbelianizationAdd ψ) where
219 toFun e := e.toIntLinearEquiv.toLinearMap
220 map_one' := by
221 ext x
222 change (1 : AddAut (KernelAbelianizationAdd ψ)) x = x
223 rfl
224 map_mul' e₁ e₂ := by
225 ext x
226 change (e₁ * e₂) x = e₁ (e₂ x)
227 rfl
229/-- The surjective-case action as a hom into `ℤ`-linear endomorphisms. -/
231 (ψ : G →* H) (hψ : Function.Surjective ψ) :
232 H →* Module.End ℤ (KernelAbelianizationAdd ψ) where
233 toFun h := kernelAbelianizationAddAutToModuleEnd (ψ := ψ)
235 map_one' := by
236 rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_one]
237 ext x
238 rfl
239 map_mul' h₁ h₂ := by
240 rw [(kernelAbelianizationAddAutOfSurjective ψ hψ).map_mul]
241 ext x
242 rfl
244omit [DecidableEq H] [DecidableEq G] in
245@[simp]
247 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
248 kernelAbelianizationModuleEndOfSurjective ψ hψ h x =
249 Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x)) := by
250 change
251 Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x)) =
252 Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h (Additive.toMul x))
253 rfl
255/-- The induced `ℤ[H]`-action on `ker(ψ)^ab` in additive form. -/
257 (ψ : G →* H) (hψ : Function.Surjective ψ) :
258 GroupRing H →+* Module.End ℤ (KernelAbelianizationAdd ψ) :=
259 MonoidAlgebra.liftNCRingHom (Int.castRingHom (Module.End ℤ (KernelAbelianizationAdd ψ)))
260 (kernelAbelianizationModuleEndOfSurjective ψ hψ) (by
261 intro z h
262 ext x
263 simp only [eq_intCast, Module.End.mul_apply, kernelAbelianizationModuleEndOfSurjective_apply,
264 kernelAbelianizationConjOfSurjective_eq_surjInv, Module.End.intCast_apply, toMul_zsmul, toMul_ofMul, map_smul])
266omit [DecidableEq H] [DecidableEq G] in
267@[simp]
269 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
270 kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h) =
271 kernelAbelianizationModuleEndOfSurjective ψ hψ h := by
272 ext x
273 simp only [kernelAbelianizationActionRingHomOfSurjective, MonoidAlgebra.of_apply,
274 MonoidAlgebra.liftNCRingHom_single, eq_intCast, Int.cast_one, one_mul,
275 kernelAbelianizationModuleEndOfSurjective_apply, kernelAbelianizationConjOfSurjective_eq_surjInv, toMul_ofMul]
277/-- The `ℤ[H]`-module structure on `ker(ψ)^ab` induced by surjective conjugation. -/
279 (ψ : G →* H) (hψ : Function.Surjective ψ) :
280 Module (GroupRing H) (KernelAbelianizationAdd ψ) :=
281 Module.compHom _ (kernelAbelianizationActionRingHomOfSurjective ψ hψ)
283omit [DecidableEq H] [DecidableEq G] in
284@[simp]
286 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : Abelianization ψ.ker) :
288 (Additive.ofMul (kernelAbelianizationConjOfSurjective ψ hψ h x)) =
290 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul x) := by
291 let g : G := Function.surjInv hψ h
292 have hg : ψ g = h := Function.surjInv_eq hψ h
293 refine QuotientGroup.induction_on x ?_
294 intro n
296 change kernelAbelianizationBoundaryAdd ψ
297 (Additive.ofMul (kernelAbelianizationConj ψ g (Abelianization.of n))) =
299 kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))
302 simpa [g, hg, MulAut.conjNormal_apply, mul_assoc] using universalDifferential_conj_of_mem_ker ψ g n.1 n.2
304omit [DecidableEq H] [DecidableEq G] in
305@[simp]
307 (ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) (x : KernelAbelianizationAdd ψ) :
308 letI := kernelAbelianizationModuleOfSurjective ψ hψ
309 kernelAbelianizationBoundaryAdd ψ ((MonoidAlgebra.of ℤ H h : GroupRing H) • x) =
310 (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x := by
311 letI := kernelAbelianizationModuleOfSurjective ψ hψ
312 change kernelAbelianizationBoundaryAdd ψ
313 ((kernelAbelianizationActionRingHomOfSurjective ψ hψ (MonoidAlgebra.of ℤ H h)) x) =
314 (MonoidAlgebra.of ℤ H h : GroupRing H) • kernelAbelianizationBoundaryAdd ψ x
317 simpa using
318 kernelAbelianizationBoundaryAdd_conjOfSurjective ψ hψ h (Additive.toMul x)
320/-- The head map of the discrete Crowell sequence, in `ℤ[H]`-linear form when `ψ` is surjective. -/
322 (ψ : G →* H) (hψ : Function.Surjective ψ) :
323 letI := kernelAbelianizationModuleOfSurjective ψ hψ
324 KernelAbelianizationAdd ψ →ₗ[GroupRing H] DifferentialModule ψ := by
325 letI := kernelAbelianizationModuleOfSurjective ψ hψ
326 let f : KernelAbelianizationAdd ψ →ₗ[ℤ] DifferentialModule ψ :=
327 (kernelAbelianizationBoundaryAdd ψ).toIntLinearMap
328 exact MonoidAlgebra.equivariantOfLinearOfComm f
329 (fun h x => by
330 simpa using kernelAbelianizationBoundaryAdd_commOfSurjective (ψ := ψ) hψ h x)
332omit [DecidableEq H] [DecidableEq G] in
333@[simp]
335 (ψ : G →* H) (hψ : Function.Surjective ψ) (n : ψ.ker) :
337 (Additive.ofMul (Abelianization.of n)) = universalDifferential ψ n.1 := by
338 letI := kernelAbelianizationModuleOfSurjective ψ hψ
340 kernelAbelianizationBoundaryLinearOfSurjective, MonoidAlgebra.equivariantOfLinearOfComm_apply,
341 AddMonoidHom.coe_toIntLinearMap, kernelAbelianizationBoundaryAdd_of]
343omit [DecidableEq H] [DecidableEq G] in
344@[simp]
346 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
348 kernelAbelianizationBoundaryAdd ψ x := by
349 letI := kernelAbelianizationModuleOfSurjective ψ hψ
350 rfl
352omit [DecidableEq H] [DecidableEq G] in
353@[simp]
355 (ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
356 toGroupRing ψ (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0 := by
358 change toGroupRing ψ
359 (Multiplicative.toAdd (kernelAbelianizationBoundary ψ (Additive.toMul x))) = 0
360 refine QuotientGroup.induction_on (Additive.toMul x) ?_
361 intro n
362 change toGroupRing ψ (universalDifferential ψ n.1) = 0
365/-- The `A_ψ`-submodule generated by the head map in the surjective case. -/
367 (ψ : G →* H) (hψ : Function.Surjective ψ) :
368 Submodule (GroupRing H) (DifferentialModule ψ) := by
369 letI := kernelAbelianizationModuleOfSurjective ψ hψ
370 exact LinearMap.range (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
373end
375end FoxDifferential