FoxDifferential/Discrete/Jacobian/Automorphism.lean
1import FoxDifferential.Discrete.Jacobian.ChainRule
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Discrete/Jacobian/Automorphism.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete group-ring Fox calculus
14Ordinary Fox derivatives over group rings are developed through augmentation, relative differential modules, coordinates, Jacobians, and chain rules.
15-/
16namespace FoxDifferential
18noncomputable section
20namespace FoxCalculus
22open scoped BigOperators
24universe u v w z t
26variable {H : Type w} [Group H]
27variable {X : Type u} {Y : Type v}
28/-- The Fox Jacobian of a free-group automorphism has a left inverse, with the expected
29coefficient push-forward. -/
31 [DecidableEq X] [Fintype X]
32 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
33 (x z : X) :
34 (∑ y : X,
35 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
36 e.symm.toMonoidHom x y *
37 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom y z) =
39 have h :=
40 freeGroupHomFoxJacobian_comp_apply (H := H)
41 (X := X) (Y := X) (Z := X) ψ e.toMonoidHom e.symm.toMonoidHom x z
42 have hid :
43 e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id (FreeGroup X) := by
44 ext w
45 simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm, MonoidHom.id_apply]
46 rw [hid, freeGroupHomFoxJacobian_id] at h
47 simpa using h.symm
49/-- The Fox Jacobian of a free-group automorphism has a right inverse, with the expected
50coefficient push-forward. -/
52 [DecidableEq X] [Fintype X]
53 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
54 (x z : X) :
55 (∑ y : X,
56 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
57 e.toMonoidHom x y *
58 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom y z) =
60 have h :=
61 freeGroupHomFoxJacobian_comp_apply (H := H)
62 (X := X) (Y := X) (Z := X) ψ e.symm.toMonoidHom e.toMonoidHom x z
63 have hid :
64 e.symm.toMonoidHom.comp e.toMonoidHom = MonoidHom.id (FreeGroup X) := by
65 ext w
66 simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom, MonoidHom.id_apply]
67 rw [hid, freeGroupHomFoxJacobian_id] at h
68 simpa using h.symm
70/-- The Jacobian matrix of a free-group automorphism has the expected left inverse. -/
72 [DecidableEq X] [Fintype X]
73 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
74 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom)
75 e.symm.toMonoidHom *
76 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
78 apply Matrix.ext
79 intro x z
80 rw [Matrix.mul_apply]
81 change
82 (∑ j : X,
83 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
84 e.symm.toMonoidHom x j *
85 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
87 rw [show
88 (∑ j : X,
89 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
90 e.symm.toMonoidHom x j *
91 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
93 freeGroupAutomorphismFoxJacobian_left_inverse_apply (H := H) ψ e x z]
94 by_cases hxz : x = z
95 · subst z
96 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
97 · simp only [ne_eq, hxz, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
99/-- The Jacobian matrix of a free-group automorphism has the expected right inverse. -/
101 [DecidableEq X] [Fintype X]
102 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
103 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.symm.toMonoidHom)
104 e.toMonoidHom *
105 freeGroupHomFoxJacobianMatrix (H := H) ψ e.symm.toMonoidHom =
107 apply Matrix.ext
108 intro x z
109 rw [Matrix.mul_apply]
110 change
111 (∑ j : X,
112 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
113 e.toMonoidHom x j *
114 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
116 rw [show
117 (∑ j : X,
118 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
119 e.toMonoidHom x j *
120 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
122 freeGroupAutomorphismFoxJacobian_right_inverse_apply (H := H) ψ e x z]
123 by_cases hxz : x = z
124 · subst z
125 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
126 · simp only [ne_eq, hxz, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
128/-- The named inverse matrix for the Fox Jacobian of a free-group automorphism.
130For `J_ψ(e)`, the inverse is the Jacobian of `e.symm` with coefficients pushed forward
131by `ψ.comp e.toMonoidHom`. -/
133 [DecidableEq X]
134 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
136 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom) e.symm.toMonoidHom
138/-- The named inverse matrix is a left inverse for the Fox Jacobian of a free-group automorphism. -/
140 [DecidableEq X] [Fintype X]
141 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
142 freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e *
143 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
145 simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] using
146 freeGroupAutomorphismFoxJacobianMatrix_left_inverse (H := H) ψ e
148/-- The named inverse matrix is a right inverse for the Fox Jacobian of a free-group automorphism. -/
150 [DecidableEq X] [Fintype X]
151 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
152 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom *
153 freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e =
155 have h :=
157 (ψ.comp e.toMonoidHom) e
158 have hcomp :
159 (ψ.comp e.toMonoidHom).comp e.symm.toMonoidHom = ψ := by
160 ext w
161 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe, Function.comp_apply,
162 MulEquiv.apply_symm_apply]
163 rw [hcomp] at h
164 simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] using h
167end FoxCalculus
169end
171end FoxDifferential