FoxDifferential.Discrete.Jacobian.ChainRule
This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.
theorem relativeFreeGroupFoxDerivative_comp_isDifferentialMap
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
IsDifferentialMap
(A := Y → GroupRing H) (ψ.comp φ)
(fun w : FreeGroup X =>
relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w))The composed derivative \(w \mapsto D(\varphi(w))\) is a crossed differential.
Show proof
by
intro u v
funext y
simp only [map_mul, relativeFreeGroupFoxDerivative_mul, MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply,
smul_eq_mul, groupRingScalar, 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.
□theorem relativeFreeGroupFoxDerivative_comp_apply
[DecidableEq X] [Fintype X] [DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) (y : Y) :
relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) y =
∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
freeGroupHomFoxJacobian (H := H) ψ φ x yThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
have h :=
crossedDifferential_comp_relativeFreeGroupFoxDerivative
(H := H) (A := Y → GroupRing H) (X := X) (Y := Y)
ψ φ (relativeFreeGroupFoxDerivative (H := H) Y ψ)
(relativeFreeGroupFoxDerivative_isDifferentialMap (H := H) Y ψ) w
have hy := congrFun h y
simpa [freeGroupHomFoxJacobian, Finset.sum_apply, Pi.smul_apply, smul_eq_mul] using hyProof. 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_comp
[DecidableEq X] [Fintype X] [DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(w : FreeGroup X) :
relativeFreeGroupFoxDerivative (H := H) Y ψ (φ w) =
fun y : Y =>
∑ x : X,
relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x *
freeGroupHomFoxJacobian (H := H) ψ φ x yFox chain rule for homomorphisms between free groups in vector form.
Show proof
by
funext y
exact relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ w yProof. 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 freeGroupHomFoxJacobian_id
[DecidableEq X]
(ψ : FreeGroup X →* H) :
freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) =
fun x : X => Pi.single x (1 : GroupRing H)The relative Fox Jacobian of the identity homomorphism is the coordinate identity family.
Show proof
by
funext x y
simp only [freeGroupHomFoxJacobian, MonoidHom.id_apply, relativeFreeGroupFoxDerivative_of]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 freeGroupHomFoxJacobian_comp_apply
[DecidableEq Y] [Fintype Y] [DecidableEq Z]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
(x : X) (z : Z) :
freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) x z =
∑ y : Y,
freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
freeGroupHomFoxJacobian (H := H) ψ φ y zThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
simpa [freeGroupHomFoxJacobian] using
relativeFreeGroupFoxDerivative_comp_apply (H := H) ψ φ (χ (FreeGroup.of x)) zProof. 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 freeGroupHomFoxJacobian_comp
[DecidableEq Y] [Fintype Y] [DecidableEq Z]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobian (H := H) ψ (φ.comp χ) =
fun x z =>
∑ y : Y,
freeGroupHomFoxJacobian (H := H) (ψ.comp φ) χ x y *
freeGroupHomFoxJacobian (H := H) ψ φ y zThe Fox Jacobian chain rule for homomorphisms between free groups is expressed in matrix form.
Show proof
by
funext x z
exact freeGroupHomFoxJacobian_comp_apply (H := H) ψ φ χ x zProof. 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 freeGroupHomFoxJacobianMatrix_id
[DecidableEq X]
(ψ : FreeGroup X →* H) :
freeGroupHomFoxJacobianMatrix (H := H) ψ (MonoidHom.id (FreeGroup X)) =
(1 : Matrix X X (GroupRing H))The relative Fox Jacobian matrix of the identity homomorphism is the identity matrix.
Show proof
by
apply Matrix.ext
intro x y
change freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
(1 : Matrix X X (GroupRing H)) x y
rw [show
freeGroupHomFoxJacobian (H := H) ψ (MonoidHom.id (FreeGroup X)) x y =
(Pi.single x (1 : GroupRing H) : X → GroupRing H) y from
congrFun (congrFun (freeGroupHomFoxJacobian_id (H := H) ψ) x) y]
by_cases hxy : x = y
· subst y
simp only [Pi.single_eq_same, Matrix.one_apply_eq]
· simp only [ne_eq, hxy, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]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 freeGroupHomFoxJacobianMatrix_comp
[DecidableEq Y] [Fintype Y] [DecidableEq Z]
(ψ : FreeGroup Z →* H)
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobianMatrix (H := H) ψ (φ.comp χ) =
freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp φ) χ *
freeGroupHomFoxJacobianMatrix (H := H) ψ φFox Jacobian chain rule, packaged as matrix multiplication.
Show proof
by
apply Matrix.ext
intro x z
simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_comp_apply, Matrix.mul_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 freeGroupHomFoxJacobianAbsolute_comp_apply
[DecidableEq Y] [Fintype Y] [DecidableEq Z]
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y)
(x : X) (z : Z) :
freeGroupHomFoxJacobianAbsolute (φ.comp χ) x z =
∑ y : Y,
groupRingMap φ (freeGroupHomFoxJacobianAbsolute χ x y) *
freeGroupHomFoxJacobianAbsolute φ y zThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
calc
freeGroupHomFoxJacobianAbsolute (φ.comp χ) x z =
∑ y : Y,
freeGroupHomFoxJacobian (H := FreeGroup Z) φ χ x y *
freeGroupHomFoxJacobianAbsolute φ y z := by
simpa [freeGroupHomFoxJacobianAbsolute] using
freeGroupHomFoxJacobian_comp_apply
(H := FreeGroup Z)
(X := X) (Y := Y) (Z := Z)
(MonoidHom.id (FreeGroup Z)) φ χ x z
_ =
∑ y : Y,
groupRingMap φ (freeGroupHomFoxJacobianAbsolute χ x y) *
freeGroupHomFoxJacobianAbsolute φ y z := by
apply Finset.sum_congr rfl
intro y _
rw [freeGroupHomFoxJacobian_eq_map_absolute_apply (H := FreeGroup Z) φ χ x y]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 freeGroupHomFoxJacobianAbsoluteMatrix_comp
[DecidableEq Y] [Fintype Y] [DecidableEq Z]
(φ : FreeGroup Y →* FreeGroup Z) (χ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobianAbsoluteMatrix (φ.comp χ) =
(freeGroupHomFoxJacobianAbsoluteMatrix χ).map (groupRingMap φ) *
freeGroupHomFoxJacobianAbsoluteMatrix φThe absolute Fox Jacobian chain rule is expressed in matrix form.
Show proof
by
apply Matrix.ext
intro x z
simp only [freeGroupHomFoxJacobianAbsoluteMatrix, freeGroupHomFoxJacobianAbsolute_comp_apply,
Matrix.mul_apply, Matrix.map_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.
□