Source: ProCGroups.FoxDifferential.Discrete.Naturality
1import ProCGroups.FoxDifferential.Discrete.FreeExpansion
3/-!
4# Fox differential: discrete — naturality
6The principal declarations in this module are:
8- `relativeFreeFoxCoordinatesMap`
9 A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward.
10- `relativeFreeFoxCoordinatesMap_apply`
11 Pushing a relative Fox-coordinate vector along `φ` applies `groupRingMap φ` to the selected
12 coordinate.
13- `relativeFreeGroupFoxDerivative_mapDomain`
14 Relative Fox derivatives are natural under coefficient push-forward.
15- `relativeFreeGroupFoxDerivative_mapDomain_apply`
16 Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.
17-/
19namespace FoxDifferential
21noncomputable section
23namespace FoxCalculus
25universe u v w
27variable {H : Type v} {K : Type w} [Group H] [Group K]
28variable {X : Type u} [DecidableEq X]
29variable (ψ : FreeGroup X →* H) (φ : H →* K)
31/-- A homomorphism of coefficient groups pushes a relative Fox-coordinate vector forward. -/
32def relativeFreeFoxCoordinatesMap :
33 RelativeFreeFoxCoordinates (H := H) X → RelativeFreeFoxCoordinates (H := K) X :=
34 fun a x => groupRingMap φ (a x)
36omit [DecidableEq X] in
37/--
38Pushing a relative Fox-coordinate vector along `φ` applies `groupRingMap φ` to the selected
39coordinate.
40-/
41@[simp]
42theorem relativeFreeFoxCoordinatesMap_apply
43 (a : RelativeFreeFoxCoordinates (H := H) X) (x : X) :
44 relativeFreeFoxCoordinatesMap (X := X) φ a x = groupRingMap φ (a x) :=
45 rfl
47/-- Relative Fox derivatives are natural under coefficient push-forward. -/
48theorem relativeFreeGroupFoxDerivative_mapDomain (w : FreeGroup X) :
49 relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w =
50 relativeFreeFoxCoordinatesMap (X := X) φ
51 (relativeFreeGroupFoxDerivative (H := H) X ψ w) := by
52 let delta : DifferentialHom (φ.comp ψ) (RelativeFreeFoxCoordinates (H := K) X) :=
53 { toFun := fun w => relativeFreeFoxCoordinatesMap (X := X) φ
54 (relativeFreeGroupFoxDerivative (H := H) X ψ w)
55 map_mul' := by
56 intro u v
57 funext x
58 simp only [scalarCrossedAction_apply, relativeFreeGroupFoxDerivative_mul,
59 MonoidAlgebra.of_apply, Pi.add_apply,
60 Pi.smul_apply, smul_eq_mul, map_add, map_mul, groupRingMap_single,
61 groupRingScalar, MonoidHom.coe_comp, Function.comp_apply,
62 relativeFreeFoxCoordinatesMap] }
63 have hbasis :
64 ∀ x : X, delta (FreeGroup.of x) = Pi.single x (1 : GroupRing K) := by
65 intro x
66 change
67 relativeFreeFoxCoordinatesMap (X := X) φ
68 (relativeFreeGroupFoxDerivative (H := H) X ψ (FreeGroup.of x)) =
69 Pi.single x (1 : GroupRing K)
70 funext y
71 by_cases hxy : x = y
72 · subst y
73 simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of,
74 Pi.single_eq_same, map_one]
75 · have hyx : y ≠ x := Ne.symm hxy
76 simp only [relativeFreeFoxCoordinatesMap_apply, relativeFreeGroupFoxDerivative_of,
77 Pi.single_eq_of_ne hyx, map_zero]
78 exact (congrFun
79 (congrArg CrossedHom.toFun
80 (relativeFreeGroupFoxHom_unique (H := K) X (φ.comp ψ) delta hbasis)) w).symm
82/--
83Component form of coefficient-push-forward naturality for relative free-group Fox derivatives.
84-/
85theorem relativeFreeGroupFoxDerivative_mapDomain_apply (w : FreeGroup X) (x : X) :
86 relativeFreeGroupFoxDerivative (H := K) X (φ.comp ψ) w x =
87 groupRingMap φ (relativeFreeGroupFoxDerivative (H := H) X ψ w x) := by
88 have h := congrFun
89 (relativeFreeGroupFoxDerivative_mapDomain (H := H) (K := K) ψ φ w) x
90 simpa [relativeFreeFoxCoordinatesMap] using h
92end FoxCalculus
94end
96end FoxDifferential