FoxDifferential.Discrete.KernelBoundary.MagnusKernel
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem kernelAbelianizationBoundaryLinearOfSurjective_injective
(hψ : Function.Surjective ψ) :
letIThe surjective-case linear kernel-boundary map is injective in the Magnus-kernel comparison.
Show proof
kernelAbelianizationModuleOfSurjective ψ hψ
Function.Injective (kernelAbelianizationBoundaryLinearOfSurjective ψ hψ) := 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 [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Rep.of_ρ, hxy,
kernelAbelianizationBoundaryLinearOfSurjective_apply]
_ = kernelAbelianizationToCoinvariantsLinear (ψ := ψ) y := by
exact differentialToKernelAugmentationIdealCoinvariantsLinearOfSurjective_boundary
(ψ := ψ) hψ y
exact (kernelAbelianizationToCoinvariantsLinear_injective (H := H) (ψ := ψ) hψ) hcoinvProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□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 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 [relationSubmodule_eq_crossedDifferentialRelationSubmodule, 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_oneProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□