Source: ProCGroups.FoxDifferential.Discrete.Jacobian.Automorphism
1import ProCGroups.FoxDifferential.Discrete.Jacobian.ChainRule
3/-!
4# Fox differential: discrete — jacobian — automorphism
6The principal declarations in this module are:
8- `freeGroupAutomorphismFoxJacobianMatrixInverse`
9 The named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J_{\psi}(e)\),
10 the inverse is the Jacobian of the inverse automorphism \(e^{-1}\), with coefficients pushed
11 forward by the composite of \(\psi\) and the monoid homomorphism underlying \(e\).
12- `freeGroupAutomorphismFoxJacobian_left_inverse_apply`
13 The Fox Jacobian of a free-group automorphism, multiplied on the left by the Jacobian of its
14 inverse, has Kronecker-delta entries.
15- `freeGroupAutomorphismFoxJacobian_right_inverse_apply`
16 The Fox Jacobian of a free-group automorphism, multiplied on the right by the Jacobian of its
17 inverse, has Kronecker-delta entries.
18- `freeGroupAutomorphismFoxJacobianMatrix_left_inverse`
19 The Jacobian matrix of a free-group automorphism has the expected left inverse.
20-/
22namespace FoxDifferential
24noncomputable section
26namespace FoxCalculus
28open scoped BigOperators
30universe u v w z t
32variable {H : Type w} [Group H]
33variable {X : Type u} {Y : Type v}
34/--
35The Fox Jacobian of a free-group automorphism, multiplied on the left by the Jacobian of its
36inverse, has Kronecker-delta entries.
37-/
38theorem freeGroupAutomorphismFoxJacobian_left_inverse_apply
39 [DecidableEq X] [Fintype X]
40 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
41 (x z : X) :
42 (∑ y : X,
43 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
44 e.symm.toMonoidHom x y *
45 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom y z) =
46 (Pi.single x (1 : GroupRing H) : X → GroupRing H) z := by
47 have h :=
48 freeGroupHomFoxJacobian_comp_apply (H := H)
49 (X := X) (Y := X) (Z := X) ψ e.toMonoidHom e.symm.toMonoidHom x z
50 have hid :
51 e.toMonoidHom.comp e.symm.toMonoidHom = MonoidHom.id (FreeGroup X) := by
52 ext w
53 simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_comp_coe_monoidHom_symm,
54 MonoidHom.id_apply]
55 rw [hid, freeGroupHomFoxJacobian_id] at h
56 simpa using h.symm
58/--
59The Fox Jacobian of a free-group automorphism, multiplied on the right by the Jacobian of its
60inverse, has Kronecker-delta entries.
61-/
62theorem freeGroupAutomorphismFoxJacobian_right_inverse_apply
63 [DecidableEq X] [Fintype X]
64 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X)
65 (x z : X) :
66 (∑ y : X,
67 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
68 e.toMonoidHom x y *
69 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom y z) =
70 (Pi.single x (1 : GroupRing H) : X → GroupRing H) z := by
71 have h :=
72 freeGroupHomFoxJacobian_comp_apply (H := H)
73 (X := X) (Y := X) (Z := X) ψ e.symm.toMonoidHom e.toMonoidHom x z
74 have hid :
75 e.symm.toMonoidHom.comp e.toMonoidHom = MonoidHom.id (FreeGroup X) := by
76 ext w
77 simp only [MulEquiv.toMonoidHom_eq_coe, MulEquiv.coe_monoidHom_symm_comp_coe_monoidHom,
78 MonoidHom.id_apply]
79 rw [hid, freeGroupHomFoxJacobian_id] at h
80 simpa using h.symm
82/-- The Jacobian matrix of a free-group automorphism has the expected left inverse. -/
83theorem freeGroupAutomorphismFoxJacobianMatrix_left_inverse
84 [DecidableEq X] [Fintype X]
85 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
86 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom)
87 e.symm.toMonoidHom *
88 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
89 (1 : Matrix X X (GroupRing H)) := by
90 apply Matrix.ext
91 intro x z
92 rw [Matrix.mul_apply]
93 change
94 (∑ j : X,
95 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
96 e.symm.toMonoidHom x j *
97 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
98 (1 : Matrix X X (GroupRing H)) x z
99 rw [show
100 (∑ j : X,
101 freeGroupHomFoxJacobian (H := H) (ψ.comp e.toMonoidHom)
102 e.symm.toMonoidHom x j *
103 freeGroupHomFoxJacobian (H := H) ψ e.toMonoidHom j z) =
104 (Pi.single x (1 : GroupRing H) : X → GroupRing H) z from
105 freeGroupAutomorphismFoxJacobian_left_inverse_apply (H := H) ψ e x z]
106 by_cases hxz : x = z
107 · subst z
108 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
109 · simp only [ne_eq, hxz, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
111/-- The Jacobian matrix of a free-group automorphism has the expected right inverse. -/
112theorem freeGroupAutomorphismFoxJacobianMatrix_right_inverse
113 [DecidableEq X] [Fintype X]
114 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
115 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.symm.toMonoidHom)
116 e.toMonoidHom *
117 freeGroupHomFoxJacobianMatrix (H := H) ψ e.symm.toMonoidHom =
118 (1 : Matrix X X (GroupRing H)) := by
119 apply Matrix.ext
120 intro x z
121 rw [Matrix.mul_apply]
122 change
123 (∑ j : X,
124 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
125 e.toMonoidHom x j *
126 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
127 (1 : Matrix X X (GroupRing H)) x z
128 rw [show
129 (∑ j : X,
130 freeGroupHomFoxJacobian (H := H) (ψ.comp e.symm.toMonoidHom)
131 e.toMonoidHom x j *
132 freeGroupHomFoxJacobian (H := H) ψ e.symm.toMonoidHom j z) =
133 (Pi.single x (1 : GroupRing H) : X → GroupRing H) z from
134 freeGroupAutomorphismFoxJacobian_right_inverse_apply (H := H) ψ e x z]
135 by_cases hxz : x = z
136 · subst z
137 simp only [Pi.single_eq_same, Matrix.one_apply_eq]
138 · simp only [ne_eq, hxz, not_false_eq_true, Pi.single_eq_of_ne', Matrix.one_apply_ne]
140/--
141The named inverse matrix for the Fox Jacobian of a free-group automorphism. For \(J_{\psi}(e)\),
142the inverse is the Jacobian of the inverse automorphism \(e^{-1}\), with coefficients pushed
143forward by the composite of \(\psi\) and the monoid homomorphism underlying \(e\).
144-/
145def freeGroupAutomorphismFoxJacobianMatrixInverse
146 [DecidableEq X]
147 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
148 Matrix X X (GroupRing H) :=
149 freeGroupHomFoxJacobianMatrix (H := H) (ψ.comp e.toMonoidHom) e.symm.toMonoidHom
151/-- The named inverse matrix is a left inverse for the Fox Jacobian of a free-group automorphism. -/
152theorem freeGroupAutomorphismFoxJacobianMatrixInverse_mul
153 [DecidableEq X] [Fintype X]
154 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
155 freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e *
156 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom =
157 (1 : Matrix X X (GroupRing H)) := by
158 simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] using
159 freeGroupAutomorphismFoxJacobianMatrix_left_inverse (H := H) ψ e
161/--
162The named inverse matrix is a right inverse for the Fox Jacobian of a free-group automorphism.
163-/
164theorem freeGroupAutomorphismFoxJacobianMatrix_mul_inverse
165 [DecidableEq X] [Fintype X]
166 (ψ : FreeGroup X →* H) (e : FreeGroup X ≃* FreeGroup X) :
167 freeGroupHomFoxJacobianMatrix (H := H) ψ e.toMonoidHom *
168 freeGroupAutomorphismFoxJacobianMatrixInverse (H := H) ψ e =
169 (1 : Matrix X X (GroupRing H)) := by
170 have h :=
171 freeGroupAutomorphismFoxJacobianMatrix_right_inverse (H := H)
172 (ψ.comp e.toMonoidHom) e
173 have hcomp :
174 (ψ.comp e.toMonoidHom).comp e.symm.toMonoidHom = ψ := by
175 ext w
176 simp only [MulEquiv.toMonoidHom_eq_coe, MonoidHom.coe_comp, MonoidHom.coe_coe,
177 Function.comp_apply,
178 MulEquiv.apply_symm_apply]
179 rw [hcomp] at h
180 simpa [freeGroupAutomorphismFoxJacobianMatrixInverse] using h
183end FoxCalculus
185end
187end FoxDifferential