This module compares the relative free Fox derivative with the universal differential and deduces the discrete Magnus-kernel criterion in relative Fox coordinates.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
variable {X : Type} {H : Type}
variable [Group H] [Finite X]instance : Fintype XSurrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
variable {X : Type} {H : Type}
variable [Group H] [Finite X]
local instance : Fintype X := Fintype.ofFinite Xinstance : DecidableEq XIf the FoxDifferential relative free Fox derivative of a word vanishes, then the Crowell universal differential of the same word vanishes.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
variable {X : Type} {H : Type}
variable [Group H] [Finite X]
local instance : Fintype X := Fintype.ofFinite X
local instance : DecidableEq X := Classical.decEq Xtheorem 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 = 0Discrete Magnus-kernel theorem with the zero condition formulated using the FoxDifferential relative free Fox derivative.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace CrowellExactSequence
noncomputable section
open FoxDifferential
variable {X : Type} {H : Type}
variable [Group H] [Finite X]
local instance : Fintype X := Fintype.ofFinite X
local instance : DecidableEq X := Classical.decEq Xtheorem 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 ψ.ker