FoxDifferential/Discrete/KernelBoundary/MagnusKernel.lean
1import FoxDifferential.Discrete.KernelBoundary.Homology
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/KernelBoundary/MagnusKernel.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Magnus-kernel theorem for universal differentials
14For a surjective homomorphism, a kernel element whose universal differential vanishes lies
15in the ordinary commutator subgroup of the kernel. This is the algebraic kernel statement
16used by Crowell and metabelian applications.
18This file contains the final injectivity and kernel-membership consequences of the
19kernel-augmentation homology comparison.
20-/
22namespace FoxDifferential
24noncomputable section
26namespace KernelAugmentation
28variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
29variable {ψ : G →* H}
31omit [DecidableEq H] in
32omit [DecidableEq H] [DecidableEq G] in
34 (hψ : Function.Surjective ψ) :
35 letI := kernelAbelianizationModuleOfSurjective ψ hψ
36 Function.Injective (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ) := by
37 letI := kernelAbelianizationModuleOfSurjective ψ hψ
38 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
39 intro x y hxy
40 have hcoinv :
41 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
42 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
43 calc
44 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
46 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) := by
47 symm
49 (ψ := ψ) hψ x
50 _ =
52 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ y) := by
53 simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Rep.of_ρ, hxy,
55 _ = kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
57 (ψ := ψ) hψ y
58 exact (kernelAbelianizationToCoinvariantsLinear_injective (H := H) (ψ := ψ) hψ) hcoinv
60omit [DecidableEq H] [DecidableEq G] in
61/-- Discrete Magnus-kernel form of the injectivity theorem: for a surjective `ψ`, if the
62Crowell/Fox differential of a kernel element vanishes, then that element already lies in the
63ordinary commutator subgroup of `ker ψ`. -/
65 (hψ : Function.Surjective ψ) (n : ψ.ker) (hn : universalDifferential ψ n.1 = 0) :
66 n ∈ commutator ψ.ker := by
67 letI := kernelAbelianizationModuleOfSurjective ψ hψ
68 have hboundary_zero :
70 (Additive.ofMul (Abelianization.of n)) =
71 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ 0 := by
74 have hclass_zero :
75 (Additive.ofMul (Abelianization.of n) : KernelAbelianizationAdd ψ) = 0 :=
77 (H := H) (ψ := ψ) hψ) hboundary_zero
78 have hclass_one : Abelianization.of n = 1 := by
79 simpa using congrArg Additive.toMul hclass_zero
80 exact (QuotientGroup.eq_one_iff (N := commutator ψ.ker) n).1 hclass_one
82end KernelAugmentation
84export KernelAugmentation
88end
90end FoxDifferential