FoxDifferential.Discrete.Jacobian.Basic
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
Imported by
def freeGroupHomFoxJacobian
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
X → Y → GroupRing H :=
fun x =>
relativeFreeGroupFoxDerivative (H := H) Y ψ (φ (FreeGroup.of x))The relative Fox Jacobian of \(\varphi : \mathrm{FreeGroup}(X) \to \mathrm{FreeGroup}(Y)\), with coefficients pushed forward by \(\psi : \mathrm{FreeGroup}(Y) \to H\). The row indexed by \(x : X\) is the relative Fox derivative of the substituted generator \(\varphi(x)\) with respect to the \(Y\)-generators.
def freeGroupHomFoxJacobianMatrix
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
Matrix X Y (GroupRing H) :=
freeGroupHomFoxJacobian (H := H) ψ φThe relative Fox Jacobian, packaged as a matrix.
theorem freeGroupHomFoxJacobianMatrix_apply
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(x : X) (y : Y) :
freeGroupHomFoxJacobianMatrix (H := H) ψ φ x y =
freeGroupHomFoxJacobian (H := H) ψ φ x yThe 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 freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobian (H := H) ψ φ =
freeCrossedDifferentialWithCoeffJacobian (X := X) (Y := Y) (groupRingScalar ψ) φThe usual relative Fox Jacobian is the coefficient-generic free crossed-differential Jacobian specialized to the group-ring coefficient homomorphism.
Show proof
by
funext x y
simp only [freeGroupHomFoxJacobian, freeCrossedDifferentialWithCoeffJacobian,
freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative]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_eq_freeCrossedDifferentialWithCoeffJacobianMatrix
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
freeCrossedDifferentialWithCoeffJacobianMatrix
(X := X) (Y := Y) (groupRingScalar ψ) φMatrix form of the comparison between the usual relative Fox Jacobian and the coefficient-generic free crossed-differential Jacobian.
Show proof
by
apply Matrix.ext
intro x y
simp only [freeGroupHomFoxJacobianMatrix_apply,
freeGroupHomFoxJacobian_eq_freeCrossedDifferentialWithCoeffJacobian,
freeCrossedDifferentialWithCoeffJacobianMatrix_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 freeGroupHomFoxJacobianAbsolute
[DecidableEq Y]
(φ : FreeGroup X →* FreeGroup Y) :
X → Y → GroupRing (FreeGroup Y) :=
freeGroupHomFoxJacobian (H := FreeGroup Y) (MonoidHom.id (FreeGroup Y)) φThe absolute Fox Jacobian of a homomorphism between free groups.
def freeGroupHomFoxJacobianAbsoluteMatrix
[DecidableEq Y]
(φ : FreeGroup X →* FreeGroup Y) :
Matrix X Y (GroupRing (FreeGroup Y)) :=
freeGroupHomFoxJacobianAbsolute φThe absolute Fox Jacobian, packaged as a matrix.
theorem freeGroupHomFoxJacobianAbsoluteMatrix_apply
[DecidableEq Y]
(φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
freeGroupHomFoxJacobianAbsoluteMatrix φ x y =
freeGroupHomFoxJacobianAbsolute φ x yThe 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 freeGroupHomFoxJacobianAbsolute_id
[DecidableEq X] :
freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) =
fun x : X => Pi.single x (1 : GroupRing (FreeGroup X))The absolute Fox Jacobian of the identity homomorphism is the coordinate identity family.
Show proof
by
funext x y
simp only [freeGroupHomFoxJacobianAbsolute, 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 freeGroupHomFoxJacobianAbsoluteMatrix_id
[DecidableEq X] :
freeGroupHomFoxJacobianAbsoluteMatrix (MonoidHom.id (FreeGroup X)) =
(1 : Matrix X X (GroupRing (FreeGroup X)))The absolute Fox Jacobian matrix of the identity homomorphism is the identity matrix.
Show proof
by
apply Matrix.ext
intro x y
change freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
(1 : Matrix X X (GroupRing (FreeGroup X))) x y
rw [show
freeGroupHomFoxJacobianAbsolute (MonoidHom.id (FreeGroup X)) x y =
(Pi.single x (1 : GroupRing (FreeGroup X)) : X → GroupRing (FreeGroup X)) y from
congrFun (congrFun freeGroupHomFoxJacobianAbsolute_id 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 freeGroupHomFoxJacobian_mapDomain_apply
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (η : H →* K)
(φ : FreeGroup X →* FreeGroup Y) (x : X) (y : Y) :
freeGroupHomFoxJacobian (H := K) (η.comp ψ) φ x y =
groupRingMap η (freeGroupHomFoxJacobian (H := H) ψ φ x y)The Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
simp only [freeGroupHomFoxJacobian, relativeFreeGroupFoxDerivative_mapDomain_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 freeGroupHomFoxJacobianMatrix_mapDomain
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (η : H →* K)
(φ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobianMatrix (H := K) (η.comp ψ) φ =
(freeGroupHomFoxJacobianMatrix (H := H) ψ φ).map (groupRingMap η)Fox Jacobians are natural under coefficient push-forward, matrix form.
Show proof
by
apply Matrix.ext
intro x y
simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_mapDomain_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.
□theorem freeGroupHomFoxJacobian_eq_map_absolute_apply
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
(x : X) (y : Y) :
freeGroupHomFoxJacobian (H := H) ψ φ x y =
groupRingMap ψ (freeGroupHomFoxJacobianAbsolute φ x y)The Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
simpa [freeGroupHomFoxJacobianAbsolute] using
freeGroupHomFoxJacobian_mapDomain_apply
(H := FreeGroup Y) (K := H)
(MonoidHom.id (FreeGroup Y)) ψ φ x 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 freeGroupHomFoxJacobianMatrix_eq_map_absolute
[DecidableEq Y]
(ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y) :
freeGroupHomFoxJacobianMatrix (H := H) ψ φ =
(freeGroupHomFoxJacobianAbsoluteMatrix φ).map (groupRingMap ψ)Matrix form of the absolute-to-relative comparison for Fox Jacobians.
Show proof
by
apply Matrix.ext
intro x y
simp only [freeGroupHomFoxJacobianMatrix, freeGroupHomFoxJacobian_eq_map_absolute_apply,
freeGroupHomFoxJacobianAbsoluteMatrix, 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.
□