Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic
1import ProCGroups.FoxDifferential.Common.FreeCrossedDifferential
2import ProCGroups.FoxDifferential.Completed.Residue.Core
4/-!
5# Fox differential: completed — residue — free group — basic
7The principal declarations in this module are:
9- `ResidueFreeFoxCoordinates`
10 Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\).
11- `residueFreeGroupFoxDerivativeVector`
12 Residue free-group Fox derivative vector, with coefficients pushed forward along
13 \(\psi:\mathrm{FreeGroup}(X)\to H\).
14- `residueFreeGroupFoxDerivativeVector_of`
15 The residue free-group derivative vector sends a free generator to the corresponding coordinate
16 basis vector.
17- `residueFreeGroupFoxDerivativeVector_unique`
18 Uniqueness of the residue free-group derivative vector among crossed differentials with standard
19 coordinate values on free generators.
20-/
22namespace FoxDifferential
24noncomputable section
26open scoped BigOperators
28universe u v
31variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
33/-- Residue Fox-coordinate vectors with coefficients in \((\mathbb{Z}/n\mathbb{Z})[H]\). -/
34abbrev ResidueFreeFoxCoordinates (n : ℕ) (H : Type v) (X : Type u) : Type (max u v) :=
35 X → ResidueGroupRing n H
37/--
38Residue free-group Fox derivative vector, with coefficients pushed forward along
39\(\psi:\mathrm{FreeGroup}(X)\to H\).
40-/
41def residueFreeGroupFoxDerivativeVector (n : ℕ) (ψ : FreeGroup X →* H)
42 : ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueFreeFoxCoordinates n H X) :=
43 freeCrossedHomWithCoeff
44 (A := ResidueFreeFoxCoordinates n H X)
45 (residueGroupRingScalar n ψ)
46 (fun x => Pi.single x (1 : ResidueGroupRing n H))
48/-- A coordinate of the residue free-group Fox derivative. -/
49def residueFreeGroupFoxDerivative (n : ℕ) (ψ : FreeGroup X →* H) (i : X) :
50 ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueGroupRing n H) :=
51 (residueFreeGroupFoxDerivativeVector n ψ).mapLinear
52 { toFun := fun v => v i
53 map_add' := by intro v w; rfl
54 map_smul' := by intro r v; rfl }
56/--
57The residue free-group derivative vector sends a free generator to the corresponding coordinate
58basis vector.
59-/
60@[simp]
61theorem residueFreeGroupFoxDerivativeVector_of (n : ℕ) (ψ : FreeGroup X →* H) (x : X) :
62 residueFreeGroupFoxDerivativeVector n ψ (FreeGroup.of x) =
63 Pi.single x (1 : ResidueGroupRing n H) := by
64 exact freeCrossedHomWithCoeff_of
65 (A := ResidueFreeFoxCoordinates n H X) (residueGroupRingScalar n ψ)
66 (fun y => Pi.single y (1 : ResidueGroupRing n H)) x
68/--
69Uniqueness of the residue free-group derivative vector among crossed differentials with standard
70coordinate values on free generators.
71-/
72theorem residueFreeGroupFoxDerivativeVector_unique
73 (n : ℕ) (ψ : FreeGroup X →* H)
74 (delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
75 (ResidueFreeFoxCoordinates n H X))
76 (hbasis :
77 ∀ x : X, delta (FreeGroup.of x) =
78 Pi.single x (1 : ResidueGroupRing n H)) :
79 delta = residueFreeGroupFoxDerivativeVector n ψ := by
80 exact freeCrossedHomWithCoeff_unique
81 (A := ResidueFreeFoxCoordinates n H X)
82 (residueGroupRingScalar n ψ)
83 (fun x => Pi.single x (1 : ResidueGroupRing n H)) delta hbasis
85/-- Existence and uniqueness theorem for the residue free-group derivative vector. -/
86theorem existsUnique_residueFreeGroupFoxDerivativeVector
87 (n : ℕ) (ψ : FreeGroup X →* H) :
88 ∃! delta : ScalarCrossedHom (residueGroupRingScalar n ψ)
89 (ResidueFreeFoxCoordinates n H X),
90 ∀ x : X, delta (FreeGroup.of x) =
91 Pi.single x (1 : ResidueGroupRing n H) := by
92 exact existsUnique_freeCrossedHomWithCoeff
93 (A := ResidueFreeFoxCoordinates n H X)
94 (residueGroupRingScalar n ψ)
95 (fun x => Pi.single x (1 : ResidueGroupRing n H))
98end
100end FoxDifferential