abbrev IsDifferentialMap (ψ : G →* H) (δ : G → A) : Prop :=
IsCrossedDifferential (groupRingScalar ψ) δA \(\psi\)-differential map is a map satisfying the Fox Leibniz rule.
def liftLinear (δ : G → A) : DifferentialPreModule H G →ₗ[GroupRing H] A :=
Finsupp.linearCombination (GroupRing H) δThe linear map out of the free pre-module determined by \(\delta\).
theorem liftLinear_single (δ : G → A) (g : G) (r : GroupRing H) :
liftLinear δ (Finsupp.single g r) = r • δ gThe linear extension of a map evaluates on a single basis vector by scalar multiplication.
Show proof
by
simp only [liftLinear, Finsupp.linearCombination_single]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem liftLinear_relationElement
(ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) (g₁ g₂ : G) :
liftLinear δ (relationElement ψ g₁ g₂) = 0A crossed differential kills each defining relation of the universal differential module.
Show proof
by
simp only [liftLinear, relationElement, MonoidAlgebra.of_apply, Finsupp.smul_single, smul_eq_mul, mul_one,
map_sub, Finsupp.linearCombination_single, hδ g₁ g₂, groupRingScalar_apply, smul_add, one_smul, map_add, sub_self]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem relationSubmodule_le_ker
(ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
relationSubmodule ψ ≤ LinearMap.ker (liftLinear δ)The relation submodule is contained in the kernel of the linear extension of a crossed differential.
Show proof
by
refine Submodule.span_le.2 ?_
rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
simpa [LinearMap.mem_ker] using liftLinear_relationElement (A := A) ψ δ hδ g₁ g₂Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□def lift (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
DifferentialModule ψ →ₗ[GroupRing H] A :=
(relationSubmodule ψ).liftQ (liftLinear δ) (relationSubmodule_le_ker (A := A) ψ δ hδ)A crossed differential factors uniquely through the universal differential module as a linear map.
theorem lift_d (ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) (g : G) :
lift ψ δ hδ (universalDifferential ψ g) = δ gThe universal lift evaluates on universalDifferential g as the original crossed differential.
Show proof
by
change
(relationSubmodule ψ).liftQ (liftLinear δ)
(relationSubmodule_le_ker (A := A) ψ δ hδ)
((relationSubmodule ψ).mkQ (Finsupp.single g 1)) = δ g
rw [Submodule.mkQ_apply, Submodule.liftQ_apply]
simp only [liftLinear_single, one_smul]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem hom_ext (ψ : G →* H) {f g : DifferentialModule ψ →ₗ[GroupRing H] A}
(hfg : ∀ g', f (universalDifferential ψ g') = g (universalDifferential ψ g')) : f = gLinear maps out of the universal differential module are equal when they agree on all universal differentials.
Show proof
by
apply Submodule.linearMap_qext _
apply Finsupp.lhom_ext
intro g' r
have hsingle : ((relationSubmodule ψ).mkQ (Finsupp.single g' r) : DifferentialModule ψ) =
r • universalDifferential ψ g' := by
rw [← Finsupp.smul_single_one]
rfl
change f ((relationSubmodule ψ).mkQ (Finsupp.single g' r)) =
g ((relationSubmodule ψ).mkQ (Finsupp.single g' r))
rw [hsingle]
simpa [map_smul] using congrArg (fun z => r • z) (hfg g')Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem lift_unique
(ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ)
(f : DifferentialModule ψ →ₗ[GroupRing H] A)
(hf : ∀ g, f (universalDifferential ψ g) = δ g) :
f = lift (A := A) ψ δ hδThe universal lift is the unique linear map with prescribed values on universal differentials.
Show proof
by
apply hom_ext ψ
intro g
rw [hf g, lift_d]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□theorem existsUnique_lift
(ψ : G →* H) (δ : G → A) (hδ : IsDifferentialMap (A := A) ψ δ) :
∃! f : DifferentialModule ψ →ₗ[GroupRing H] A, ∀ g, f (universalDifferential ψ g) = δ gExistence and uniqueness of the linear map representing a discrete Fox crossed differential.
Show proof
by
refine ⟨lift (A := A) ψ δ hδ, ?_, ?_⟩
· intro g
exact lift_d (A := A) ψ δ hδ g
· intro f hf
exact lift_unique (A := A) ψ δ hδ f hfProof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□def crossedDifferentialOfLinearMap
(ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) : G → A :=
fun g => f (universalDifferential ψ g)The crossed differential induced by a linear map out of the universal differential module.
theorem crossedDifferentialOfLinearMap_isDifferentialMap
(ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) :
IsDifferentialMap (A := A) ψ (crossedDifferentialOfLinearMap (A := A) ψ f)A linear map out of the universal differential module induces a crossed differential.
Show proof
by
intro g₁ g₂
simp only [crossedDifferentialOfLinearMap, relationSubmodule_eq_crossedDifferentialRelationSubmodule,
universalDifferential_mul, MonoidAlgebra.of_apply, map_add, map_smul, groupRingScalar_apply]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□def crossedDifferentialEquivLinearMap (ψ : G →* H) :
{δ : G → A // IsDifferentialMap (A := A) ψ δ} ≃
(DifferentialModule ψ →ₗ[GroupRing H] A) where
toFun δ := lift (A := A) ψ δ.1 δ.2
invFun f :=
⟨crossedDifferentialOfLinearMap (A := A) ψ f,
crossedDifferentialOfLinearMap_isDifferentialMap (A := A) ψ f⟩
left_inv δ := by
apply Subtype.ext
funext g
exact lift_d (A := A) ψ δ.1 δ.2 g
right_inv f := by
apply hom_ext ψ
intro g
exact lift_d (A := A) ψ (crossedDifferentialOfLinearMap (A := A) ψ f)
(crossedDifferentialOfLinearMap_isDifferentialMap (A := A) ψ f) gDiscrete Fox crossed differentials \(G \to A\) with respect to \(\psi: G \to H\) are represented by \(\mathbb{Z}[H]\)-linear maps out of the universal differential module \(A_{\psi}\).
theorem crossedDifferentialEquivLinearMap_eq_generic
(ψ : G →* H)
(δ : {δ : G → A // IsDifferentialMap (A := A) ψ δ}) :
crossedDifferentialEquivLinearMap (A := A) ψ δ =
(crossedDifferentialModuleEquivLinearMap
(A := A) (groupRingScalar ψ) δ).comp
(differentialModuleEquivCrossedDifferentialModule ψ).toLinearMapThe compatibility between the discrete representation theorem and the generic crossed-differential-module representation theorem.
Show proof
by
apply hom_ext ψ
intro g
change
lift (A := A) ψ δ.1 δ.2 (universalDifferential ψ g) =
crossedDifferentialModuleLift (A := A) (groupRingScalar ψ) δ.1 δ.2
(universalCrossedDifferential (groupRingScalar ψ) g)
rw [lift_d, crossedDifferentialModuleLift_universal]Proof. Use the algebraic crossed-differential rule. The values on generators determine the map, and the product, inverse, quotient, and power formulas follow from the rule \(d(xy)=d(x)+x d(y)\) by induction and linearity. Universal-module and lift statements are checked on basis elements and then descend through the defining crossed-differential relations. Equality, naturality, and matrix formulas follow from generator or basis extensionality, while augmentation-kernel claims use the Fox fundamental formula.
□