The principal declarations in this module are:
GroupRingThe integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra.
groupRingMapA group homomorphism induces the corresponding group-ring map.
groupRingMap_ofThe induced group-ring map sends monomials to monomials.
groupRingMap_singleThe induced group-ring map sends Finsupp.single basis terms along the group map.
The integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable sectionabbrev GroupRing (H : Type*) : Type _A group homomorphism induces the corresponding group-ring map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable sectiondef groupRingMap {H K : Type*} [Group H] [Group K] (φ : H →* K) :
GroupRing H →+* GroupRing KThe induced group-ring map sends monomials to monomials.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable sectiontheorem groupRingMap_of {H K : Type*} [Group H] [Group K]
(φ : H →* K) (h : H) :
groupRingMap φ (MonoidAlgebra.of ℤ H h) =
MonoidAlgebra.of ℤ K (φ h)The induced group-ring map sends Finsupp.single basis terms along the group map.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable sectiontheorem groupRingMap_single {H K : Type*} [Group H] [Group K]
(φ : H →* K) (h : H) (z : ℤ) :
groupRingMap φ (MonoidAlgebra.single h z : GroupRing H) =
(MonoidAlgebra.single (φ h) z : GroupRing K)The free \(\mathbb{Z}[H]\)-module on the underlying set of G.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable sectionabbrev DifferentialPreModule (H : Type*) (G : Type*) : Type _The group-ring monomial attached to the group identity is the ring identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRing_of_one : (MonoidAlgebra.of ℤ H (1 : H) : GroupRing H) = 1The pre-module element imposing the Fox product relation \(d(g_1g_2)=d(g_1)+\psi(g_1)\,d(g_2)\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def relationElement (ψ : G →* H) (g₁ g₂ : G) : DifferentialPreModule H GThe submodule generated by the Fox differential relations.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def relationSubmodule (ψ : G →* H) : Submodule (GroupRing H) (DifferentialPreModule H G)The differential module is the universal module receiving the crossed Fox differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]abbrev DifferentialModule (ψ : G →* H) : Type _The universal differential \(G \to A_{\psi}\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def universalDifferential (ψ : G →* H) (g : G) : DifferentialModule ψEvery defining Fox relation belongs to the relation submodule.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem relationElement_mem (ψ : G →* H) (g₁ g₂ : G) :
relationElement ψ g₁ g₂ ∈ relationSubmodule ψThe universal differential satisfies the Fox product rule.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem universalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
universalDifferential ψ (g₁ * g₂) =
universalDifferential ψ g₁ +
(MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂The universal differential vanishes at the group identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem universalDifferential_one (ψ : G →* H) : universalDifferential ψ (1 : G) = 0The universal differentials of \(g\) and \(g^{-1}\) add to zero with the Fox twist.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem universalDifferential_mul_inv_right (ψ : G →* H) (g : G) :
universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ = 0Conjugation by \(g\) acts on the differential of a kernel element by the \(\psi(g)\) scalar.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem universalDifferential_conj_of_mem_ker (ψ : G →* H) (g n : G) (hn : ψ n = 1) :
universalDifferential ψ (g * n * g⁻¹) = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential
ψ nThe coefficient homomorphism \(G \to \mathbb{Z}[H]\) induced by \(\psi: G \to H\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def groupRingScalar (ψ : G →* H) : G →* GroupRing HThe group-ring scalar associated to g is the basis element supported at ψ g.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem groupRingScalar_apply (ψ : G →* H) (g : G) :
groupRingScalar ψ g = (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H)The discrete Fox relation is the coefficient-ring-agnostic crossed-differential relation for the group-ring coefficient homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem relationElement_eq_crossedDifferentialRelationElement
(ψ : G →* H) (g₁ g₂ : G) :
relationElement ψ g₁ g₂ =
crossedDifferentialRelationElement (groupRingScalar ψ) g₁ g₂The discrete Fox relation submodule agrees with the generic crossed-differential relation submodule for the group-ring coefficient homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem relationSubmodule_eq_crossedDifferentialRelationSubmodule (ψ : G →* H) :
relationSubmodule ψ =
crossedDifferentialRelationSubmodule (groupRingScalar ψ)The discrete universal differential module is linearly equivalent to the generic universal crossed-differential module for the group-ring coefficient homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def differentialModuleEquivCrossedDifferentialModule (ψ : G →* H) :
DifferentialModule ψ ≃ₗ[GroupRing H]
CrossedDifferentialModule (groupRingScalar ψ)The generic universal crossed-differential module for the group-ring scalar homomorphism associated to \(\psi\) is linearly equivalent to the discrete universal differential module \(A_{\psi}\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]def crossedDifferentialModuleEquivDifferentialModule (ψ : G →* H) :
CrossedDifferentialModule (groupRingScalar ψ) ≃ₗ[GroupRing H]
DifferentialModule ψThe discrete universal differential is the generic universal crossed differential under the canonical linear equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem differentialModuleEquivCrossedDifferentialModule_d
(ψ : G →* H) (g : G) :
differentialModuleEquivCrossedDifferentialModule ψ (universalDifferential ψ g) =
universalCrossedDifferential (groupRingScalar ψ) gThe generic universal crossed differential maps back to the discrete universal differential under the canonical linear equivalence.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {H G : Type*} [Group H] [Group G]theorem crossedDifferentialModuleEquivDifferentialModule_universal
(ψ : G →* H) (g : G) :
crossedDifferentialModuleEquivDifferentialModule ψ
(universalCrossedDifferential (groupRingScalar ψ) g) =
universalDifferential ψ g