Source: ProCGroups.FoxDifferential.Discrete.FreeExpansion
1import ProCGroups.FoxDifferential.Discrete.FoxCalculus.Universal
3/-!
4# Fox differential: discrete — free expansion
6The principal declarations in this module are:
8- `freeCrossedDifferentialExpansion`
9 Prescribed values on the free generators determine the Fox-coordinate expansion.
10- `freeCrossedDifferentialExpansionHom`
11 The Fox-coordinate expansion is a crossed differential.
12- `freeCrossedDifferentialExpansion_one`
13 The Fox-coordinate expansion of the identity word is zero.
14- `freeCrossedDifferentialExpansion_of`
15 The Fox-coordinate expansion of a free generator returns its prescribed basis value.
16-/
18namespace FoxDifferential
20noncomputable section
22namespace FoxCalculus
24open scoped BigOperators
26universe u v w
28variable {H : Type v} [Group H]
29variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
30variable {X : Type u} [DecidableEq X] [Fintype X]
31variable (ψ : FreeGroup X →* H) (basisValue : X → A)
33/-- Prescribed values on the free generators determine the Fox-coordinate expansion. -/
34def freeCrossedDifferentialExpansion (w : FreeGroup X) : A :=
35 ∑ x : X,
36 relativeFreeGroupFoxDerivative (H := H) X ψ w x • basisValue x
38/-- The Fox-coordinate expansion of the identity word is zero. -/
39@[simp]
40theorem freeCrossedDifferentialExpansion_one :
41 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue 1 = 0 := by
42 simp only [freeCrossedDifferentialExpansion, relativeFreeGroupFoxDerivative_one,
43 Pi.zero_apply, zero_smul,
44 Finset.sum_const_zero]
46/-- The Fox-coordinate expansion of a free generator returns its prescribed basis value. -/
47@[simp]
48theorem freeCrossedDifferentialExpansion_of (x : X) :
49 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue (FreeGroup.of x) =
50 basisValue x := by
51 rw [freeCrossedDifferentialExpansion]
52 rw [relativeFreeGroupFoxDerivative_of]
53 rw [Finset.sum_eq_single x]
54 · simp only [Pi.single_eq_same, one_smul]
55 · intro y _ hy
56 simp only [Pi.single_eq_of_ne hy, zero_smul]
57 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, one_smul, IsEmpty.forall_iff]
59/-- The Fox-coordinate expansion is a crossed differential. -/
60def freeCrossedDifferentialExpansionHom : DifferentialHom ψ A where
61 toFun := freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue
62 map_mul' := by
63 intro u v
64 simp only [scalarCrossedAction_apply, freeCrossedDifferentialExpansion]
65 change
66 (∑ x : X,
67 relativeFreeGroupFoxDerivative (H := H) X ψ (u * v) x • basisValue x) =
68 (∑ x : X,
69 relativeFreeGroupFoxDerivative (H := H) X ψ u x • basisValue x) +
70 (MonoidAlgebra.of ℤ H (ψ u) : GroupRing H) •
71 (∑ x : X,
72 relativeFreeGroupFoxDerivative (H := H) X ψ v x • basisValue x)
73 rw [relativeFreeGroupFoxDerivative_mul]
74 simp only [MonoidAlgebra.of_apply, Pi.add_apply, Pi.smul_apply, smul_eq_mul,
75 add_smul, Finset.sum_add_distrib, Finset.smul_sum, smul_smul]
77/--
78The coefficient-generic free crossed differential over a group ring is the Fox-coordinate
79expansion of its generator values.
80-/
81theorem freeCrossedDifferentialWithCoeff_groupRingScalar_eq_expansion (w : FreeGroup X) :
82 freeCrossedDifferentialWithCoeff (A := A) (groupRingScalar ψ) basisValue w =
83 freeCrossedDifferentialExpansion (H := H) (A := A) ψ basisValue w := by
84 have h :=
85 freeCrossedHomWithCoeff_unique (A := A) (groupRingScalar ψ) basisValue
86 (freeCrossedDifferentialExpansionHom (H := H) (A := A) ψ basisValue)
87 (freeCrossedDifferentialExpansion_of (H := H) (A := A) ψ basisValue)
88 exact congrArg (fun d : DifferentialHom ψ A => d w) h.symm
90omit [Fintype X] in
91/--
92The coefficient-generic coordinate crossed differential specializes to the usual relative Fox
93derivative over a group ring.
94-/
95theorem freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
96 (w : FreeGroup X) :
97 freeCrossedDifferentialWithCoeffCoordinates
98 (X := X) (groupRingScalar ψ) w =
99 relativeFreeGroupFoxDerivative (H := H) X ψ w := by
100 exact congrArg
101 (fun d : DifferentialHom ψ (RelativeFreeFoxCoordinates (H := H) X) => d w)
102 (relativeFreeGroupFoxHom_unique (H := H) X ψ
103 (freeCrossedHomWithCoeffCoordinates (X := X) (groupRingScalar ψ))
104 (freeCrossedDifferentialWithCoeffCoordinates_of
105 (X := X) (groupRingScalar ψ)))
107variable {Y : Type w}
109/-- Abstract Fox chain rule for an arbitrary crossed differential. -/
110theorem crossedHom_comp_relativeFreeGroupFoxDerivative
111 (ψ : FreeGroup Y →* H) (φ : FreeGroup X →* FreeGroup Y)
112 (delta : DifferentialHom ψ A) (w : FreeGroup X) :
113 delta (φ w) =
114 ∑ x : X,
115 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
116 delta (φ (FreeGroup.of x)) := by
117 calc
118 delta (φ w) =
119 freeCrossedDifferentialWithCoeffExpansion
120 (X := X) (groupRingScalar (ψ.comp φ))
121 (fun x : X => delta (φ (FreeGroup.of x))) w := by
122 exact freeCrossedHomWithCoeff_comp_expansion
123 (X := X) (Y := Y) (B := A) (groupRingScalar ψ) φ delta w
124 _ =
125 ∑ x : X,
126 relativeFreeGroupFoxDerivative (H := H) X (ψ.comp φ) w x •
127 delta (φ (FreeGroup.of x)) := by
128 rw [freeCrossedDifferentialWithCoeffExpansion,
129 freeCrossedDifferentialWithCoeffExpansionLinearMap_apply,
130 freeCrossedDifferentialWithCoeffCoordinates_eq_relativeFreeGroupFoxDerivative
131 (H := H) (X := X) (ψ.comp φ) w]
133end FoxCalculus
135end
137end FoxDifferential