FoxDifferential.Common.CrossedDifferentialModule
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
import
- FoxDifferential.Common.CrossedDifferential
- Mathlib.Algebra.MonoidAlgebra.Basic
- Mathlib.LinearAlgebra.Finsupp.LinearCombination
- Mathlib.LinearAlgebra.Quotient.Basic
abbrev CrossedDifferentialPreModule (R G : Type*) [Ring R] : Type _ :=
G →₀ RThe free \(R\)-module on the underlying set of a group \(G\).
def crossedDifferentialRelationElement (coeff : G →* R) (g₁ g₂ : G) :
CrossedDifferentialPreModule R G :=
Finsupp.single (g₁ * g₂) 1 -
(Finsupp.single g₁ 1 + coeff g₁ • Finsupp.single g₂ 1)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.
def crossedDifferentialRelationSubmodule (coeff : G →* R) :
Submodule R (CrossedDifferentialPreModule R G) :=
Submodule.span R (Set.range fun p : G × G =>
crossedDifferentialRelationElement coeff p.1 p.2)The submodule generated by all universal crossed-differential relations.
abbrev CrossedDifferentialModule (coeff : G →* R) : Type _ :=
CrossedDifferentialPreModule R G ⧸ crossedDifferentialRelationSubmodule coeffThe universal module representing crossed differentials with coefficient homomorphism \(\mathrm{coeff}:G\to R\), viewed multiplicatively.
def universalCrossedDifferential (coeff : G →* R) (g : G) :
CrossedDifferentialModule coeff :=
(crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)The universal crossed differential \(d_{\mathrm{coeff}} : G \to \mathrm{CrossedDifferentialModule}(\mathrm{coeff})\).
theorem crossedDifferentialRelationElement_mem (coeff : G →* R) (g₁ g₂ : G) :
crossedDifferentialRelationElement coeff g₁ g₂ ∈
crossedDifferentialRelationSubmodule coeffEvery defining crossed-differential relation belongs to the relation submodule.
Show proof
by
exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩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 universalCrossedDifferential_mul (coeff : G →* R) (g₁ g₂ : G) :
universalCrossedDifferential coeff (g₁ * g₂) =
universalCrossedDifferential coeff g₁ +
coeff g₁ • universalCrossedDifferential coeff g₂The universal crossed differential satisfies the crossed product rule.
Show proof
by
have hzero :
(crossedDifferentialRelationSubmodule coeff).mkQ
(crossedDifferentialRelationElement coeff g₁ g₂) = 0 := by
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule coeff)
(x := crossedDifferentialRelationElement coeff g₁ g₂)).2
(crossedDifferentialRelationElement_mem coeff g₁ g₂)
have hzero' :
universalCrossedDifferential coeff (g₁ * g₂) -
(universalCrossedDifferential coeff g₁ +
(crossedDifferentialRelationSubmodule coeff).mkQ
(coeff g₁ • Finsupp.single g₂ 1)) = 0 := by
simpa [universalCrossedDifferential, crossedDifferentialRelationElement] using hzero
have hsmul :
(crossedDifferentialRelationSubmodule coeff).mkQ
(coeff g₁ • Finsupp.single g₂ 1) =
coeff g₁ • universalCrossedDifferential coeff g₂ := by
simpa [universalCrossedDifferential, Submodule.mkQ_apply] using
(Submodule.Quotient.mk_smul (p := crossedDifferentialRelationSubmodule coeff)
(r := coeff g₁) (x := Finsupp.single g₂ 1))
have hzero'' :
universalCrossedDifferential coeff (g₁ * g₂) -
(universalCrossedDifferential coeff g₁ +
coeff g₁ • universalCrossedDifferential coeff g₂) = 0 := by
rw [hsmul] at hzero'
exact hzero'
exact sub_eq_zero.mp hzero''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 universalCrossedDifferential_one (coeff : G →* R) :
universalCrossedDifferential coeff (1 : G) = 0The universal crossed differential vanishes at the identity.
Show proof
by
have h := universalCrossedDifferential_mul coeff (1 : G) (1 : G)
rw [map_one, one_smul] at h
have h' := congrArg
(fun z : CrossedDifferentialModule coeff => z - universalCrossedDifferential coeff (1 : G))
h
have hzero : 0 = universalCrossedDifferential coeff (1 : G) := by
simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
simpa using hzero.symmProof. 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 universalCrossedDifferential_isCrossedDifferential (coeff : G →* R) :
IsCrossedDifferential coeff (universalCrossedDifferential coeff)The universal crossed differential is itself a crossed differential.
Show proof
by
intro g₁ g₂
exact universalCrossedDifferential_mul coeff 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 crossedDifferentialModuleLiftLinear (delta : G → A) :
CrossedDifferentialPreModule R G →ₗ[R] A :=
Finsupp.linearCombination R deltaThe linear extension of a map out of G to the free crossed-differential pre-module.
theorem crossedDifferentialModuleLiftLinear_single (delta : G → A) (g : G) (r : R) :
crossedDifferentialModuleLiftLinear (R := R) delta (Finsupp.single g r) = r • delta gThe linear extension of a map evaluates on a single basis vector by scalar multiplication.
Show proof
by
simp only [crossedDifferentialModuleLiftLinear, 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 crossedDifferentialModuleLiftLinear_relationElement
(coeff : G →* R) (delta : G → A)
(hdelta : IsCrossedDifferential coeff delta) (g₁ g₂ : G) :
crossedDifferentialModuleLiftLinear (R := R) delta
(crossedDifferentialRelationElement coeff g₁ g₂) = 0A crossed differential kills each defining universal relation.
Show proof
by
simp only [crossedDifferentialModuleLiftLinear, crossedDifferentialRelationElement, Finsupp.smul_single,
smul_eq_mul, mul_one, map_sub, Finsupp.linearCombination_single, hdelta g₁ g₂, 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 crossedDifferentialRelationSubmodule_le_ker
(coeff : G →* R) (delta : G → A)
(hdelta : IsCrossedDifferential coeff delta) :
crossedDifferentialRelationSubmodule coeff ≤
LinearMap.ker (crossedDifferentialModuleLiftLinear (R := R) delta)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
crossedDifferentialModuleLiftLinear_relationElement
(A := A) coeff delta hdelta 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 crossedDifferentialModuleLift
(coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) :
CrossedDifferentialModule coeff →ₗ[R] A :=
(crossedDifferentialRelationSubmodule coeff).liftQ
(crossedDifferentialModuleLiftLinear (R := R) delta)
(crossedDifferentialRelationSubmodule_le_ker (A := A) coeff delta hdelta)The universal linear map induced by a crossed differential.
theorem crossedDifferentialModuleLift_mkQ
(coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta)
(x : CrossedDifferentialPreModule R G) :
crossedDifferentialModuleLift (A := A) coeff delta hdelta
((crossedDifferentialRelationSubmodule coeff).mkQ x) =
crossedDifferentialModuleLiftLinear (R := R) delta xThe universal lift evaluated on a quotient representative is the finite linear combination of the prescribed crossed differential on that representative.
Show proof
by
rw [crossedDifferentialModuleLift, Submodule.mkQ_apply, Submodule.liftQ_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.
□theorem crossedDifferentialModuleLift_universal
(coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) (g : G) :
crossedDifferentialModuleLift (A := A) coeff delta hdelta
(universalCrossedDifferential coeff g) = delta gThe universal lift evaluates on \(d_{\mathrm{coeff}}(g)\) as the original crossed differential.
Show proof
by
change
(crossedDifferentialRelationSubmodule coeff).liftQ
(crossedDifferentialModuleLiftLinear (R := R) delta)
(crossedDifferentialRelationSubmodule_le_ker (A := A) coeff delta hdelta)
((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g 1)) =
delta g
rw [Submodule.mkQ_apply, Submodule.liftQ_apply]
simp only [crossedDifferentialModuleLiftLinear_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 crossedDifferentialModuleHom_ext
(coeff : G →* R) {f h : CrossedDifferentialModule coeff →ₗ[R] A}
(hfh : ∀ g, f (universalCrossedDifferential coeff g) =
h (universalCrossedDifferential coeff g)) :
f = hLinear maps out of the universal crossed-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 :
((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r) :
CrossedDifferentialModule coeff) =
r • universalCrossedDifferential coeff g := by
rw [← Finsupp.smul_single_one]
rfl
change f ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r)) =
h ((crossedDifferentialRelationSubmodule coeff).mkQ (Finsupp.single g r))
simpa [hsingle, map_smul] using congrArg (fun z => r • z) (hfh 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 crossedDifferentialModuleLift_unique
(coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta)
(f : CrossedDifferentialModule coeff →ₗ[R] A)
(hf : ∀ g, f (universalCrossedDifferential coeff g) = delta g) :
f = crossedDifferentialModuleLift (A := A) coeff delta hdeltaThe universal lift is the unique linear map with prescribed values on universal differentials.
Show proof
by
apply crossedDifferentialModuleHom_ext coeff
intro g
rw [hf g, 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.
□theorem existsUnique_crossedDifferentialModuleLift
(coeff : G →* R) (delta : G → A) (hdelta : IsCrossedDifferential coeff delta) :
∃! f : CrossedDifferentialModule coeff →ₗ[R] A,
∀ g, f (universalCrossedDifferential coeff g) = delta gExistence and uniqueness of the linear map representing a crossed differential.
Show proof
by
refine ⟨crossedDifferentialModuleLift (A := A) coeff delta hdelta, ?_, ?_⟩
· intro g
exact crossedDifferentialModuleLift_universal (A := A) coeff delta hdelta g
· intro f hf
exact crossedDifferentialModuleLift_unique (A := A) coeff delta hdelta 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 crossedDifferentialOfModuleLinearMap
(coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) : G → A :=
fun g => f (universalCrossedDifferential coeff g)The crossed differential induced by a linear map out of the universal module.
theorem crossedDifferentialOfModuleLinearMap_isCrossedDifferential
(coeff : G →* R) (f : CrossedDifferentialModule coeff →ₗ[R] A) :
IsCrossedDifferential coeff (crossedDifferentialOfModuleLinearMap (A := A) coeff f)A linear map out of the universal module induces a crossed differential.
Show proof
by
intro g₁ g₂
change
f (universalCrossedDifferential coeff (g₁ * g₂)) =
f (universalCrossedDifferential coeff g₁) +
coeff g₁ • f (universalCrossedDifferential coeff g₂)
rw [universalCrossedDifferential_mul]
simp only [map_add, map_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.
□def crossedDifferentialModuleEquivLinearMap (coeff : G →* R) :
{delta : G → A // IsCrossedDifferential coeff delta} ≃
(CrossedDifferentialModule coeff →ₗ[R] A) where
toFun delta := crossedDifferentialModuleLift (A := A) coeff delta.1 delta.2
invFun f :=
⟨crossedDifferentialOfModuleLinearMap (A := A) coeff f,
crossedDifferentialOfModuleLinearMap_isCrossedDifferential (A := A) coeff f⟩
left_inv delta := by
apply Subtype.ext
funext g
exact crossedDifferentialModuleLift_universal (A := A) coeff delta.1 delta.2 g
right_inv f := by
apply crossedDifferentialModuleHom_ext coeff
intro g
exact crossedDifferentialModuleLift_universal (A := A) coeff
(crossedDifferentialOfModuleLinearMap (A := A) coeff f)
(crossedDifferentialOfModuleLinearMap_isCrossedDifferential (A := A) coeff f) gCrossed 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}\).
def monoidAlgebraToIdentityCrossedDifferentialModule :
MonoidAlgebra S G →ₗ[S]
CrossedDifferentialModule (MonoidAlgebra.of S G) :=
Finsupp.linearCombination S
(fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)The S-linear map from a group algebra to the identity crossed-differential module sending \([g]\) to the universal differential d g.
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 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\).
Show proof
by
refine Finsupp.induction_linear a ?zero ?add ?single
· simp only [MonoidAlgebra.of_apply, zero_mul, map_zero, zero_smul]
· intro a b ha hb
rw [add_mul, map_add, ha, hb, add_smul]
· intro p c
rw [MonoidAlgebra.of_apply]
rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]
change
monoidAlgebraToIdentityCrossedDifferentialModule
(Finsupp.single (p * g) (c * 1) - Finsupp.single p c) =
(MonoidAlgebra.single p c : MonoidAlgebra S G) •
universalCrossedDifferential (MonoidAlgebra.of S G) g
rw [map_sub]
change
(Finsupp.linearCombination S
(fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
(Finsupp.single (p * g) (c * 1)) -
(Finsupp.linearCombination S
(fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
(Finsupp.single p c) =
(MonoidAlgebra.single p c : MonoidAlgebra S G) •
universalCrossedDifferential (MonoidAlgebra.of S G) g
rw [Finsupp.linearCombination_single, Finsupp.linearCombination_single]
simp only [mul_one]
rw [universalCrossedDifferential_mul]
rw [smul_add, add_sub_cancel_left]
rw [MonoidAlgebra.of_apply]
rw [show (MonoidAlgebra.single p c : MonoidAlgebra S G) =
c • MonoidAlgebra.single p 1 by
simp only [MonoidAlgebra.smul_single, smul_eq_mul, mul_one]]
exact (smul_assoc c (MonoidAlgebra.single p 1 : MonoidAlgebra S G)
(universalCrossedDifferential (MonoidAlgebra.of S G) g)).symmProof. 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 identityCrossedDifferentialBoundary :
CrossedDifferentialModule (MonoidAlgebra.of S G) →ₗ[MonoidAlgebra S G]
MonoidAlgebra S G :=
crossedDifferentialModuleLift
(A := MonoidAlgebra S G)
(MonoidAlgebra.of S G)
(fun g : G => MonoidAlgebra.of S G g - 1)
(by
intro g h
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])
@[simp]The identity crossed-differential boundary sends \(d g\) to \([g] - 1\) over a group algebra.
theorem identityCrossedDifferentialBoundary_universal (g : G) :
identityCrossedDifferentialBoundary
(universalCrossedDifferential (MonoidAlgebra.of S G) g) =
MonoidAlgebra.of S G g - 1The identity crossed-differential boundary sends the universal differential at \(g\) to the group-algebra element \([g]-1\).
Show proof
by
rw [identityCrossedDifferentialBoundary, 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.
□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 xComposing the identity-boundary map with the monoid-algebra comparison has the stated value on quotient generators.
Show proof
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)).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.
□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)The 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.
Show proof
by
refine Finsupp.induction_linear a ?zero ?add ?single
· simp only [monoidAlgebraToIdentityCrossedDifferentialModule, map_zero, Finsupp.single_zero, sub_self]
· intro x y hx hy
rw [show
monoidAlgebraToIdentityCrossedDifferentialModule (S := S) (G := G) (x + y) =
monoidAlgebraToIdentityCrossedDifferentialModule x +
monoidAlgebraToIdentityCrossedDifferentialModule y by
rw [map_add]]
rw [show
identityCrossedDifferentialBoundary
(monoidAlgebraToIdentityCrossedDifferentialModule x +
monoidAlgebraToIdentityCrossedDifferentialModule y) =
identityCrossedDifferentialBoundary
(monoidAlgebraToIdentityCrossedDifferentialModule x) +
identityCrossedDifferentialBoundary
(monoidAlgebraToIdentityCrossedDifferentialModule y) by
rw [map_add]]
rw [hx, hy]
have haug :
((MonoidAlgebra.lift S S G (1 : G →* S)) (x + y : MonoidAlgebra S G)) =
((MonoidAlgebra.lift S S G (1 : G →* S)) x) +
((MonoidAlgebra.lift S S G (1 : G →* S)) y) := by
exact map_add (MonoidAlgebra.lift S S G (1 : G →* S)) x y
rw [haug]
simp only [sub_eq_add_neg, add_left_comm, add_assoc, Finsupp.single_add, neg_add_rev, add_comm]
· intro g c
rw [monoidAlgebraToIdentityCrossedDifferentialModule]
have hlin :
(Finsupp.linearCombination S
(fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
(Finsupp.single g c) =
c • universalCrossedDifferential (MonoidAlgebra.of S G) g := by
exact Finsupp.linearCombination_single
(R := S)
(v := fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g)
(c := c) (a := g)
calc
identityCrossedDifferentialBoundary
((Finsupp.linearCombination S
(fun g : G => universalCrossedDifferential (MonoidAlgebra.of S G) g))
(Finsupp.single g c)) =
identityCrossedDifferentialBoundary
(c • universalCrossedDifferential (MonoidAlgebra.of S G) g) := by
exact congrArg identityCrossedDifferentialBoundary hlin
_ =
(MonoidAlgebra.single g c : MonoidAlgebra S G) -
MonoidAlgebra.single (1 : G)
((MonoidAlgebra.lift S S G (1 : G →* S))
(Finsupp.single g c : MonoidAlgebra S G)) := by
rw [LinearMap.map_smul_of_tower,
identityCrossedDifferentialBoundary_universal]
rw [Algebra.smul_def, MonoidAlgebra.of_apply]
rw [show (algebraMap S (MonoidAlgebra S G)) c =
MonoidAlgebra.single (1 : G) c by rfl]
rw [mul_sub, mul_one, MonoidAlgebra.single_mul_single]
simp only [MonoidAlgebra.single, one_mul, mul_one, MonoidAlgebra.lift_single, MonoidHom.one_apply,
smul_eq_mul]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 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) = aOn 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.
Show proof
by
rw [idCrossedDiffBoundary_monoidAlgebraToModule,
ha]
simp only [Finsupp.single_zero, sub_zero]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 identityCrossedDifferentialBoundary_injective :
Function.Injective (identityCrossedDifferentialBoundary (S := S) (G := G))For the identity coefficient map into a group algebra, the boundary map sending \(d g\) to \([g] - 1\) is injective.
Show proof
by
intro x y hxy
revert y
refine Submodule.Quotient.induction_on
(p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) x ?_
intro x y hxy'
revert hxy'
refine Submodule.Quotient.induction_on
(p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)) y ?_
intro y hxy'
apply (Submodule.Quotient.eq
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))).2
have hdiff :
crossedDifferentialModuleLiftLinear
(R := MonoidAlgebra S G)
(fun g : G => MonoidAlgebra.of S G g - 1) (x - y) = 0 := by
have hboundary :
identityCrossedDifferentialBoundary
((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y)) =
0 := by
rw [show
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x -
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y by
rw [map_sub]]
rw [map_sub]
have hxy'' :
identityCrossedDifferentialBoundary
((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ x) =
identityCrossedDifferentialBoundary
((crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ y) := by
simpa [Submodule.mkQ_apply] using hxy'
rw [hxy'', sub_self]
simpa [identityCrossedDifferentialBoundary, crossedDifferentialModuleLift_mkQ]
using hboundary
have hmk :
(crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G)).mkQ (x - y) =
0 := by
have happ :=
monoidAlgebraToIdentityCrossedDifferentialModule_comp_identityBoundary_mkQ
(S := S) (G := G) (x - y)
rw [hdiff, map_zero] at happ
exact happ.symm
exact
(Submodule.Quotient.mk_eq_zero
(p := crossedDifferentialRelationSubmodule (MonoidAlgebra.of S G))
(x := x - y)).1 hmkProof. 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.
□