Source: ProCGroups.FoxDifferential.Discrete.DifferentialModule.Universal
1import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic
3/-!
4# Fox differential: discrete — differential module — universal
6The principal declarations in this module are:
8- `DifferentialHom`
9 A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule.
10- `liftLinear`
11 The linear map out of the free pre-module determined by \(\delta\).
12- `liftLinear_single`
13 The linear extension of a map evaluates on a single basis vector by scalar multiplication.
14- `differentialHomLiftLinear_relationElement`
15 A crossed differential kills each defining relation of the universal differential module.
16-/
18namespace FoxDifferential
20noncomputable section
22variable {H G : Type*} [Group H] [Group G]
24section UniversalProperty
26variable {A : Type*} [AddCommGroup A] [Module (GroupRing H) A]
28/-- A \(\psi\)-differential map is a map satisfying the Fox Leibniz rule. -/
29abbrev DifferentialHom (ψ : G →* H) (A : Type*) [AddCommGroup A] [Module (GroupRing H) A] :=
30 ScalarCrossedHom (groupRingScalar ψ) A
32/-- The linear map out of the free pre-module determined by \(\delta\). -/
33def liftLinear (δ : G → A) : DifferentialPreModule H G →ₗ[GroupRing H] A :=
34 Finsupp.linearCombination (GroupRing H) δ
36omit [Group G] in
37/-- The linear extension of a map evaluates on a single basis vector by scalar multiplication. -/
38@[simp]
39theorem liftLinear_single (δ : G → A) (g : G) (r : GroupRing H) :
40 liftLinear δ (Finsupp.single g r) = r • δ g := by
41 simp only [liftLinear, Finsupp.linearCombination_single]
43/-- A crossed differential kills each defining relation of the universal differential module. -/
44theorem differentialHomLiftLinear_relationElement
45 (ψ : G →* H) (δ : DifferentialHom ψ A) (g₁ g₂ : G) :
46 liftLinear δ (relationElement ψ g₁ g₂) = 0 := by
47 simp only [liftLinear, relationElement, MonoidAlgebra.of_apply, Finsupp.smul_single,
48 smul_eq_mul, mul_one, map_sub, Finsupp.linearCombination_single,
49 ScalarCrossedHom.map_mul, groupRingScalar_apply, smul_add, one_smul, map_add,
50 sub_self]
52/--
53The relation submodule is contained in the kernel of the linear extension of a crossed
54differential.
55-/
56theorem differentialHomRelationSubmodule_le_ker
57 (ψ : G →* H) (δ : DifferentialHom ψ A) :
58 relationSubmodule ψ ≤ LinearMap.ker (liftLinear δ) := by
59 refine Submodule.span_le.2 ?_
60 rintro _ ⟨⟨g₁, g₂⟩, rfl⟩
61 simpa [LinearMap.mem_ker] using
62 differentialHomLiftLinear_relationElement (A := A) ψ δ g₁ g₂
64/--
65A crossed differential factors uniquely through the universal differential module as a linear
66map.
67-/
68def differentialModuleLift (ψ : G →* H) (δ : DifferentialHom ψ A) :
69 DifferentialModule ψ →ₗ[GroupRing H] A :=
70 (relationSubmodule ψ).liftQ (liftLinear δ)
71 (differentialHomRelationSubmodule_le_ker (A := A) ψ δ)
73/-- The universal lift evaluates on universalDifferential g as the original crossed differential. -/
74@[simp]
75theorem differentialModuleLift_d (ψ : G →* H) (δ : DifferentialHom ψ A) (g : G) :
76 differentialModuleLift ψ δ (universalDifferential ψ g) = δ g := by
77 change
78 (relationSubmodule ψ).liftQ (liftLinear δ)
79 (differentialHomRelationSubmodule_le_ker (A := A) ψ δ)
80 ((relationSubmodule ψ).mkQ (Finsupp.single g 1)) = δ g
81 rw [Submodule.mkQ_apply, Submodule.liftQ_apply]
82 simp only [liftLinear_single, one_smul]
84/--
85Linear maps out of the universal differential module are equal when they agree on all universal
86differentials.
87-/
88@[ext]
89theorem hom_ext (ψ : G →* H) {f g : DifferentialModule ψ →ₗ[GroupRing H] A}
90 (hfg : ∀ g', f (universalDifferential ψ g') = g (universalDifferential ψ g')) : f = g := by
91 apply Submodule.linearMap_qext _
92 apply Finsupp.lhom_ext
93 intro g' r
94 have hsingle : ((relationSubmodule ψ).mkQ (Finsupp.single g' r) : DifferentialModule ψ) =
95 r • universalDifferential ψ g' := by
96 rw [← Finsupp.smul_single_one]
97 rfl
98 change f ((relationSubmodule ψ).mkQ (Finsupp.single g' r)) =
99 g ((relationSubmodule ψ).mkQ (Finsupp.single g' r))
100 rw [hsingle]
101 simpa [map_smul] using congrArg (fun z => r • z) (hfg g')
103/--
104The universal lift is the unique linear map with prescribed values on universal differentials.
105-/
106theorem differentialModuleLift_unique
107 (ψ : G →* H) (δ : DifferentialHom ψ A)
108 (f : DifferentialModule ψ →ₗ[GroupRing H] A)
109 (hf : ∀ g, f (universalDifferential ψ g) = δ g) :
110 f = differentialModuleLift (A := A) ψ δ := by
111 apply hom_ext ψ
112 intro g
113 rw [hf g, differentialModuleLift_d]
115/-- Existence and uniqueness of the linear map representing a discrete Fox crossed differential. -/
116theorem existsUnique_differentialModuleLift
117 (ψ : G →* H) (δ : DifferentialHom ψ A) :
118 ∃! f : DifferentialModule ψ →ₗ[GroupRing H] A,
119 ∀ g, f (universalDifferential ψ g) = δ g := by
120 refine ⟨differentialModuleLift (A := A) ψ δ, ?_, ?_⟩
121 · intro g
122 exact differentialModuleLift_d (A := A) ψ δ g
123 · intro f hf
124 exact differentialModuleLift_unique (A := A) ψ δ f hf
126/-- The crossed differential induced by a linear map out of the universal differential module. -/
127def differentialHomOfLinearMap
128 (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) : DifferentialHom ψ A where
129 toFun g := f (universalDifferential ψ g)
130 map_mul' := by
131 intro g₁ g₂
132 change f (universalDifferential ψ (g₁ * g₂)) =
133 f (universalDifferential ψ g₁) +
134 (MonoidAlgebra.of ℤ H (ψ g₁) : GroupRing H) •
135 f (universalDifferential ψ g₂)
136 rw [universalDifferential_mul, map_add, map_smul]
138/-- The differential induced by a linear map evaluates that map on the universal
139differential. -/
140@[simp]
141theorem differentialHomOfLinearMap_apply
142 (ψ : G →* H) (f : DifferentialModule ψ →ₗ[GroupRing H] A) (g : G) :
143 differentialHomOfLinearMap (A := A) ψ f g = f (universalDifferential ψ g) :=
144 rfl
146/--
147Discrete Fox crossed differentials \(G \to A\) with respect to \(\psi: G \to H\) are represented
148by \(\mathbb{Z}[H]\)-linear maps out of the universal differential module \(A_{\psi}\).
149-/
150def differentialHomEquivLinearMap (ψ : G →* H) :
151 DifferentialHom ψ A ≃ (DifferentialModule ψ →ₗ[GroupRing H] A) where
152 toFun δ := differentialModuleLift (A := A) ψ δ
153 invFun f := differentialHomOfLinearMap (A := A) ψ f
154 left_inv δ := by
155 apply CrossedHom.ext
156 intro g
157 exact differentialModuleLift_d (A := A) ψ δ g
158 right_inv f := by
159 apply hom_ext ψ
160 intro g
161 exact differentialModuleLift_d (A := A) ψ
162 (differentialHomOfLinearMap (A := A) ψ f) g
164/--
165The compatibility between the discrete representation theorem and the generic
166crossed-differential-module representation theorem.
167-/
168theorem differentialHomEquivLinearMap_eq_generic
169 (ψ : G →* H) (δ : DifferentialHom ψ A) :
170 differentialHomEquivLinearMap (A := A) ψ δ =
171 (crossedHomModuleEquivLinearMap
172 (A := A) (groupRingScalar ψ) δ).comp
173 (differentialModuleEquivCrossedDifferentialModule ψ).toLinearMap := by
174 apply hom_ext ψ
175 intro g
176 change
177 differentialModuleLift (A := A) ψ δ (universalDifferential ψ g) =
178 crossedHomModuleLift (A := A) (groupRingScalar ψ) δ
179 (universalCrossedDifferential (groupRingScalar ψ) g)
180 rw [differentialModuleLift_d, crossedHomModuleLift_universal]
182end UniversalProperty
184end
186end FoxDifferential