Source: ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Universal
1import ProCGroups.FoxDifferential.Completed.Residue.FreeGroup.Basic
3/-!
4# Fox differential: completed — residue — free group — universal
6The principal declarations in this module are:
8- `residueFreeCrossedHomEquivLinearMap`
9 Residue crossed homomorphisms on a free group are represented by the universal residue module.
10- `residueFreeGroupFoxDerivativeVectorLinearMap`
11 The linear map from the residue universal module representing the residue derivative vector.
12- `residueFreeGroupFoxDerivativeVectorLinearMap_universal`
13 The representing linear map evaluates on the universal differential as the residue derivative
14 vector.
15- `existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap`
16 Existence and uniqueness of the linear map representing the residue derivative vector.
17-/
19namespace FoxDifferential
21noncomputable section
23open scoped BigOperators
25universe u v
28variable {X : Type u} {H : Type v} [Group H] [DecidableEq X]
30/--
31Residue crossed homomorphisms on a free group are represented by the universal residue module.
32-/
33def residueFreeCrossedHomEquivLinearMap
34 (n : ℕ) (ψ : FreeGroup X →* H) :
35 ScalarCrossedHom (residueGroupRingScalar n ψ) (ResidueFreeFoxCoordinates n H X) ≃
36 (ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
37 ResidueFreeFoxCoordinates n H X) :=
38 residueCrossedHomEquivLinearMap
39 (A := ResidueFreeFoxCoordinates n H X) n ψ
41/-- The linear map from the residue universal module representing the residue derivative vector. -/
42def residueFreeGroupFoxDerivativeVectorLinearMap
43 (n : ℕ) (ψ : FreeGroup X →* H) :
44 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
45 ResidueFreeFoxCoordinates n H X :=
46 residueDifferentialModuleLift
47 (A := ResidueFreeFoxCoordinates n H X) n ψ
48 (residueFreeGroupFoxDerivativeVector n ψ)
50/--
51The representing linear map evaluates on the universal differential as the residue derivative
52vector.
53-/
54@[simp]
55theorem residueFreeGroupFoxDerivativeVectorLinearMap_universal
56 (n : ℕ) (ψ : FreeGroup X →* H) (w : FreeGroup X) :
57 residueFreeGroupFoxDerivativeVectorLinearMap n ψ
58 (residueUniversalDifferential n ψ w) =
59 residueFreeGroupFoxDerivativeVector n ψ w := by
60 exact residueDifferentialModuleLift_universal
61 (A := ResidueFreeFoxCoordinates n H X) n ψ
62 (residueFreeGroupFoxDerivativeVector n ψ) w
64/-- Existence and uniqueness of the linear map representing the residue derivative vector. -/
65theorem existsUnique_residueFreeGroupFoxDerivativeVectorLinearMap
66 (n : ℕ) (ψ : FreeGroup X →* H) :
67 ∃! f :
68 ResidueDifferentialModule n ψ →ₗ[ResidueGroupRing n H]
69 ResidueFreeFoxCoordinates n H X,
70 ∀ w : FreeGroup X,
71 f (residueUniversalDifferential n ψ w) =
72 residueFreeGroupFoxDerivativeVector n ψ w := by
73 exact existsUnique_residueDifferentialModuleLift
74 (A := ResidueFreeFoxCoordinates n H X) n ψ
75 (residueFreeGroupFoxDerivativeVector n ψ)
77end
79end FoxDifferential