The principal declarations in this module are:
groupRingBoundaryThe standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map.
groupRingBoundaryHomThe Fox boundary is itself a crossed differential.
groupRingBoundary_oneThe Fox boundary vanishes at the identity.
groupRingBoundary_eq_zero_of_mem_kerThe Fox boundary is zero on elements in the kernel of \(\psi\).
The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def groupRingBoundary (ψ : G →* H) (g : G) : GroupRing HThe Fox boundary vanishes at the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingBoundary_one (ψ : G →* H) :
groupRingBoundary ψ (1 : G) = 0The Fox boundary is zero on elements in the kernel of \(\psi\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingBoundary_eq_zero_of_mem_ker (ψ : G →* H) {g : G} (hg : ψ g = 1) :
groupRingBoundary ψ g = 0The Fox boundary vanishes on the kernel subgroup of \(\psi\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingBoundary_subtype_ker (ψ : G →* H) (g : ψ.ker) :
groupRingBoundary ψ g = 0The Fox boundary is itself a crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def groupRingBoundaryHom (ψ : G →* H) : DifferentialHom ψ (GroupRing H) where
toFun := groupRingBoundary ψ
map_mul' := by
intro g₁ g₂
simp only [scalarCrossedAction_apply, groupRingBoundary, map_mul,
MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg,
add_comm, groupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
add_neg_cancel_comm_assoc]The bundled group-ring boundary homomorphism evaluates to the usual Fox boundary.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingBoundaryHom_apply (ψ : G →* H) (g : G) :
groupRingBoundaryHom ψ g = groupRingBoundary ψ gGroup-ring functoriality carries Fox boundaries to Fox boundaries.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingMap_groupRingBoundary {K : Type*} [Group K]
(φ : H →* K) (ψ : G →* H) (g : G) :
groupRingMap φ (groupRingBoundary ψ g) = groupRingBoundary (φ.comp ψ) gThe universal boundary map \(A_{\psi}\ \to \mathbb{Z}[H]\), \(universalDifferential(g) \mapsto \psi(g) - 1\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def toGroupRing (ψ : G →* H) : DifferentialModule ψ →ₗ[GroupRing H] GroupRing HThe universal boundary sends universalDifferential g to \([\psi(g)] - 1\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem toGroupRing_d (ψ : G →* H) (g : G) :
toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ gThe standard group-ring generator \(h-1\) appearing in Fox boundary formulas.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def augmentationGenerator (H : Type*) [Group H] (h : H) : GroupRing HThe standard augmentation generator at the identity is zero.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem augmentationGenerator_one (H : Type*) [Group H] :
augmentationGenerator H (1 : H) = 0The augmentation generator is the identity-coefficient Fox boundary.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem augmentationGenerator_eq_groupRingBoundary (H : Type*) [Group H] (h : H) :
augmentationGenerator H h = groupRingBoundary (MonoidHom.id H) hGroup-ring functoriality carries augmentation generators to augmentation generators.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingMap_augmentationGenerator {K : Type*} [Group K]
(φ : H →* K) (h : H) :
groupRingMap φ (augmentationGenerator H h) = augmentationGenerator K (φ h)