Source: ProCGroups.FoxDifferential.Discrete.DifferentialModule.Basic
1import ProCGroups.FoxDifferential.Common.CrossedDifferentialModule
2import Mathlib.Algebra.MonoidAlgebra.MapDomain
4/-!
5# Fox differential: discrete — differential module — basic
7The principal declarations in this module are:
9- `GroupRing`
10 The integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra.
11- `groupRingMap`
12 A group homomorphism induces the corresponding group-ring map.
13- `groupRingMap_of`
14 The induced group-ring map sends monomials to monomials.
15- `groupRingMap_single`
16 The induced group-ring map sends Finsupp.single basis terms along the group map.
17-/
19namespace FoxDifferential
21noncomputable section
23/-- The integral group ring \(\mathbb{Z}[H]\), realized as a monoid algebra. -/
24abbrev GroupRing (H : Type*) : Type _ := MonoidAlgebra ℤ H
26/-- A group homomorphism induces the corresponding group-ring map. -/
27def groupRingMap {H K : Type*} [Group H] [Group K] (φ : H →* K) :
28 GroupRing H →+* GroupRing K :=
29 MonoidAlgebra.mapDomainRingHom ℤ φ
31/-- The induced group-ring map sends monomials to monomials. -/
32@[simp]
33theorem groupRingMap_of {H K : Type*} [Group H] [Group K]
34 (φ : H →* K) (h : H) :
35 groupRingMap φ (MonoidAlgebra.of ℤ H h) =
36 MonoidAlgebra.of ℤ K (φ h) := by
37 change
38 MonoidAlgebra.mapDomain φ (MonoidAlgebra.single h 1) =
39 MonoidAlgebra.single (φ h) 1
40 exact MonoidAlgebra.mapDomain_single
42/-- The induced group-ring map sends Finsupp.single basis terms along the group map. -/
43@[simp]
44theorem groupRingMap_single {H K : Type*} [Group H] [Group K]
45 (φ : H →* K) (h : H) (z : ℤ) :
46 groupRingMap φ (MonoidAlgebra.single h z : GroupRing H) =
47 (MonoidAlgebra.single (φ h) z : GroupRing K) := by
48 change
49 MonoidAlgebra.mapDomain φ (MonoidAlgebra.single h z) =
50 MonoidAlgebra.single (φ h) z
51 exact MonoidAlgebra.mapDomain_single
53/-- The free \(\mathbb{Z}[H]\)-module on the underlying set of G. -/
54abbrev DifferentialPreModule (H : Type*) (G : Type*) : Type _ :=
55 G →₀ GroupRing H
58variable {H G : Type*} [Group H] [Group G]
60/-- The group-ring monomial attached to the group identity is the ring identity. -/
61@[simp]
62theorem groupRing_of_one : (MonoidAlgebra.of ℤ H (1 : H) : GroupRing H) = 1 := by
63 exact map_one (MonoidAlgebra.of ℤ H)
65/--
66The pre-module element imposing the Fox product relation \(d(g_1g_2)=d(g_1)+\psi(g_1)\,d(g_2)\).
67-/
68def relationElement (ψ : G →* H) (g₁ g₂ : G) : DifferentialPreModule H G :=
69 Finsupp.single (g₁ * g₂) 1 -
70 (Finsupp.single g₁ 1 + (MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)
72/-- The submodule generated by the Fox differential relations. -/
73def relationSubmodule (ψ : G →* H) : Submodule (GroupRing H) (DifferentialPreModule H G) :=
74 Submodule.span (GroupRing H) (Set.range fun p : G × G => relationElement ψ p.1 p.2)
76/-- The differential module is the universal module receiving the crossed Fox differential. -/
77abbrev DifferentialModule (ψ : G →* H) : Type _ := DifferentialPreModule H G ⧸ relationSubmodule ψ
79/-- The universal differential \(G \to A_{\psi}\). -/
80def universalDifferential (ψ : G →* H) (g : G) : DifferentialModule ψ :=
81 (relationSubmodule ψ).mkQ (Finsupp.single g 1)
83/-- Every defining Fox relation belongs to the relation submodule. -/
84theorem relationElement_mem (ψ : G →* H) (g₁ g₂ : G) :
85 relationElement ψ g₁ g₂ ∈ relationSubmodule ψ := by
86 exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩
88/-- The universal differential satisfies the Fox product rule. -/
89theorem universalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
90 universalDifferential ψ (g₁ * g₂) =
91 universalDifferential ψ g₁ +
92 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂ := by
93 have hzero : (relationSubmodule ψ).mkQ (relationElement ψ g₁ g₂) = 0 := by
94 exact
95 (Submodule.Quotient.mk_eq_zero (p := relationSubmodule ψ) (x := relationElement ψ g₁ g₂)).2
96 (relationElement_mem ψ g₁ g₂)
97 have hzero' :
98 universalDifferential ψ (g₁ * g₂) -
99 (universalDifferential ψ g₁ +
100 (relationSubmodule ψ).mkQ
101 ((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)) = 0 := by
102 simpa [universalDifferential, relationElement] using hzero
103 have hsmul :
104 (relationSubmodule ψ).mkQ ((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1) =
105 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂ := by
106 simpa [universalDifferential, Submodule.mkQ_apply] using
107 (Submodule.Quotient.mk_smul (p := relationSubmodule ψ)
108 (r := MonoidAlgebra.of ℤ H (ψ g₁)) (x := Finsupp.single g₂ 1))
109 have hzero'' :
110 universalDifferential ψ (g₁ * g₂) -
111 (universalDifferential ψ g₁ +
112 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂) = 0 := by
113 rw [hsmul] at hzero'
114 exact hzero'
115 exact sub_eq_zero.mp hzero''
117/-- The universal differential vanishes at the group identity. -/
118@[simp]
119theorem universalDifferential_one (ψ : G →* H) : universalDifferential ψ (1 : G) = 0 := by
120 have h := universalDifferential_mul ψ (1 : G) (1 : G)
121 rw [map_one, groupRing_of_one (H := H), one_smul] at h
122 have h' := congrArg (fun z : DifferentialModule ψ => z - universalDifferential ψ (1 : G)) h
123 have h'' : 0 = universalDifferential ψ (1 : G) := by
124 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
125 simpa using h''.symm
127/-- The universal differentials of \(g\) and \(g^{-1}\) add to zero with the Fox twist. -/
128theorem universalDifferential_mul_inv_right (ψ : G →* H) (g : G) :
129 universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ = 0 := by
130 have h : 0 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential
131 ψ g⁻¹ := by
132 simpa using universalDifferential_mul ψ g g⁻¹
133 simpa using h.symm
135/-- Conjugation by \(g\) acts on the differential of a kernel element by the \(\psi(g)\) scalar. -/
136theorem universalDifferential_conj_of_mem_ker (ψ : G →* H) (g n : G) (hn : ψ n = 1) :
137 universalDifferential ψ (g * n * g⁻¹) = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential
138 ψ n := by
139 calc
140 universalDifferential ψ (g * n * g⁻¹)
141 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ (n
142 * g⁻¹) := by
143 simpa [mul_assoc] using universalDifferential_mul ψ g (n * g⁻¹)
144 _ = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) •
145 (universalDifferential ψ n + (MonoidAlgebra.of ℤ H (ψ n)) • universalDifferential ψ
146 g⁻¹) := by
147 rw [universalDifferential_mul]
148 _ = universalDifferential ψ g +
149 (MonoidAlgebra.of ℤ H (ψ g)) •
150 (universalDifferential ψ n + universalDifferential ψ g⁻¹) := by
151 rw [hn, groupRing_of_one (H := H), one_smul]
152 _ = (universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹) +
153 (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
154 simp only [MonoidAlgebra.of_apply, smul_add, add_comm, add_left_comm]
155 _ = (0 : DifferentialModule ψ) + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
156 rw [universalDifferential_mul_inv_right]
157 _ = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
158 simp only [MonoidAlgebra.of_apply, zero_add]
160/-- The coefficient homomorphism \(G \to \mathbb{Z}[H]\) induced by \(\psi: G \to H\). -/
161def groupRingScalar (ψ : G →* H) : G →* GroupRing H :=
162 (MonoidAlgebra.of ℤ H).comp ψ
164/-- The group-ring scalar associated to `g` is the basis element supported at `ψ g`. -/
165@[simp]
166theorem groupRingScalar_apply (ψ : G →* H) (g : G) :
167 groupRingScalar ψ g = (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) :=
168 rfl
170/--
171The discrete Fox relation is the coefficient-ring-agnostic crossed-differential relation for the
172group-ring coefficient homomorphism.
173-/
174@[simp]
175theorem relationElement_eq_crossedDifferentialRelationElement
176 (ψ : G →* H) (g₁ g₂ : G) :
177 relationElement ψ g₁ g₂ =
178 crossedDifferentialRelationElement (groupRingScalar ψ) g₁ g₂ :=
179 rfl
181/--
182The discrete Fox relation submodule agrees with the generic crossed-differential relation
183submodule for the group-ring coefficient homomorphism.
184-/
185@[simp]
186theorem relationSubmodule_eq_crossedDifferentialRelationSubmodule (ψ : G →* H) :
187 relationSubmodule ψ =
188 crossedDifferentialRelationSubmodule (groupRingScalar ψ) :=
189 rfl
191/--
192The discrete universal differential module is linearly equivalent to the generic universal
193crossed-differential module for the group-ring coefficient homomorphism.
194-/
195def differentialModuleEquivCrossedDifferentialModule (ψ : G →* H) :
196 DifferentialModule ψ ≃ₗ[GroupRing H]
197 CrossedDifferentialModule (groupRingScalar ψ) :=
198 LinearEquiv.refl _ _
200/--
201The generic universal crossed-differential module for the group-ring scalar homomorphism
202associated to \(\psi\) is linearly equivalent to the discrete universal differential module
203\(A_{\psi}\).
204-/
205def crossedDifferentialModuleEquivDifferentialModule (ψ : G →* H) :
206 CrossedDifferentialModule (groupRingScalar ψ) ≃ₗ[GroupRing H]
207 DifferentialModule ψ :=
208 (differentialModuleEquivCrossedDifferentialModule ψ).symm
210/--
211The discrete universal differential is the generic universal crossed differential under the
212canonical linear equivalence.
213-/
214@[simp]
215theorem differentialModuleEquivCrossedDifferentialModule_d
216 (ψ : G →* H) (g : G) :
217 differentialModuleEquivCrossedDifferentialModule ψ (universalDifferential ψ g) =
218 universalCrossedDifferential (groupRingScalar ψ) g :=
219 rfl
221/--
222The generic universal crossed differential maps back to the discrete universal differential
223under the canonical linear equivalence.
224-/
225@[simp]
226theorem crossedDifferentialModuleEquivDifferentialModule_universal
227 (ψ : G →* H) (g : G) :
228 crossedDifferentialModuleEquivDifferentialModule ψ
229 (universalCrossedDifferential (groupRingScalar ψ) g) =
230 universalDifferential ψ g :=
231 rfl
234end
236end FoxDifferential