Source: ProCGroups.FoxDifferential.Discrete.FoxCalculus.Semidirect
1import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic
3/-!
4# Fox differential: discrete — fox calculus — semidirect
6The principal declarations in this module are:
8- `RelativeFreeFoxCoordinates`
9 Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The
10 coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate module which
11 will identify \(A_{\psi}\) with \(\mathbb{Z}[H]^X\) for \(\psi:\mathrm{FreeGroup}(X)\to H\).
12- `RelativeFoxAction`
13 The canonical group-ring scalar action of `H` on relative Fox-coordinate vectors.
14-/
16namespace FoxDifferential
18noncomputable section
20namespace FoxCalculus
22open scoped BigOperators
24universe u v
27variable {H : Type v} [Group H]
28variable (X : Type u)
30/--
31Fox-coordinate vectors for a homomorphism from a free group to a target group \(H\). The
32coefficients are already pushed forward to \(\mathbb{Z}[H]\); this is the coordinate module
33which will identify \(A_{\psi}\) with \(\mathbb{Z}[H]^X\) for \(\psi:\mathrm{FreeGroup}(X)\to
34H\).
35-/
36abbrev RelativeFreeFoxCoordinates : Type _ := X → GroupRing H
38/-- The canonical group-ring scalar action of `H` on relative Fox-coordinate vectors. -/
39abbrev RelativeFoxAction :
40 H →* Multiplicative (AddAut (RelativeFreeFoxCoordinates (H := H) X)) :=
41 scalarCrossedAction (A := RelativeFreeFoxCoordinates (H := H) X)
42 (groupRingScalar (MonoidHom.id H))
44end FoxCalculus
46end
48end FoxDifferential