FoxDifferential.Discrete.Jacobian.Automorphism
This module develops the Fox-differential part of the theory. It records the formulas that connect generators, boundaries, Jacobians, and completed coordinates.
theorem freeGroupAutomorphismFoxJacobian_left_inverse_apply
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
(x z : X) :
(∑ y : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
e.symm.toMonoidHom x y *
freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom y z) =
(Pi.single x (1 : GroupRing H) : X → GroupRing H) zThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
have h :=
freeGroupHomFoxJacobian_comp_apply (H := H)
(X := X) (Y := X) (Z := X) ψ e.toMonoidHom e.symm.toMonoidHom x z
have hid :
e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id (FreeGroup X) := by
ext w
simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm, MonoidHom.id_apply]
rw [hid, freeGroupHomFoxJacobian_id] at h
simpa using h.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 freeGroupAutomorphismFoxJacobian_right_inverse_apply
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
(x z : X) :
(∑ y : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
e.toMonoidHom x y *
freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom y z) =
(Pi.single x (1 : GroupRing H) : X → GroupRing H) zThe Fox differential coordinate map is evaluated by the generator formula and the crossed-derivation rule.
Show proof
by
have h :=
freeGroupHomFoxJacobian_comp_apply (H := H)
(X := X) (Y := X) (Z := X) ψ e.symm.toMonoidHom e.toMonoidHom x z
have hid :
e.symm.toMonoidHom.comp e.toMonoidHom = MonoidHom.id (FreeGroup X) := by
ext w
simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom, MonoidHom.id_apply]
rw [hid, freeGroupHomFoxJacobian_id] at h
simpa using h.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 freeGroupAutomorphismFoxJacobianMatrix_left_inverse
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom)
e.symm.toMonoidHom *
freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
(1 : Matrix X X (GroupRing H))The Jacobian matrix of a free-group automorphism has the expected left inverse.
Show proof
by
apply Matrix.ext
intro x z
rw [Matrix.mul_apply]
change
(∑ j : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
e.symm.toMonoidHom x j *
freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
(1 : Matrix X X (GroupRing H)) x z
rw [show
(∑ j : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
e.symm.toMonoidHom x j *
freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
(Pi.single x (1 : GroupRing H) : X → GroupRing H) z from
freeGroupAutomorphismFoxJacobian_left_inverse_apply (H := H) ψ e x z]
by_cases hxz : x = z
· subst z
simp only [Pi.single_eq_same, Matrix.one_apply_eq]
· simp only [ne_eq, hxz, 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 freeGroupAutomorphismFoxJacobianMatrix_right_inverse
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.symm.toMonoidHom)
e.toMonoidHom *
freeGroupHomFoxJacobianMatrix (H := H) ψ e.symm.toMonoidHom =
(1 : Matrix X X (GroupRing H))The Jacobian matrix of a free-group automorphism has the expected right inverse.
Show proof
by
apply Matrix.ext
intro x z
rw [Matrix.mul_apply]
change
(∑ j : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
e.toMonoidHom x j *
freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
(1 : Matrix X X (GroupRing H)) x z
rw [show
(∑ j : X,
freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
e.toMonoidHom x j *
freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
(Pi.single x (1 : GroupRing H) : X → GroupRing H) z from
freeGroupAutomorphismFoxJacobian_right_inverse_apply (H := H) ψ e x z]
by_cases hxz : x = z
· subst z
simp only [Pi.single_eq_same, Matrix.one_apply_eq]
· simp only [ne_eq, hxz, 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.
□def freeGroupAutomorphismFoxJacobianMatrixInverse
[DecidableEq X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
Matrix X X (GroupRing H) :=
freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom) e.symm.toMonoidHomThe named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J_{\psi}(e)\), the inverse is the Jacobian of the inverse automorphism \(e^{-1}\), with coefficients pushed forward by the composite of \(\psi\) and the monoid homomorphism underlying \(e\).
theorem freeGroupAutomorphismFoxJacobianMatrixInverse_mul
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e *
freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
(1 : Matrix X X (GroupRing H))The named inverse matrix is a left inverse for the Fox Jacobian of a free-group automorphism.
Show proof
by
simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] using
freeGroupAutomorphismFoxJacobianMatrix_left_inverse (H := H) ψ eProof. 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 freeGroupAutomorphismFoxJacobianMatrix_mul_inverse
[DecidableEq X] [Fintype X]
(ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom *
freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e =
(1 : Matrix X X (GroupRing H))The named inverse matrix is a right inverse for the Fox Jacobian of a free-group automorphism.
Show proof
by
have h :=
freeGroupAutomorphismFoxJacobianMatrix_right_inverse (H := H)
(ψ.comp e.toMonoidHom) e
have hcomp :
(ψ.comp e.toMonoidHom).comp e.symm.toMonoidHom = ψ := by
ext w
simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
MulEquiv.apply_symm_apply]
rw [hcomp] at h
simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] 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.
□