The principal declarations in this module are:
CrossedDifferentialPreModuleThe free \(R\)-module on the underlying set of a group \(G\).
crossedDifferentialRelationElementThe universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot d(g_2)\) in the free pre-module.
crossedDifferentialRelationElement_memEvery defining crossed-differential relation belongs to the relation submodule.
universalCrossedDifferential_mulThe universal crossed differential satisfies the crossed product rule.
The free \(R\)-module on the underlying set of a group \(G\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]abbrev CrossedDifferentialPreModule (R G : Type*) [Ring R] : Type _The universal crossed-differential relation \(d(g_1g_2) = d(g_1) + \mathrm{coeff}(g_1) \cdot d(g_2)\) in the free pre-module.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]def crossedDifferentialRelationElement (coeff : G →* R) (g₁ g₂ : G) :
CrossedDifferentialPreModule R GThe submodule generated by all universal crossed-differential relations.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]def crossedDifferentialRelationSubmodule (coeff : G →* R) :
Submodule R (CrossedDifferentialPreModule R G)The universal module representing crossed differentials with coefficient homomorphism \(\mathrm{coeff}:G\to R\), viewed multiplicatively.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]abbrev CrossedDifferentialModule (coeff : G →* R) : Type _The universal crossed differential d_coeff : G -> CrossedDifferentialModule coeff.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]def universalCrossedDifferential (coeff : G →* R) (g : G) :
CrossedDifferentialModule coeffEvery defining crossed-differential relation belongs to the relation submodule.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]theorem crossedDifferentialRelationElement_mem (coeff : G →* R) (g₁ g₂ : G) :
crossedDifferentialRelationElement coeff g₁ g₂ ∈
crossedDifferentialRelationSubmodule coeffThe universal crossed differential satisfies the crossed product rule.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]theorem universalCrossedDifferential_mul (coeff : G →* R) (g₁ g₂ : G) :
universalCrossedDifferential coeff (g₁ * g₂) =
universalCrossedDifferential coeff g₁ +
coeff g₁ • universalCrossedDifferential coeff g₂The universal crossed differential \(d_{\mathrm{coeff}} : G \to \mathrm{CrossedDifferentialModule}(\mathrm{coeff})\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]def universalCrossedHom (coeff : G →* R) :
ScalarCrossedHom coeff (CrossedDifferentialModule coeff) where
toFun := universalCrossedDifferential coeff
map_mul' := by
intro g₁ g₂
change universalCrossedDifferential coeff (g₁ * g₂) =
universalCrossedDifferential coeff g₁ +
coeff g₁ • universalCrossedDifferential coeff g₂
exact universalCrossedDifferential_mul coeff g₁ g₂The universal crossed differential vanishes at the identity.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]theorem universalCrossedDifferential_one (coeff : G →* R) :
universalCrossedDifferential coeff (1 : G) = 0The linear extension of a map out of G to the free crossed-differential pre-module.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]def crossedDifferentialModuleLiftLinear (delta : G → A) :
CrossedDifferentialPreModule R G →ₗ[R] AThe linear extension of a map evaluates on a single basis vector by scalar multiplication.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]
omit [Group G] intheorem crossedDifferentialModuleLiftLinear_single (delta : G → A) (g : G) (r : R) :
crossedDifferentialModuleLiftLinear (R := R) delta (Finsupp.single g r) = r • delta gA crossed differential kills each defining universal relation.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomModuleLiftLinear_relationElement
(coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g₁ g₂ : G) :
crossedDifferentialModuleLiftLinear (R := R) delta
(crossedDifferentialRelationElement coeff g₁ g₂) = 0The relation submodule is contained in the kernel of the linear extension of a crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomRelationSubmodule_le_ker
(coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
crossedDifferentialRelationSubmodule coeff ≤
LinearMap.ker (crossedDifferentialModuleLiftLinear (R := R) delta)The universal linear map induced by a crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]def crossedHomModuleLift
(coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
CrossedDifferentialModule coeff →ₗ[R] AThe universal lift evaluated on a quotient representative is the finite linear combination of the prescribed crossed differential on that representative.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomModuleLift_mkQ
(coeff : G →* R) (delta : ScalarCrossedHom coeff A)
(x : CrossedDifferentialPreModule R G) :
crossedHomModuleLift (A := A) coeff delta
((crossedDifferentialRelationSubmodule coeff).mkQ x) =
crossedDifferentialModuleLiftLinear (R := R) delta xThe universal lift evaluates on \(d_{\mathrm{coeff}}(g)\) as the original crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomModuleLift_universal
(coeff : G →* R) (delta : ScalarCrossedHom coeff A) (g : G) :
crossedHomModuleLift (A := A) coeff delta (universalCrossedDifferential coeff g) = delta gLinear maps out of the universal crossed-differential module are equal when they agree on all universal differentials.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedDifferentialModuleHom_ext
(coeff : G →* R) {f h : CrossedDifferentialModule coeff →ₗ[R] A}
(hfh : ∀ g, f (universalCrossedDifferential coeff g) =
h (universalCrossedDifferential coeff g)) :
f = hThe universal lift is the unique linear map with prescribed values on universal differentials.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomModuleLift_unique
(coeff : G →* R) (delta : ScalarCrossedHom coeff A)
(f : CrossedDifferentialModule coeff →ₗ[R] A)
(hf : ∀ g, f (universalCrossedDifferential coeff g) = delta g) :
f = crossedHomModuleLift (A := A) coeff deltaExistence and uniqueness of the linear map representing a crossed differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem existsUnique_crossedHomModuleLift
(coeff : G →* R) (delta : ScalarCrossedHom coeff A) :
∃! f : CrossedDifferentialModule coeff →ₗ[R] A,
∀ g, f (universalCrossedDifferential coeff g) = delta gThe crossed differential induced by a linear map out of the universal module.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]def crossedHomOfModuleLinearMap
(coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) :
ScalarCrossedHom coeff A where
toFun g := f (universalCrossedDifferential coeff g)
map_mul' := by
intro g₁ g₂
change f (universalCrossedDifferential coeff (g₁ * g₂)) =
f (universalCrossedDifferential coeff g₁) +
coeff g₁ • f (universalCrossedDifferential coeff g₂)
rw [universalCrossedDifferential_mul, map_add, map_smul]The crossed homomorphism induced by a linear map evaluates the map on the universal differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]theorem crossedHomOfModuleLinearMap_apply
(coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) (g : G) :
crossedHomOfModuleLinearMap (A := A) coeff f g =
f (universalCrossedDifferential coeff g)Crossed differentials \(G \to A\) with coefficient homomorphism \(\mathrm{coeff}:G \to R\) are represented by \(R\)-linear maps out of the universal module \(\mathrm{CrossedDifferentialModule}\,\mathrm{coeff}\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section UniversalProperty
variable {A : Type*} [AddCommGroup A] [Module R A]def crossedHomModuleEquivLinearMap (coeff : G →* R) :
ScalarCrossedHom coeff A ≃ (CrossedDifferentialModule coeff →ₗ[R] A) where
toFun delta := crossedHomModuleLift (A := A) coeff delta
invFun f := crossedHomOfModuleLinearMap (A := A) coeff f
left_inv delta := by
apply CrossedHom.ext
intro g
change crossedHomModuleLift (A := A) coeff delta
(universalCrossedDifferential coeff g) = delta g
exact crossedHomModuleLift_universal (A := A) coeff delta g
right_inv f := by
apply crossedDifferentialModuleHom_ext coeff
intro g
change crossedHomModuleLift (A := A) coeff
(crossedHomOfModuleLinearMap (A := A) coeff f)
(universalCrossedDifferential coeff g) =
f (universalCrossedDifferential coeff g)
exact crossedHomModuleLift_universal (A := A) coeff
(crossedHomOfModuleLinearMap (A := A) coeff f) gThe S-linear map from a group algebra to the identity crossed-differential module sending \([g]\) to the universal differential d g.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]def monoidAlgebraToIdentityCrossedDifferentialModule :
MonoidAlgebra S G →ₗ[S]
CrossedDifferentialModule (MonoidAlgebra.of S G)A group-algebra basis term maps to its coefficient times the corresponding universal differential.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem monoidAlgebraToIdentityCrossedDifferentialModule_single (g : G) (a : S) :
monoidAlgebraToIdentityCrossedDifferentialModule
(MonoidAlgebra.single g a : MonoidAlgebra S G) =
a • universalCrossedDifferential (MonoidAlgebra.of S G) gThe linear map from the group algebra to the identity crossed-differential module sends \(a([g]-1)\) to \(a\) acting on the universal differential of \(g\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one
(a : MonoidAlgebra S G) (g : G) :
monoidAlgebraToIdentityCrossedDifferentialModule
(a * (MonoidAlgebra.of S G g - 1)) =
a • universalCrossedDifferential (MonoidAlgebra.of S G) gThe group-algebra boundary g ↦ [g] - 1, bundled as a scalar crossed homomorphism.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]def identityGroupAlgebraCrossedHom :
ScalarCrossedHom (MonoidAlgebra.of S G) (MonoidAlgebra S G) where
toFun g := MonoidAlgebra.of S G g - 1
map_mul' := by
intro g h
change MonoidAlgebra.of S G (g * h) - 1 =
(MonoidAlgebra.of S G g - 1) +
MonoidAlgebra.of S G g • (MonoidAlgebra.of S G h - 1)
simp only [map_mul, MonoidAlgebra.of_apply,
MonoidAlgebra.single_mul_single, mul_one, sub_eq_add_neg, smul_eq_mul, mul_add,
mul_neg, add_comm, add_assoc, neg_add_cancel_left]The identity-coefficient crossed homomorphism sends a group element to its group-like term minus one.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem identityGroupAlgebraCrossedHom_apply (g : G) :
identityGroupAlgebraCrossedHom (S := S) (G := G) g =
MonoidAlgebra.of S G g - 1The identity crossed-differential boundary sends \(d g\) to \([g] - 1\) over a group algebra.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]def identityCrossedDifferentialBoundary :
CrossedDifferentialModule (MonoidAlgebra.of S G) →ₗ[MonoidAlgebra S G]
MonoidAlgebra S GThe identity crossed-differential boundary sends the universal differential at \(g\) to the group-algebra element \([g]-1\).
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem identityCrossedDifferentialBoundary_universal (g : G) :
identityCrossedDifferentialBoundary
(universalCrossedDifferential (MonoidAlgebra.of S G) g) =
MonoidAlgebra.of S G g - 1Composing the identity-boundary map with the monoid-algebra comparison has the stated value on quotient generators.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ
(x : CrossedDifferentialPreModule (MonoidAlgebra S G) G) :
monoidAlgebraToIdentityCrossedDifferentialModule
(crossedDifferentialModuleLiftLinear
(R := MonoidAlgebra S G)
(fun g : G => MonoidAlgebra.of S G g - 1) x) =
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x := by
refine Finsupp.induction_linear x ?zero ?add ?single
· simp only [crossedDifferentialModuleLiftLinear, MonoidAlgebra.of_apply, map_zero]
· intro x y hx hy
rw [map_add, map_add]
exact congrArg₂ (· + ·)
(by simpa [MonoidAlgebra.of_apply] using hx)
(by simpa [MonoidAlgebra.of_apply] using hy)
· intro g a
rw [crossedDifferentialModuleLiftLinear_single]
change
monoidAlgebraToIdentityCrossedDifferentialModule
(a * (MonoidAlgebra.of S G g - 1)) =
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ
(Finsupp.single g a)
rw [monoidAlgebraToIdentityCrossedDifferentialModule_mul_sub_one]
rw [← Finsupp.smul_single_one]
exact
(Submodule.Quotient.mk_smul
(p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))
(r := a) (x := Finsupp.single g 1)).symmThe boundary of the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is the augmentation-zero part of the group-algebra element.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem idCrossedDiffBoundary_monoidAlgebraToModule
(a : MonoidAlgebra S G) :
identityCrossedDifferentialBoundary
(monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) =
a -
MonoidAlgebra.single (1 : G)
((MonoidAlgebra.lift S S G (1 : G →* S)) a)On the augmentation ideal, the additive lift \(\sum a_g [g] \mapsto \sum a_g d g\) is a right inverse to the identity crossed-differential boundary.
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
{a : MonoidAlgebra S G}
(ha : (MonoidAlgebra.lift S S G (1 : G →* S)) a = 0) :
identityCrossedDifferentialBoundary
(monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) a) = aFor the identity coefficient map into a group algebra, the boundary map sending \(d g\) to \([g]
Surrounding namespaces, section variables, and local commands at this declaration.
namespace FoxDifferential
noncomputable section
variable {R G : Type*} [Ring R] [Group G]
section MonoidAlgebraIdentityBoundary
variable {S : Type*} [CommRing S]theorem identityCrossedDifferentialBoundary_injective :
Function.Injective (identityCrossedDifferentialBoundary (S := S) (G := G))