ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusComparison
This module compares the relative free Fox derivative with the universal differential and deduces the discrete Magnus-kernel criterion in relative Fox coordinates.
imports
theorem d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
(ψ : FreeGroup X →* H) (w : FreeGroup X)
(hw :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
(H := H) X ψ w = 0) :
universalDifferential ψ w = 0If the FoxDifferential relative free Fox derivative of a word vanishes, then the Crowell universal differential of the same word vanishes.
Show Lean proof
by
have h :=
FoxDifferential.FoxCalculus.relativeFreeFoxCoordinatesLinearMap_derivative
(H := H) X ψ w
rw [hw, map_zero] at h
exact h.symmtheorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
(ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ) (n : ψ.ker)
(hn :
FoxDifferential.FoxCalculus.relativeFreeGroupFoxDerivative
(H := H) X ψ n.1 = 0) :
n ∈ commutator ψ.kerDiscrete Magnus-kernel theorem with the zero condition formulated using the FoxDifferential relative free Fox derivative.
Show Lean proof
mem_commutator_ker_of_d_eq_zero_of_surjective (ψ := ψ) hψ n
(d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
(X := X) (H := H) ψ n.1 hn)