Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusKernel
1import ProCGroups.FoxDifferential.Discrete.KernelBoundary.Homology
3/-!
4# Fox differential: discrete — kernel boundary — magnus kernel
6The principal declarations in this module are:
8- `kernelAbelianizationBoundaryLinearOfSurjective_injective`
9 The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.
10- `mem_commutator_ker_of_d_eq_zero_of_surjective`
11 Discrete Magnus-kernel form of the injectivity theorem: for a surjective \(\psi\), if the
12 Crowell/Fox differential of a kernel element vanishes, then that element already lies in the
13 ordinary commutator subgroup of \(\ker \psi\).
14-/
16namespace FoxDifferential
18noncomputable section
20namespace KernelAugmentation
22variable {H G : Type} [Group H] [DecidableEq H] [Group G] [DecidableEq G]
23variable {ψ : G →* H}
25omit [DecidableEq H] in
26omit [DecidableEq H] [DecidableEq G] in
27/-- The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison. -/
28theorem kernelAbelianizationBoundaryLinearOfSurjective_injective
29 (hψ : Function.Surjective ψ) :
30 letI := kernelAbelianizationModuleOfSurjective ψ hψ
31 Function.Injective (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ) := by
32 letI := kernelAbelianizationModuleOfSurjective ψ hψ
33 letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
34 intro x y hxy
35 have hcoinv :
36 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
37 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
38 calc
39 kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
40 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
41 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) := by
42 symm
43 exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
44 (ψ := ψ) hψ x
45 _ =
46 differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
47 (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ y) := by
48 simp only [hxy, kernelAbelianizationBoundaryLinearOfSurjective_apply]
49 _ = kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
50 exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
51 (ψ := ψ) hψ y
52 exact (kernelAbelianizationToCoinvariantsLinear_injective (H := H) (ψ := ψ) hψ) hcoinv
54omit [DecidableEq H] [DecidableEq G] in
55/--
56Discrete Magnus-kernel form of the injectivity theorem: for a surjective \(\psi\), if the
57Crowell/Fox differential of a kernel element vanishes, then that element already lies in the
58ordinary commutator subgroup of \(\ker \psi\).
59-/
60theorem mem_commutator_ker_of_d_eq_zero_of_surjective
61 (hψ : Function.Surjective ψ) (n : ψ.ker) (hn : universalDifferential ψ n.1 = 0) :
62 n ∈ commutator ψ.ker := by
63 letI := kernelAbelianizationModuleOfSurjective ψ hψ
64 have hboundary_zero :
65 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
66 (Additive.ofMul (Abelianization.of n)) =
67 kernelAbelianizationBoundaryLinearOfSurjective ψ hψ 0 := by
68 rw [kernelAbelianizationBoundaryLinearOfSurjective_of, hn]
69 simp only [map_zero]
70 have hclass_zero :
71 (Additive.ofMul (Abelianization.of n) : KernelAbelianizationAdd ψ) = 0 :=
73 (H := H) (ψ := ψ) hψ) hboundary_zero
74 have hclass_one : Abelianization.of n = 1 := by
75 simpa using congrArg Additive.toMul hclass_zero
76 exact (QuotientGroup.eq_one_iff (N := commutator ψ.ker) n).1 hclass_one
78end KernelAugmentation
80export KernelAugmentation
81 (kernelAbelianizationBoundaryLinearOfSurjective_injective
82 mem_commutator_ker_of_d_eq_zero_of_surjective)
84end
86end FoxDifferential