ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusKernel
The principal declarations in this module are:
kernelAbelianizationBoundaryLinearOfSurjective_injectiveThe surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison. -mem_commutator_ker_of_d_eq_zero_of_surjectiveDiscrete Magnus-kernel form of the injectivity theorem: for a surjective \(\psi\), if the Crowell/Fox differential of a kernel element vanishes, then that element already lies in the ordinary commutator subgroup of \(\ker \psi\).
omit [DecidableEq H] in
omit [DecidableEq H] [DecidableEq G] in
theorem kernelAbelianizationBoundaryLinearOfSurjective_injective
(hψ : Function.Surjective ψ) :
letI := kernelAbelianizationModuleOfSurjective ψ hψ
Function.Injective (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)The surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.
Show Lean proof
by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
letI := kernelAugmentationIdealCoinvariantsModuleOfSurjective (ψ := ψ) hψ
intro x y hxy
have hcoinv :
kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
calc
kernelAbelianizationToCoinvariantsLinear (ψ := ψ) x =
differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) := by
symm
exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
(ψ := ψ) hψ x
_ =
differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective (ψ := ψ) hψ
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ y) := by
simp only [hxy, kernelAbelianizationBoundaryLinearOfSurjective_apply]
_ = kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
(ψ := ψ) hψ y
exact (kernelAbelianizationToCoinvariantsLinear_injective (H := H) (ψ := ψ) hψ) hcoinvomit [DecidableEq H] [DecidableEq G] in
theorem mem_commutator_ker_of_d_eq_zero_of_surjective
(hψ : Function.Surjective ψ) (n : ψ.ker) (hn : universalDifferential ψ n.1 = 0) :
n ∈ commutator ψ.kerDiscrete Magnus-kernel form of the injectivity theorem: for a surjective \(\psi\), if the Crowell/Fox differential of a kernel element vanishes, then that element already lies in the ordinary commutator subgroup of \(\ker \psi\).
Show Lean proof
by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
have hboundary_zero :
kernelAbelianizationBoundaryLinearOfSurjective ψ hψ
(Additive.ofMul (Abelianization.of n)) =
kernelAbelianizationBoundaryLinearOfSurjective ψ hψ 0 := by
rw [kernelAbelianizationBoundaryLinearOfSurjective_of, hn]
simp only [map_zero]
have hclass_zero :
(Additive.ofMul (Abelianization.of n) : KernelAbelianizationAdd ψ) = 0 :=
(FoxDifferential.KernelAugmentation.kernelAbelianizationBoundaryLinearOfSurjective_injective
(H := H) (ψ := ψ) hψ) hboundary_zero
have hclass_one : Abelianization.of n = 1 := by
simpa using congrArg Additive.toMul hclass_zero
exact (QuotientGroup.eq_one_iff (N := commutator ψ.ker) n).1 hclass_one