FoxDifferential.Common.FoxBoundary
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
def coefficientFoxBoundary (coeff : G →* R) (g : G) : R :=
coeff g - 1The Fox boundary crossed differential attached to a coefficient homomorphism: \(g \mapsto \operatorname{coeff}(g)-1\).
theorem coefficientFoxBoundary_one (coeff : G →* R) :
coefficientFoxBoundary coeff 1 = 0The coefficient Fox boundary sends the identity to zero.
Show proof
by
simp only [coefficientFoxBoundary, map_one, 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 coefficientFoxBoundary_mul (coeff : G →* R) (g h : G) :
coefficientFoxBoundary coeff (g * h) =
coefficientFoxBoundary coeff g + coeff g • coefficientFoxBoundary coeff hProduct rule for the coefficient Fox boundary \(g \mapsto \operatorname{coeff}(g)-1\).
Show proof
by
rw [coefficientFoxBoundary, coefficientFoxBoundary, coefficientFoxBoundary, map_mul]
change coeff g * coeff h - 1 = coeff g - 1 + coeff g * (coeff h - 1)
rw [sub_eq_add_neg, sub_eq_add_neg, sub_eq_add_neg, mul_add, mul_neg, mul_one]
rw [show coeff g + -1 + (coeff g * coeff h + -coeff g) =
coeff g + -coeff g + (coeff g * coeff h + -1) by ac_rfl]
simp only [add_neg_cancel, zero_add]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 coefficientFoxBoundary_isCrossedDifferential (coeff : G →* R) :
IsCrossedDifferential coeff (coefficientFoxBoundary coeff)The coefficient Fox boundary is a crossed differential.
Show proof
by
intro g h
exact coefficientFoxBoundary_mul coeff g hProof. 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 foxBoundaryMap (generatorBoundary : X → R) : (X → R) →ₗ[R] R where
toFun v := ∑ x : X, v x * generatorBoundary x
map_add' v w := by
simp only [Pi.add_apply, add_mul, Finset.sum_add_distrib]
map_smul' r v := by
simp only [Pi.smul_apply, smul_eq_mul, mul_assoc, RingHom.id_apply, Finset.mul_sum]theorem foxBoundaryMap_apply (generatorBoundary : X → R) (v : X → R) :
foxBoundaryMap generatorBoundary v =
∑ x : X, v x * generatorBoundary xThe boundary map is evaluated on the canonical generators and then extended linearly to the coordinate module.
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 foxBoundaryMap_single (generatorBoundary : X → R) (x : X) :
foxBoundaryMap generatorBoundary (Pi.single x (1 : R)) = generatorBoundary xShow proof
by
rw [foxBoundaryMap_apply]
rw [Finset.sum_eq_single x]
· simp only [Pi.single_eq_same, one_mul]
· intro y _ hy
simp only [Pi.single_eq_of_ne hy, zero_mul]
· simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_mul, IsEmpty.forall_iff]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 foxBoundaryMap_freeCrossedDifferentialWithCoeff
(boundary : FreeGroup X → R)
(hboundary : IsCrossedDifferential coeff boundary)
(hgenerator :
∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
(w : FreeGroup X) :
foxBoundaryMap generatorBoundary
(freeCrossedDifferentialWithCoeff
(A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w) =
boundary wBoundary-map form of the generic free-group Fox formula: applying the Fox boundary map to the free crossed differential recovers the crossed differential with the prescribed generator values.
Show proof
by
let delta : FreeGroup X → R := fun w =>
foxBoundaryMap generatorBoundary
(freeCrossedDifferentialWithCoeff
(A := X → R) coeff (fun x : X => Pi.single x (1 : R)) w)
have hdelta : IsCrossedDifferential coeff delta :=
IsCrossedDifferential.map_linear
(freeCrossedDifferentialWithCoeff_isCrossedDifferential
(A := X → R) coeff (fun x : X => Pi.single x (1 : R)))
(foxBoundaryMap generatorBoundary)
have hdelta_generator :
∀ x : X, delta (FreeGroup.of x) = generatorBoundary x := by
intro x
simp only [freeCrossedDifferentialWithCoeff_of, foxBoundaryMap_single, delta]
have hdelta_eq :
delta = freeCrossedDifferentialWithCoeff (A := R) coeff generatorBoundary :=
freeCrossedDifferentialWithCoeff_unique
(A := R) coeff generatorBoundary delta hdelta hdelta_generator
have hboundary_eq :
boundary = freeCrossedDifferentialWithCoeff (A := R) coeff generatorBoundary :=
freeCrossedDifferentialWithCoeff_unique
(A := R) coeff generatorBoundary boundary hboundary hgenerator
change delta w = boundary w
rw [hdelta_eq, hboundary_eq]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 foxBoundaryMap_of_crossedDifferential
(delta : FreeGroup X → X → R)
(hdelta : IsCrossedDifferential coeff delta)
(hdelta_generator :
∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
(boundary : FreeGroup X → R)
(hboundary : IsCrossedDifferential coeff boundary)
(hboundary_generator :
∀ x : X, boundary (FreeGroup.of x) = generatorBoundary x)
(w : FreeGroup X) :
foxBoundaryMap generatorBoundary (delta w) = boundary wConditional boundary-map form of the generic free-group Fox formula. Any crossed differential with standard coordinate values satisfies the same boundary formula as the canonical free crossed differential.
Show proof
by
have hdelta_eq :
delta =
freeCrossedDifferentialWithCoeff
(A := X → R) coeff (fun x : X => Pi.single x (1 : R)) :=
freeCrossedDifferentialWithCoeff_unique
(A := X → R) coeff (fun x : X => Pi.single x (1 : R))
delta hdelta hdelta_generator
rw [hdelta_eq]
exact foxBoundaryMap_freeCrossedDifferentialWithCoeff
coeff generatorBoundary boundary hboundary hboundary_generator wProof. 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 foxEulerFormula_of_crossedDifferential
(delta : FreeGroup X → X → R)
(hdelta : IsCrossedDifferential coeff delta)
(hdelta_generator :
∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : R))
(w : FreeGroup X) :
coeff w - 1 =
∑ x : X, delta w x * (coeff (FreeGroup.of x) - 1)Explicit finite-sum form of the generic Fox--Euler formula for any crossed differential with standard coordinate values: \(\mathrm{coeff}(w)-1=\sum_x \delta_x(w)(\mathrm{coeff}(x)-1)\).
Show proof
by
have hboundary :=
foxBoundaryMap_of_crossedDifferential
coeff
(fun x : X => coefficientFoxBoundary coeff (FreeGroup.of x))
delta hdelta hdelta_generator
(coefficientFoxBoundary coeff)
(coefficientFoxBoundary_isCrossedDifferential coeff)
(by intro x; rfl)
w
simpa [coefficientFoxBoundary, foxBoundaryMap_apply] using hboundary.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.
□