The principal declarations in this module are:
ResidueGroupRingThe residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\).
residueGroupRingScalarThe coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group homomorphism \(\psi: G \to H\).
residueGroupRingScalar_applyThe residue coefficient homomorphism sends a group element to the residue group-ring basis element of its image.
residueGroupRingBoundary_oneThe residue Fox boundary vanishes at the identity.
The residue group ring \((\mathbb{Z}/n\mathbb{Z})[H]\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u vabbrev ResidueGroupRing (n : ℕ) (H : Type*) : Type _The coefficient homomorphism \(G \to (\mathbb{Z}/n\mathbb{Z})[H]\) induced by a group homomorphism \(\psi: G \to H\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]def residueGroupRingScalar (n : ℕ) (ψ : G →* H) : G →* ResidueGroupRing n HThe residue coefficient homomorphism sends a group element to the residue group-ring basis element of its image.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]theorem residueGroupRingScalar_apply (n : ℕ) (ψ : G →* H) (g : G) :
residueGroupRingScalar n ψ g =
(MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) : ResidueGroupRing n H)The residue universal differential module attached to \(\psi : G \to H\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]abbrev ResidueDifferentialModule (n : ℕ) (ψ : G →* H) : Type _The universal residue crossed homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]def residueUniversalDifferential (n : ℕ) (ψ : G →* H) :
ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueDifferentialModule n ψ)The residue Fox boundary \(g \mapsto [\psi(g)] - 1\), bundled as a crossed homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]def residueGroupRingBoundary (n : ℕ) (ψ : G →* H) :
ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) where
toFun g := MonoidAlgebra.of (ModNCompletedCoeff n) H (ψ g) - 1
map_mul' := by
intro g h
simp only [scalarCrossedAction_apply, map_mul, MonoidAlgebra.of_apply,
MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg, add_comm,
residueGroupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
add_neg_cancel_comm_assoc]The residue Fox boundary vanishes at the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]theorem residueGroupRingBoundary_one (n : ℕ) (ψ : G →* H) :
residueGroupRingBoundary n ψ (1 : G) = 0The universal linear map induced by a residue crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]def residueDifferentialModuleLift
(ψ : G →* H)
(delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] AThe residue universal lift evaluates on the universal differential as the original crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]theorem residueDifferentialModuleLift_universal
(ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A)
(g : G) :
residueDifferentialModuleLift (A := A) n ψ delta
(residueUniversalDifferential n ψ g) =
delta gLinear maps out of the residue universal module are equal when they agree on universal residue differentials.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]theorem residueDifferentialModuleHom_ext
(ψ : G →* H)
{f h : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A}
(hfh : ∀ g, f (residueUniversalDifferential n ψ g) =
h (residueUniversalDifferential n ψ g)) :
f = hExistence and uniqueness of the linear map representing a residue crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]theorem existsUnique_residueDifferentialModuleLift
(ψ : G →* H) (delta : ScalarCrossedHom (residueGroupRingScalar n ψ) A) :
∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A,
∀ g, f (residueUniversalDifferential n ψ g) = delta gResidue crossed homomorphisms are represented by the corresponding universal residue module.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]def residueCrossedHomEquivLinearMap (ψ : G →* H) :
ScalarCrossedHom (residueGroupRingScalar n ψ) A ≃
(ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] A)The universal residue Fox boundary map from the residue differential module to the residue group ring.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]def residueToGroupRing (ψ : G →* H) :
ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n HThe universal residue Fox boundary sends \(d g\) to \([\psi(g)] - 1\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]theorem residueToGroupRing_universal (ψ : G →* H) (g : G) :
residueToGroupRing n ψ (residueUniversalDifferential n ψ g) =
residueGroupRingBoundary n ψ gExistence and uniqueness of the universal residue Fox boundary map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
open scoped BigOperators
universe u v
section Basic
variable {G : Type u} {H : Type v} [Group G] [Group H]
section UniversalProperty
variable (n : ℕ)
variable {A : Type*} [AddCommGroup A] [Module (ResidueGroupRing n H) A]theorem existsUnique_residueToGroupRing (ψ : G →* H) :
∃! f : ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H] ResidueGroupRing n H,
∀ g, f (residueUniversalDifferential n ψ g) =
residueGroupRingBoundary n ψ g