Source: ProCGroups.FoxDifferential.Discrete.GroupRing
1import ProCGroups.FoxDifferential.Discrete.DifferentialModule.Boundary
2import Mathlib.Algebra.MonoidAlgebra.Basic
3import Mathlib.RingTheory.Ideal.Maps
5/-!
6# Fox differential: discrete — group ring
8The principal declarations in this module are:
10- `augmentationAlgHom`
11 The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).
12- `augmentation`
13 The augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\).
14- `augmentation_of`
15 The augmentation map has the stated value on group-ring elements.
16- `augmentation_one`
17 The augmentation sends the group identity to \(1\).
18-/
20namespace FoxDifferential
22noncomputable section
24variable (H : Type*) [Group H]
26/-- The augmentation algebra homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). -/
27def augmentationAlgHom : GroupRing H →ₐ[ℤ] ℤ :=
28 MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)
30/-- The augmentation ring homomorphism \(\mathbb{Z}[H] \to \mathbb{Z}\). -/
31def augmentation : GroupRing H →+* ℤ :=
32 (augmentationAlgHom H).toRingHom
34/-- The augmentation ideal of the integral group ring \(\mathbb{Z}[H]\). -/
35def augmentationIdeal : Ideal (GroupRing H) :=
36 RingHom.ker (augmentation H)
38/-- The ideal generated by the standard augmentation generators \(h-1\). -/
39def augmentationGeneratorIdeal : Ideal (GroupRing H) :=
40 Ideal.span (Set.range (augmentationGenerator H))
42/-- The augmentation map has the stated value on group-ring elements. -/
43@[simp]
44theorem augmentation_of (h : H) :
45 augmentation H (MonoidAlgebra.of ℤ H h) = 1 := by
46 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply,
47 RingHom.coe_coe,
48 MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
50/-- The augmentation sends the group identity to \(1\). -/
51@[simp]
52theorem augmentation_one :
53 augmentation H (1 : GroupRing H) = 1 := by
54 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, map_one]
56variable {H} in
57/-- A group-ring element lies in the Fox augmentation ideal iff its augmentation is zero. -/
58@[simp]
59theorem mem_augmentationIdeal_iff {x : GroupRing H} :
60 x ∈ augmentationIdeal H ↔ augmentation H x = 0 := by
61 rw [augmentationIdeal, RingHom.mem_ker]
63/-- The group-ring boundary value \([\psi(g)]-1\) lies in the augmentation ideal. -/
64@[simp]
65theorem groupRingBoundary_mem_augmentationIdeal
66 {G : Type*} [Group G] (ψ : G →* H) (g : G) :
67 groupRingBoundary ψ g ∈ augmentationIdeal H := by
68 rw [mem_augmentationIdeal_iff]
69 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, groupRingBoundary,
70 MonoidAlgebra.of_apply, RingHom.coe_coe, map_sub, MonoidAlgebra.lift_single,
71 MonoidHom.one_apply, Int.zsmul_eq_mul,
72 mul_one, map_one, sub_self]
74/-- Each standard generator \(h-1\) lies in the ordinary group-ring augmentation ideal. -/
75@[simp]
76theorem augmentationGenerator_mem_augmentationIdeal (h : H) :
77 augmentationGenerator H h ∈ augmentationIdeal H := by
78 simpa [augmentationGenerator_eq_groupRingBoundary] using
79 groupRingBoundary_mem_augmentationIdeal (H := H) (G := H) (MonoidHom.id H) h
81/-- Augmentation generators lie in the augmentation-generator ideal. -/
82@[simp]
83theorem augmentationGenerator_mem_augmentationGeneratorIdeal (h : H) :
84 augmentationGenerator H h ∈ augmentationGeneratorIdeal H := by
85 exact Ideal.subset_span ⟨h, rfl⟩
87/--
88The generator-defined augmentation ideal is contained in the ordinary group-ring augmentation
89ideal.
90-/
91theorem augmentationGeneratorIdeal_le_augmentationIdeal :
92 augmentationGeneratorIdeal H ≤ augmentationIdeal H := by
93 refine Ideal.span_le.2 ?_
94 rintro _ ⟨h, rfl⟩
95 exact augmentationGenerator_mem_augmentationIdeal H h
97/--
98An augmentation-zero group-ring element can be decomposed using the standard augmentation
99generators.
100-/
101theorem exists_mem_augmentationGeneratorIdeal_add (x : GroupRing H) :
102 ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H) := by
103 refine (MonoidAlgebra.induction_on
104 (p := fun x =>
105 ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H))
106 x ?_ ?_ ?_)
107 · intro h
108 refine ⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationGeneratorIdeal H h, ?_⟩
109 simp only [MonoidAlgebra.of_apply, augmentationGenerator, augmentation, augmentationAlgHom,
110 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply,
111 Int.zsmul_eq_mul, mul_one,
112 Int.cast_one, sub_add_cancel]
113 · intro x z hx hz
114 rcases hx with ⟨y, hy, hxy⟩
115 rcases hz with ⟨w, hw, hwz⟩
116 refine ⟨y + w, (augmentationGeneratorIdeal H).add_mem hy hw, ?_⟩
117 have hy0 : augmentation H y = 0 :=
118 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
119 have hw0 : augmentation H w = 0 :=
120 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hw)
121 rw [hxy, hwz, map_add]
122 simp only [add_left_comm, add_assoc, map_add, hy0, map_intCast, Int.cast_eq, zero_add, hw0,
123 Int.cast_add]
124 · intro n x hx
125 rcases hx with ⟨y, hy, hxy⟩
126 refine ⟨n • y, zsmul_mem hy n, ?_⟩
127 have hy0 : augmentation H y = 0 :=
128 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
129 rw [hxy, smul_add]
130 simp only [zsmul_eq_mul, map_add, map_mul, map_intCast, Int.cast_eq, hy0, mul_zero,
131 zero_add, Int.cast_mul]
133/--
134The ordinary group-ring augmentation ideal is contained in the ideal generated by the elements
135\(g-1\).
136-/
137theorem augmentationIdeal_le_augmentationGeneratorIdeal :
138 augmentationIdeal H ≤ augmentationGeneratorIdeal H := by
139 intro x hx
140 rcases exists_mem_augmentationGeneratorIdeal_add H x with ⟨y, hy, hxy⟩
141 have haug : augmentation H x = 0 := (mem_augmentationIdeal_iff (H := H)).1 hx
142 rw [hxy, haug]
143 simpa using hy
145/-- The ideal generated by the standard elements \(g-1\) is the ordinary augmentation ideal. -/
146theorem augmentationGeneratorIdeal_eq_augmentationIdeal :
147 augmentationGeneratorIdeal H = augmentationIdeal H := by
148 exact le_antisymm (augmentationGeneratorIdeal_le_augmentationIdeal H)
149 (augmentationIdeal_le_augmentationGeneratorIdeal H)
151variable {H G : Type*} [Group H] [Group G]
153/-- The Crowell boundary map with codomain restricted to the augmentation ideal. -/
154def augmentationBoundary (ψ : G →* H) (g : G) : augmentationIdeal H :=
155 ⟨groupRingBoundary ψ g, groupRingBoundary_mem_augmentationIdeal (H := H) ψ g⟩
157/-- The standard generators \(h-1\) of the augmentation ideal, viewed in the ideal itself. -/
158def augmentationGeneratorSubtype (h : H) : augmentationIdeal H :=
159 ⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationIdeal H h⟩
161/-- The group-ring image of any differential-module element lies in the augmentation ideal. -/
162theorem toGroupRing_mem_augmentationIdeal (ψ : G →* H) (x : DifferentialModule ψ) :
163 toGroupRing ψ x ∈ augmentationIdeal H := by
164 refine Submodule.Quotient.induction_on (p := relationSubmodule ψ) x ?_
165 intro y
166 change liftLinear (A := GroupRing H) (groupRingBoundary ψ) y ∈ augmentationIdeal H
167 rw [liftLinear, Finsupp.linearCombination_apply]
168 exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>
169 (augmentationIdeal H).smul_mem _ (groupRingBoundary_mem_augmentationIdeal (H := H) ψ g)
171/--
172The factorization \(A_{\psi} \to I(\mathbb{Z}[H])\) of the boundary map through the augmentation
173ideal.
174-/
175def toAugmentationIdeal (ψ : G →* H) :
176 DifferentialModule ψ →ₗ[GroupRing H] augmentationIdeal H :=
177 LinearMap.codRestrict (augmentationIdeal H) (toGroupRing ψ)
178 (toGroupRing_mem_augmentationIdeal (H := H) ψ)
180/-- The universal differential maps into the ordinary group-ring augmentation ideal. -/
181@[simp]
182theorem toAugmentationIdeal_d (ψ : G →* H) (g : G) :
183 toAugmentationIdeal (H := H) ψ (universalDifferential ψ g) =
184 augmentationBoundary (H := H) ψ g := by
185 apply Subtype.ext
186 change toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g
187 exact toGroupRing_d ψ g
189/--
190Composing the boundary factorization through the augmentation ideal with the subtype map gives
191the original boundary map.
192-/
193@[simp]
194theorem subtype_comp_toAugmentationIdeal (ψ : G →* H) :
195 (augmentationIdeal H).subtype.comp (toAugmentationIdeal (H := H) ψ) =
196 toGroupRing ψ := by
197 ext x
198 rfl
200/-- The standard augmentation generators span the augmentation ideal as a module. -/
201theorem span_augmentationGeneratorSubtype_eq_top :
202 Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) = ⊤ := by
203 have hspan :
204 Submodule.span (GroupRing H)
205 (Set.range fun h => (⟨augmentationGenerator H h,
206 augmentationGenerator_mem_augmentationIdeal (H := H) h⟩ : augmentationIdeal H)) = ⊤ := by
207 rw [Submodule.span_range_subtype_eq_top_iff (p := augmentationIdeal H)
208 (s := augmentationGenerator H) (hs := augmentationGenerator_mem_augmentationIdeal (H := H))]
209 simpa [augmentationGeneratorIdeal] using
210 congrArg (fun I : Ideal (GroupRing H) => (I : Submodule (GroupRing H) (GroupRing H)))
211 (augmentationGeneratorIdeal_eq_augmentationIdeal (H := H))
212 unfold augmentationGeneratorSubtype
213 exact hspan
215/-- The boundary factorization onto the augmentation ideal is surjective in the identity case. -/
216theorem toAugmentationIdeal_surjective (ψ : G →* H) (hψ : Function.Surjective ψ) :
217 Function.Surjective (toAugmentationIdeal (H := H) ψ) := by
218 apply (LinearMap.range_eq_top).1
219 have hle :
220 Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) ≤
221 LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
222 refine Submodule.span_le.2 ?_
223 rintro _ ⟨h, rfl⟩
224 rcases hψ h with ⟨g, rfl⟩
225 refine ⟨universalDifferential ψ g, ?_⟩
226 exact toAugmentationIdeal_d (H := H) ψ g
227 have htop : ⊤ ≤ LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
228 simpa [span_augmentationGeneratorSubtype_eq_top (H := H)] using hle
229 exact eq_top_iff.mpr htop
231/-- The identity-case map from the differential module to the group ring is injective. -/
232theorem toGroupRing_id_injective :
233 Function.Injective (toGroupRing (MonoidHom.id H)) :=
234 identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)
236/--
237The inverse map from the augmentation ideal to the identity differential module, obtained by
238integrating an augmentation-zero group-ring element.
239-/
240def augmentationIdealToIdentityDifferentialModule :
241 augmentationIdeal H →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
242 toFun x :=
243 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
244 map_add' x y := by
245 change
246 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (x.1 + y.1) =
247 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1 +
248 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) y.1
249 simp only [map_add]
250 map_smul' r x := by
251 change
252 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1) =
253 r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
254 apply identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)
255 have hxaug :
256 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
257 (mem_augmentationIdeal_iff (H := H)).1 x.2
258 have hrxaug :
259 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) (r * x.1) = 0 := by
260 rw [map_mul, hxaug, mul_zero]
261 calc
262 identityCrossedDifferentialBoundary (S := ℤ) (G := H)
263 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1)) =
264 r * x.1 := by
265 exact
266 idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
267 (S := ℤ) (G := H) hrxaug
268 _ =
269 r * identityCrossedDifferentialBoundary (S := ℤ) (G := H)
270 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
271 exact congrArg (fun z => r * z)
272 (idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
273 (S := ℤ) (G := H) hxaug).symm
274 _ =
275 identityCrossedDifferentialBoundary (S := ℤ) (G := H)
276 (r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
277 exact
278 (LinearMap.map_smul
279 (identityCrossedDifferentialBoundary (S := ℤ) (G := H)) r
280 (monoidAlgebraToIdentityCrossedDifferentialModule
281 (S := ℤ) (G := H) x.1)).symm
283/--
284Composing from the augmentation ideal to the identity differential module and back gives the
285original augmentation-ideal element.
286-/
287theorem toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule
288 (x : augmentationIdeal H) :
289 toAugmentationIdeal (H := H) (MonoidHom.id H)
290 (augmentationIdealToIdentityDifferentialModule (H := H) x) = x := by
291 apply Subtype.ext
292 change
293 toGroupRing (MonoidHom.id H)
294 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) =
295 x.1
296 have hxaug :
297 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
298 (mem_augmentationIdeal_iff (H := H)).1 x.2
299 exact
300 idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
301 (S := ℤ) (G := H) hxaug
303/--
304Composing from the identity differential module to the augmentation ideal and back gives the
305original differential-module element.
306-/
307theorem augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal
308 (x : DifferentialModule (MonoidHom.id H)) :
309 augmentationIdealToIdentityDifferentialModule (H := H)
310 (toAugmentationIdeal (H := H) (MonoidHom.id H) x) = x := by
311 apply toGroupRing_id_injective (H := H)
312 change
313 toGroupRing (MonoidHom.id H)
314 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H)
315 (toGroupRing (MonoidHom.id H) x)) =
316 toGroupRing (MonoidHom.id H) x
317 have hxaug :
318 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ))
319 (toGroupRing (MonoidHom.id H) x) = 0 :=
320 (mem_augmentationIdeal_iff (H := H)).1
321 (toGroupRing_mem_augmentationIdeal (H := H) (MonoidHom.id H) x)
322 exact
323 idCrossedDiffBoundary_monoidAlgebraToModule_of_augmentation_eq_zero
324 (S := ℤ) (G := H) hxaug
326/--
327Universe-polymorphic identity case of the Crowell differential module: \(A_{\mathrm{id}}\) is
328the augmentation ideal of the integral group ring.
329-/
330def identityDifferentialModuleEquivAugmentationIdeal :
331 DifferentialModule (MonoidHom.id H) ≃ₗ[GroupRing H] augmentationIdeal H where
332 toLinearMap := toAugmentationIdeal (H := H) (MonoidHom.id H)
333 invFun := augmentationIdealToIdentityDifferentialModule (H := H)
334 left_inv := augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal (H := H)
335 right_inv := toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule (H := H)
337/--
338The linear map underlying the equivalence from the identity differential module to the
339augmentation ideal is the canonical map to that augmentation ideal.
340-/
341theorem identityDifferentialModuleEquivAugmentationIdeal_toLinearMap :
342 (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap =
343 toAugmentationIdeal (H := H) (MonoidHom.id H) :=
344 rfl
346end
348end FoxDifferential