FoxDifferential.Discrete.DifferentialModule.Boundary
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
def groupRingBoundary (ψ : G →* H) (g : G) : GroupRing H :=
MonoidAlgebra.of ℤ H (ψ g) - 1The standard map \(G \to \mathbb{Z}[H]\), \(g \mapsto \psi(g)-1\) is viewed as a differential map.
theorem groupRingBoundary_one (ψ : G →* H) :
groupRingBoundary ψ (1 : G) = 0The Fox boundary vanishes at the identity.
Show proof
by
simp only [groupRingBoundary, map_one, groupRing_of_one (H := H), 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 groupRingBoundary_eq_zero_of_mem_ker (ψ : G →* H) {g : G} (hg : ψ g = 1) :
groupRingBoundary ψ g = 0The Fox boundary is zero on elements in the kernel of \(\psi\).
Show proof
by
rw [groupRingBoundary, hg, groupRing_of_one (H := H)]
simp only [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 groupRingBoundary_subtype_ker (ψ : G →* H) (g : ψ.ker) :
groupRingBoundary ψ g = 0The Fox boundary vanishes on the kernel subgroup of \(\psi\).
Show proof
groupRingBoundary_eq_zero_of_mem_ker (ψ := ψ) g.2Proof. 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 groupRingBoundary_isDifferential (ψ : G →* H) :
IsDifferentialMap (A := GroupRing H) ψ (groupRingBoundary ψ)The Fox boundary is itself a crossed differential.
Show proof
by
intro g₁ g₂
simp only [groupRingBoundary, map_mul, MonoidAlgebra.of_apply, MonoidAlgebra.single_mul_single, mul_one,
sub_eq_add_neg, add_comm, groupRingScalar_apply, smul_eq_mul, mul_add, mul_neg, add_assoc,
add_neg_cancel_comm_assoc]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 groupRingMap_groupRingBoundary {K : Type*} [Group K]
(φ : H →* K) (ψ : G →* H) (g : G) :
groupRingMap φ (groupRingBoundary ψ g) = groupRingBoundary (φ.comp ψ) gGroup-ring functoriality carries Fox boundaries to Fox boundaries.
Show proof
by
simp only [groupRingBoundary, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one,
MonoidHom.coe_comp, Function.comp_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 toGroupRing (ψ : G →* H) : DifferentialModule ψ →ₗ[GroupRing H] GroupRing H :=
lift (A := GroupRing H) ψ (groupRingBoundary ψ) (groupRingBoundary_isDifferential ψ)The universal boundary map \(A_{\psi}\ \to \mathbb{Z}[H]\), \(universalDifferential(g) \mapsto \psi(g) - 1\).
theorem toGroupRing_d (ψ : G →* H) (g : G) :
toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ gThe universal boundary sends universalDifferential g to \([\psi(g)] - 1\).
Show proof
by
simpa [toGroupRing] using
lift_d (A := GroupRing H) ψ (groupRingBoundary ψ) (groupRingBoundary_isDifferential ψ) 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 augmentationGenerator_one (H : Type*) [Group H] :
augmentationGenerator H (1 : H) = 0The standard augmentation generator at the identity is zero.
Show proof
by
simp only [augmentationGenerator, groupRing_of_one (H := H), 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 augmentationGenerator_eq_groupRingBoundary (H : Type*) [Group H] (h : H) :
augmentationGenerator H h = groupRingBoundary (MonoidHom.id H) hThe augmentation generator is the identity-coefficient Fox boundary.
Show proof
rflProof. 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 groupRingMap_augmentationGenerator {K : Type*} [Group K]
(φ : H →* K) (h : H) :
groupRingMap φ (augmentationGenerator H h) = augmentationGenerator K (φ h)Group-ring functoriality carries augmentation generators to augmentation generators.
Show proof
by
simp only [augmentationGenerator, MonoidAlgebra.of_apply, map_sub, groupRingMap_single, map_one]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.
□