Source: ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusComparison
1import ProCGroups.FoxDifferential.Discrete.KernelBoundary.MagnusKernel
2import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Boundary
4/-!
5# Fox Differential / Discrete / Kernel Boundary / Magnus Comparison
7This module compares the relative free Fox derivative with the universal differential and
8deduces the discrete Magnus-kernel criterion in relative Fox coordinates.
9-/
11namespace CrowellExactSequence
13noncomputable section
15open FoxDifferential
17variable {X : Type} {H : Type}
18variable [Group H] [Finite X]
20local instance : Fintype X := Fintype.ofFinite X
21local instance : DecidableEq X := Classical.decEq X
23/--
24If the FoxDifferential relative free Fox derivative of a word vanishes, then the Crowell
25universal differential of the same word vanishes.
26-/
27theorem d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
28 (ψ : FreeGroup X →* H) (w : FreeGroup X)
29 (hw :
31 (H := H) X ψ w = 0) :
32 universalDifferential ψ w = 0 := by
33 have h :=
35 (H := H) X ψ w
36 rw [hw, map_zero] at h
37 exact h.symm
39/--
40Discrete Magnus-kernel theorem with the zero condition formulated using the FoxDifferential
41relative free Fox derivative.
42-/
43theorem mem_commutator_ker_of_relFreeFoxDeriv_eq_zero_of_surj
44 (ψ : FreeGroup X →* H) (hψ : Function.Surjective ψ) (n : ψ.ker)
45 (hn :
47 (H := H) X ψ n.1 = 0) :
48 n ∈ commutator ψ.ker :=
49 mem_commutator_ker_of_d_eq_zero_of_surjective (ψ := ψ) hψ n
50 (d_eq_zero_of_foxDifferential_relativeFreeGroupFoxDerivative_eq_zero
51 (X := X) (H := H) ψ n.1 hn)
53end
55end CrowellExactSequence