abbrev HeadQuotientOfSurjective (ψ : G →* H) (hψ : Function.Surjective ψ) : Type _ :=
DifferentialModule ψ ⧸ kernelAbelianizationBoundaryRangeOfSurjective ψ hψThe quotient of \(A_{\psi}\) by the image of the head map.
def toIdentityDifferentialModule (ψ : G →* H) :
DifferentialModule ψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
lift ψ (fun g => universalDifferential (MonoidHom.id H) (ψ g)) (by
intro g₁ g₂
simpa [map_mul] using universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂))
@[simp]The canonical map from \(A_{\psi}\) to the derived module of the identity map on \(H\).
theorem toIdentityDifferentialModule_d (ψ : G →* H) (g : G) :
toIdentityDifferentialModule ψ (universalDifferential ψ g) = universalDifferential (MonoidHom.id H) (ψ g)The canonical map to the identity differential module sends the universal differential of \(g\) to the universal differential of its image.
Show proof
by
simpa [toIdentityDifferentialModule] using
lift_d (A := DifferentialModule (MonoidHom.id H)) ψ
(fun g => universalDifferential (MonoidHom.id H) (ψ g)) (by
intro g₁ g₂
simpa [map_mul] using universalDifferential_mul (MonoidHom.id H) (ψ g₁) (ψ g₂)) gProof. 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 toAugmentationIdeal_id_comp_toIdentityDifferentialModule
(ψ : G →* H) :
(toAugmentationIdeal (H := H) (MonoidHom.id H)).comp (toIdentityDifferentialModule ψ) =
toAugmentationIdeal (H := H) ψFor the identity map, composing the identity differential module with the augmentation-ideal map gives the expected augmentation boundary.
Show proof
by
apply hom_ext ψ
intro g
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, LinearMap.coe_comp, Function.comp_apply,
toIdentityDifferentialModule_d, toAugmentationIdeal_d, augmentationBoundary, groupRingBoundary, MonoidHom.id_apply,
MonoidAlgebra.of_apply]
@[simp]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) (x : KernelAbelianizationAdd ψ) :
toIdentityDifferentialModule ψ
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0Composing the surjective-case kernel-boundary map with the identity differential-module map gives the corresponding identity-module boundary value.
Show proof
by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
rw [kernelAbelianizationBoundaryLinearOfSurjective_apply]
change
(fun y : Abelianization ψ.ker =>
toIdentityDifferentialModule ψ (kernelAbelianizationBoundaryAdd ψ (Additive.ofMul y)) = 0)
(Additive.toMul x)
refine QuotientGroup.induction_on (Additive.toMul x) ?_
intro n
change toIdentityDifferentialModule ψ
(kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) = 0
have hinner :
toIdentityDifferentialModule ψ
(kernelAbelianizationBoundaryAdd ψ (Additive.ofMul (Abelianization.of n))) =
toIdentityDifferentialModule ψ (universalDifferential ψ n.1) := by
exact congrArg (toIdentityDifferentialModule ψ) (kernelAbelianizationBoundaryAdd_of ψ n)
rw [hinner, toIdentityDifferentialModule_d, n.2, universalDifferential_one]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule
(ψ : G →* H) (hψ : Function.Surjective ψ) :
kernelAbelianizationBoundaryRangeOfSurjective ψ hψ ≤
LinearMap.ker (toIdentityDifferentialModule ψ)The surjective-case kernel-boundary range lies in the kernel of the map to the identity differential module.
Show proof
by
intro y hy
rcases hy with ⟨x, rfl⟩
simpa [LinearMap.mem_ker] using
toIdentityDifferentialModule_kernelAbelianizationBoundaryLinearOfSurjective ψ hψ xProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□def headQuotientToIdentityDifferentialModule
(ψ : G →* H) (hψ : Function.Surjective ψ) :
HeadQuotientOfSurjective ψ hψ →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) :=
(kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).liftQ
(toIdentityDifferentialModule ψ)
(kernelAbelianizationBoundaryRangeOfSurjective_le_ker_toIdentityDiffModule ψ hψ)
@[simp]The quotient map \(A_{\psi} / \operatorname{im}(\mathrm{head}) \to A_{\mathrm{id}}\).
theorem headQuotientToIdentityDifferentialModule_mkQ
(ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
headQuotientToIdentityDifferentialModule ψ hψ
((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
toIdentityDifferentialModule ψ xThe map from the head quotient to the identity differential module has the stated value on quotient classes.
Show proof
by
rflProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□def headQuotientSectionOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
HeadQuotientOfSurjective ψ hψ :=
(kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ
(universalDifferential ψ (Function.surjInv hψ h))A section of \(\psi\) is viewed as a differential map into the head quotient.
theorem headQuotientSectionOfSurjective_isDifferential
(ψ : G →* H) (hψ : Function.Surjective ψ) :
IsDifferentialMap (A := HeadQuotientOfSurjective ψ hψ) (MonoidHom.id H)
(headQuotientSectionOfSurjective ψ hψ)The head-quotient section in the surjective case is a crossed differential.
Show proof
by
intro h₁ h₂
let s : H → G := Function.surjInv hψ
let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
kernelAbelianizationBoundaryRangeOfSurjective ψ hψ
have hs12 : ψ (s (h₁ * h₂)) = h₁ * h₂ := by
simpa [s] using Function.surjInv_eq hψ (h₁ * h₂)
let n : ψ.ker := ⟨s (h₁ * h₂) * (s h₁ * s h₂)⁻¹, by
calc
ψ (s (h₁ * h₂) * (s h₁ * s h₂)⁻¹)
= ψ (s (h₁ * h₂)) * (ψ (s h₁ * s h₂))⁻¹ := by simp only [mul_inv_rev, map_mul, map_inv]
_ = (h₁ * h₂) * (h₂⁻¹ * h₁⁻¹) := by
rw [hs12]
simp only [map_mul, Function.surjInv_eq hψ h₁, Function.surjInv_eq hψ h₂, mul_inv_rev, s]
_ = 1 := by simp only [mul_assoc, mul_inv_cancel_left, mul_inv_cancel]⟩
have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
have hn_mem : universalDifferential ψ n.1 ∈ q := by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
exact LinearMap.mem_range_self _ _
exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
have hs :
universalDifferential ψ (s (h₁ * h₂)) = universalDifferential ψ n.1 + universalDifferential ψ (s h₁ * s h₂) := by
have hmul := universalDifferential_mul ψ n.1 (s h₁ * s h₂)
have hψn : (MonoidAlgebra.of ℤ H (ψ n.1) : GroupRing H) = 1 := by
rw [n.2, groupRing_of_one (H := H)]
rw [hψn, one_smul] at hmul
simpa [n, s, mul_assoc] using hmul
have hq :
q.mkQ (universalDifferential ψ (s (h₁ * h₂))) = q.mkQ (universalDifferential ψ (s h₁ * s h₂)) := by
have hq' := congrArg q.mkQ hs
simpa [map_add, hn_zero] using hq'
calc
headQuotientSectionOfSurjective ψ hψ (h₁ * h₂)
= q.mkQ (universalDifferential ψ (s (h₁ * h₂))) := rfl
_ = q.mkQ (universalDifferential ψ (s h₁ * s h₂)) := hq
_ = q.mkQ (universalDifferential ψ (s h₁) + (MonoidAlgebra.of ℤ H (ψ (s h₁))) • universalDifferential ψ (s h₂)) := by
rw [universalDifferential_mul]
_ = headQuotientSectionOfSurjective ψ hψ h₁ +
(MonoidAlgebra.of ℤ H h₁ : GroupRing H) •
headQuotientSectionOfSurjective ψ hψ h₂ := by
simp only [relationSubmodule_eq_crossedDifferentialRelationSubmodule, Function.surjInv_eq hψ h₁,
MonoidAlgebra.of_apply, Submodule.mkQ_apply, Submodule.Quotient.mk_add, Submodule.Quotient.mk_smul,
headQuotientSectionOfSurjective, q, s]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□def fromIdentityDifferentialModuleOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] HeadQuotientOfSurjective ψ hψ :=
lift (MonoidHom.id H) (headQuotientSectionOfSurjective ψ hψ)
(headQuotientSectionOfSurjective_isDifferential ψ hψ)
@[simp]The inverse-direction map \(A_{\mathrm{id}} \to A_{\psi} / \operatorname{im}(\mathrm{head})\) is induced by a surjective section of \(\psi\).
theorem fromIdentityDifferentialModuleOfSurjective_d
(ψ : G →* H) (hψ : Function.Surjective ψ) (h : H) :
fromIdentityDifferentialModuleOfSurjective ψ hψ (universalDifferential (MonoidHom.id H) h) =
headQuotientSectionOfSurjective ψ hψ hThe surjective-case map from the identity differential module has the stated value on the differential generator.
Show proof
by
simpa [fromIdentityDifferentialModuleOfSurjective] using
lift_d (A := HeadQuotientOfSurjective ψ hψ) (MonoidHom.id H)
(headQuotientSectionOfSurjective ψ hψ)
(headQuotientSectionOfSurjective_isDifferential ψ hψ) hProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
(headQuotientToIdentityDifferentialModule ψ hψ).comp
(fromIdentityDifferentialModuleOfSurjective ψ hψ) =
LinearMap.idThe maps between the head quotient and the identity differential module are inverse on the displayed side.
Show proof
by
apply hom_ext (ψ := MonoidHom.id H)
intro h
rw [LinearMap.comp_apply, fromIdentityDifferentialModuleOfSurjective_d,
headQuotientSectionOfSurjective, headQuotientToIdentityDifferentialModule_mkQ,
toIdentityDifferentialModule_d]
simp only [Function.surjInv_eq hψ h, relationSubmodule_eq_crossedDifferentialRelationSubmodule,
LinearMap.id_coe, id_eq]Proof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule
(ψ : G →* H) (hψ : Function.Surjective ψ) :
(fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
(toIdentityDifferentialModule ψ) =
(kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQThe map from the identity differential module is a left inverse to the identity-differential quotient map in the surjective case.
Show proof
by
apply hom_ext (ψ := ψ)
intro g
let s : H → G := Function.surjInv hψ
let q : Submodule (GroupRing H) (DifferentialModule ψ) :=
kernelAbelianizationBoundaryRangeOfSurjective ψ hψ
let n : ψ.ker := ⟨g * (s (ψ g))⁻¹, by
simp only [MonoidHom.mem_ker, map_mul, map_inv, Function.surjInv_eq hψ (ψ g), mul_inv_cancel, s]⟩
have hn_zero : q.mkQ (universalDifferential ψ n.1) = 0 := by
have hn_mem : universalDifferential ψ n.1 ∈ q := by
letI := kernelAbelianizationModuleOfSurjective ψ hψ
rw [← kernelAbelianizationBoundaryLinearOfSurjective_of (ψ := ψ) (hψ := hψ) n]
exact LinearMap.mem_range_self _ _
exact (Submodule.Quotient.mk_eq_zero (p := q) (x := universalDifferential ψ n.1)).2 hn_mem
have hgdecomp : universalDifferential ψ g = universalDifferential ψ n.1 + universalDifferential ψ (s (ψ g)) := by
have hmul := universalDifferential_mul ψ n.1 (s (ψ g))
have hψn : (MonoidAlgebra.of ℤ H (ψ n.1) : GroupRing H) = 1 := by
rw [n.2, groupRing_of_one (H := H)]
rw [hψn, one_smul] at hmul
simpa [n, s, mul_assoc] using hmul
have hq : q.mkQ (universalDifferential ψ g) = q.mkQ (universalDifferential ψ (s (ψ g))) := by
have hq' := congrArg q.mkQ hgdecomp
simpa [map_add, hn_zero] using hq'
calc
fromIdentityDifferentialModuleOfSurjective ψ hψ
(toIdentityDifferentialModule ψ (universalDifferential ψ g))
= q.mkQ (universalDifferential ψ (s (ψ g))) := by
rw [toIdentityDifferentialModule_d, fromIdentityDifferentialModuleOfSurjective_d,
headQuotientSectionOfSurjective]
_ = q.mkQ (universalDifferential ψ g) := hq.symmProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□def headQuotientEquivIdentityDifferentialModuleOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
toLinearMap := headQuotientToIdentityDifferentialModule ψ hψ
invFun := fromIdentityDifferentialModuleOfSurjective ψ hψ
left_inv := by
intro x
have hcomp :
(fromIdentityDifferentialModuleOfSurjective ψ hψ).comp
(headQuotientToIdentityDifferentialModule ψ hψ) =
LinearMap.id := by
apply Submodule.linearMap_qext _
simpa using
fromIdentityDifferentialModuleOfSurjective_comp_toIdentityDifferentialModule ψ hψ
exact LinearMap.congr_fun hcomp x
right_inv := by
intro x
exact LinearMap.congr_fun
(headQuotientToIdentityDiffModule_fromIdentityDiffModuleOfSurjective ψ hψ) xThe quotient \(A_{\psi} / im(head)\) is canonically identified with the derived module of \(id_H\).
def headQuotientEquivAugmentationIdealOfSurjective
(ψ : G →* H) (hψ : Function.Surjective ψ) :
HeadQuotientOfSurjective ψ hψ ≃ₗ[GroupRing H] augmentationIdeal H :=
by
classical
exact
(headQuotientEquivIdentityDifferentialModuleOfSurjective ψ hψ).trans
(FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal (H := H))
@[simp]For a surjective \(\psi\), the Crowell head quotient is the augmentation ideal.
theorem headQuotientEquivAugmentationIdealOfSurjective_mkQ
(ψ : G →* H) (hψ : Function.Surjective ψ) (x : DifferentialModule ψ) :
headQuotientEquivAugmentationIdealOfSurjective ψ hψ
((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x) =
toAugmentationIdeal (H := H) ψ xThe head quotient is equivalent to the augmentation ideal and sends quotient classes to their augmentation representatives.
Show proof
by
unfold headQuotientEquivAugmentationIdealOfSurjective
rw [LinearEquiv.trans_apply]
change (FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal (H := H))
(headQuotientToIdentityDifferentialModule ψ hψ
((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ x)) = _
rw [headQuotientToIdentityDifferentialModule_mkQ]
have hid := congrArg
(fun f : DifferentialModule (MonoidHom.id H) →ₗ[GroupRing H] augmentationIdeal H =>
f (toIdentityDifferentialModule ψ x))
(FoxDifferential.identityDifferentialModuleEquivAugmentationIdeal_toLinearMap (H := H))
exact hid.trans <|
LinearMap.congr_fun (toAugmentationIdeal_id_comp_toIdentityDifferentialModule (H := H) ψ) xProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
(ψ : G →* H) (hψ : Function.Surjective ψ) :
kernelAbelianizationBoundaryRangeOfSurjective ψ hψ =
LinearMap.ker (toAugmentationIdeal (H := H) ψ)The range of the surjective-case kernel-abelianization boundary is the kernel of the map to the augmentation ideal.
Show proof
by
apply le_antisymm
· intro y hy
rcases hy with ⟨x, rfl⟩
change toAugmentationIdeal (H := H) ψ
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ x) = 0
apply Subtype.ext
exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ x
· intro y hy
have hy0 : toAugmentationIdeal (H := H) ψ y = 0 := by
simpa [LinearMap.mem_ker] using hy
have hq0 :
headQuotientEquivAugmentationIdealOfSurjective ψ hψ
((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y) = 0 := by
rw [headQuotientEquivAugmentationIdealOfSurjective_mkQ]
exact hy0
have hq : ((kernelAbelianizationBoundaryRangeOfSurjective ψ hψ).mkQ y :
HeadQuotientOfSurjective ψ hψ) = 0 := by
exact (headQuotientEquivAugmentationIdealOfSurjective ψ hψ).injective
(by simpa using hq0)
exact (Submodule.Quotient.mk_eq_zero (p := kernelAbelianizationBoundaryRangeOfSurjective ψ hψ)
(x := y)).1 hqProof. Unfold the relevant Fox differential, quotient, or finite-stage map. The asserted formula is checked on group-ring generators or quotient classes; linearity, the crossed-derivation rule, and the defining augmentation/kernel relations extend the calculation to the whole module.
□theorem exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
(ψ : G →* H) (hψ : Function.Surjective ψ) :
Function.Exact
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
(toAugmentationIdeal (H := H) ψ)Exactness at \(A_{\psi}\), formulated against the augmentation ideal.
Show proof
by
intro y
constructor
· intro hy
have hyker : y ∈ LinearMap.ker (toAugmentationIdeal (H := H) ψ) := by
simpa [LinearMap.mem_ker] using hy
rw [← kernelAbelianizationBoundaryRangeOfSurjective_eq_ker_toAugmentationIdeal
(H := H) (ψ := ψ) hψ] at hyker
exact hyker
· rintro ⟨x, rfl⟩
apply Subtype.ext
exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ xProof. 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 exact_kernelAbelianizationBoundaryLinearOfSurjective_toGroupRing
(ψ : G →* H) (hψ : Function.Surjective ψ) :
Function.Exact
(kernelAbelianizationBoundaryLinearOfSurjective ψ hψ)
(toGroupRing ψ)Exactness at \(A_{\psi}\), against the usual map \(A_{\psi}\ \to \mathbb{Z}[H]\).
Show proof
by
intro y
constructor
· intro hy
have hy' : toAugmentationIdeal (H := H) ψ y = 0 := by
apply Subtype.ext
exact hy
exact (exact_kernelAbelianizationBoundaryLinearOfSurjective_toAugmentationIdeal
(H := H) ψ hψ y).1 hy'
· rintro ⟨x, rfl⟩
exact toGroupRing_kernelAbelianizationBoundaryLinearOfSurjective (H := H) ψ hψ xProof. 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.
□