FoxDifferential.Discrete.Naturality
This module develops Fox differentials and completed Fox coordinates for free, profinite, and pro-\(C\) group constructions.
def relativeFreeFoxCoordinatesMap :
RelativeFreeFoxCoordinates (H := H) X → RelativeFreeFoxCoordinates (H := K) X :=
fun a x => groupRingMap φ (a x)A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward.
theorem relativeFreeFoxCoordinatesMap_apply
(a : RelativeFreeFoxCoordinates (H := H) X) (x : X) :
relativeFreeFoxCoordinatesMap (X := X) φ a x = groupRingMap φ (a x)The Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
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 relativeFreeGroupFoxDerivative_mapDomain (w : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w =
relativeFreeFoxCoordinatesMap (X := X) φ
(relativeFreeGroupFoxDerivative (H := H) X ψ w)Relative Fox derivatives are natural under coefficient push-forward.
Show proof
by
let delta : FreeGroup X → RelativeFreeFoxCoordinates (H := K) X :=
fun w => relativeFreeFoxCoordinatesMap (X := X) φ
(relativeFreeGroupFoxDerivative (H := H) X ψ w)
have hdelta :
IsDifferentialMap
(A := RelativeFreeFoxCoordinates (H := K) X) (φ.comp ψ) delta := by
intro u v
funext x
simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_mul, MonoidAlgebra.of_apply,
Pi.add_apply, Pi.smul_apply, smul_eq_mul, map_add, map_mul, groupRingMap_single, groupRingScalar,
MonoidHom.coe_comp, Function.comp_apply, relativeFreeFoxCoordinatesMap, delta]
have hbasis :
∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing K) := by
intro x
funext y
by_cases hxy : x = y
· subst y
simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of, Pi.single_eq_same, map_one,
delta]
· simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of, ne_eq, hxy,
not_false_eq_true, Pi.single_eq_of_ne', map_zero, delta]
exact (congrFun
(relativeFreeGroupFoxDerivative_unique (H := K) X (φ.comp ψ) delta hdelta hbasis) w).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 relativeFreeGroupFoxDerivative_mapDomain_apply (w : FreeGroup X) (x : X) :
relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w x =
groupRingMap φ (relativeFreeGroupFoxDerivative (H := H) X ψ w x)Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.
Show proof
by
have h := congrFun
(relativeFreeGroupFoxDerivative_mapDomain (H := H) (K := K) ψ φ w) x
simpa [relativeFreeFoxCoordinatesMap] using 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.
□