FoxDifferential/Discrete/GroupRing.lean
1import FoxDifferential.Discrete.DifferentialModule.Boundary
2import Mathlib.Algebra.MonoidAlgebra.Basic
3import Mathlib.RingTheory.Ideal.Maps
5/-
6PUBLIC_PAGE_SNAPSHOT
7generated_at: 2026-05-27T09:47:29+09:00
8lean_source: lean4/FoxDifferential/Discrete/GroupRing.lean
9translation_root: data/translation
10purpose: identifies the local data snapshot used to build pages/
11placement: after imports, never before imports
12-/
13/-!
14# Group-ring augmentation for the discrete Crowell sequence
16This file contains the integral group-ring augmentation, its ideal, and the factorization of
17the universal Fox boundary through that ideal.
18-/
20namespace FoxDifferential
22noncomputable section
24variable (H : Type*) [Group H]
26/-- The augmentation algebra homomorphism `ℤ[H] → ℤ`. -/
27def augmentationAlgHom : GroupRing H →ₐ[ℤ] ℤ :=
28 MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)
30/-- The augmentation ring homomorphism `ℤ[H] → ℤ`. -/
31def augmentation : GroupRing H →+* ℤ :=
32 (augmentationAlgHom H).toRingHom
34/-- The augmentation ideal of the integral group ring `ℤ[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@[simp]
43theorem augmentation_of (h : H) :
44 augmentation H (MonoidAlgebra.of ℤ H h) = 1 := by
45 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, MonoidAlgebra.of_apply, RingHom.coe_coe,
46 MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one]
48@[simp]
49theorem augmentation_one :
50 augmentation H (1 : GroupRing H) = 1 := by
51 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, map_one]
53variable {H} in
54@[simp]
55theorem mem_augmentationIdeal_iff {x : GroupRing H} :
56 x ∈ augmentationIdeal H ↔ augmentation H x = 0 := by
57 rw [augmentationIdeal, RingHom.mem_ker]
59@[simp]
61 {G : Type*} [Group G] (ψ : G →* H) (g : G) :
62 groupRingBoundary ψ g ∈ augmentationIdeal H := by
64 simp only [augmentation, augmentationAlgHom, AlgHom.toRingHom_eq_coe, groupRingBoundary,
65 MonoidAlgebra.of_apply, RingHom.coe_coe, map_sub, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul,
68@[simp]
69theorem augmentationGenerator_mem_augmentationIdeal (h : H) :
70 augmentationGenerator H h ∈ augmentationIdeal H := by
71 simpa [augmentationGenerator_eq_groupRingBoundary] using
72 groupRingBoundary_mem_augmentationIdeal (H := H) (G := H) (MonoidHom.id H) h
74@[simp]
75theorem augmentationGenerator_mem_augmentationGeneratorIdeal (h : H) :
76 augmentationGenerator H h ∈ augmentationGeneratorIdeal H := by
77 exact Ideal.subset_span ⟨h, rfl⟩
80 augmentationGeneratorIdeal H ≤ augmentationIdeal H := by
81 refine Ideal.span_le.2 ?_
82 rintro _ ⟨h, rfl⟩
85theorem exists_mem_augmentationGeneratorIdeal_add (x : GroupRing H) :
86 ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H) := by
87 refine (MonoidAlgebra.induction_on
88 (p := fun x =>
89 ∃ y ∈ augmentationGeneratorIdeal H, x = y + (augmentation H x : GroupRing H))
90 x ?_ ?_ ?_)
91 · intro h
92 refine ⟨augmentationGenerator H h, augmentationGenerator_mem_augmentationGeneratorIdeal H h, ?_⟩
93 simp only [MonoidAlgebra.of_apply, augmentationGenerator, augmentation, augmentationAlgHom,
94 AlgHom.toRingHom_eq_coe, RingHom.coe_coe, MonoidAlgebra.lift_single, MonoidHom.one_apply, Int.zsmul_eq_mul, mul_one,
95 Int.cast_one, sub_add_cancel]
96 · intro x z hx hz
97 rcases hx with ⟨y, hy, hxy⟩
98 rcases hz with ⟨w, hw, hwz⟩
99 refine ⟨y + w, (augmentationGeneratorIdeal H).add_mem hy hw, ?_⟩
100 have hy0 : augmentation H y = 0 :=
101 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
102 have hw0 : augmentation H w = 0 :=
103 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hw)
105 simp only [add_left_comm, add_assoc, map_add, hy0, map_intCast, Int.cast_eq, zero_add, hw0, Int.cast_add]
106 · intro n x hx
107 rcases hx with ⟨y, hy, hxy⟩
108 refine ⟨n • y, zsmul_mem hy n, ?_⟩
109 have hy0 : augmentation H y = 0 :=
110 (mem_augmentationIdeal_iff (H := H)).1 (augmentationGeneratorIdeal_le_augmentationIdeal H hy)
111 rw [hxy, smul_add]
112 simp only [zsmul_eq_mul, map_add, map_mul, map_intCast, Int.cast_eq, hy0, mul_zero, zero_add, Int.cast_mul]
115 augmentationIdeal H ≤ augmentationGeneratorIdeal H := by
116 intro x hx
117 rcases exists_mem_augmentationGeneratorIdeal_add H x with ⟨y, hy, hxy⟩
118 have haug : augmentation H x = 0 := (mem_augmentationIdeal_iff (H := H)).1 hx
119 rw [hxy, haug]
120 simpa using hy
123 augmentationGeneratorIdeal H = augmentationIdeal H := by
124 exact le_antisymm (augmentationGeneratorIdeal_le_augmentationIdeal H)
127variable {H G : Type*} [Group H] [Group G]
129/-- The Crowell boundary map with codomain restricted to the augmentation ideal. -/
130def augmentationBoundary (ψ : G →* H) (g : G) : augmentationIdeal H :=
131 ⟨groupRingBoundary ψ g, groupRingBoundary_mem_augmentationIdeal (H := H) ψ g⟩
133/-- The standard generators `h - 1` of the augmentation ideal, viewed in the ideal itself. -/
134def augmentationGeneratorSubtype (h : H) : augmentationIdeal H :=
137theorem toGroupRing_mem_augmentationIdeal (ψ : G →* H) (x : DifferentialModule ψ) :
138 toGroupRing ψ x ∈ augmentationIdeal H := by
139 refine Submodule.Quotient.induction_on (p := relationSubmodule ψ) x ?_
140 intro y
141 change liftLinear (A := GroupRing H) (groupRingBoundary ψ) y ∈ augmentationIdeal H
142 rw [liftLinear, Finsupp.linearCombination_apply]
143 exact Submodule.sum_mem (augmentationIdeal H) fun g _ =>
144 (augmentationIdeal H).smul_mem _ (groupRingBoundary_mem_augmentationIdeal (H := H) ψ g)
146/-- The factorization `A_ψ → I(ℤ[H])` of the boundary map through the augmentation ideal. -/
147def toAugmentationIdeal (ψ : G →* H) :
148 DifferentialModule ψ →ₗ[GroupRing H] augmentationIdeal H :=
149 LinearMap.codRestrict (augmentationIdeal H) (toGroupRing ψ)
150 (toGroupRing_mem_augmentationIdeal (H := H) ψ)
152@[simp]
153theorem toAugmentationIdeal_d (ψ : G →* H) (g : G) :
154 toAugmentationIdeal (H := H) ψ (universalDifferential ψ g) =
155 augmentationBoundary (H := H) ψ g := by
156 apply Subtype.ext
157 change toGroupRing ψ (universalDifferential ψ g) = groupRingBoundary ψ g
158 exact toGroupRing_d ψ g
160@[simp]
161theorem subtype_comp_toAugmentationIdeal (ψ : G →* H) :
162 (augmentationIdeal H).subtype.comp (toAugmentationIdeal (H := H) ψ) =
163 toGroupRing ψ := by
164 ext x
165 rfl
168 Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) = ⊤ := by
169 have hspan :
171 (Set.range fun h => (⟨augmentationGenerator H h,
172 augmentationGenerator_mem_augmentationIdeal (H := H) h⟩ : augmentationIdeal H)) = ⊤ := by
173 rw [Submodule.span_range_subtype_eq_top_iff (p := augmentationIdeal H)
174 (s := augmentationGenerator H) (hs := augmentationGenerator_mem_augmentationIdeal (H := H))]
175 simpa [augmentationGeneratorIdeal] using
178 simpa [augmentationGeneratorSubtype] using hspan
180theorem toAugmentationIdeal_surjective (ψ : G →* H) (hψ : Function.Surjective ψ) :
181 Function.Surjective (toAugmentationIdeal (H := H) ψ) := by
182 apply (LinearMap.range_eq_top).1
183 have hle :
184 Submodule.span (GroupRing H) (Set.range (augmentationGeneratorSubtype (H := H))) ≤
185 LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
186 refine Submodule.span_le.2 ?_
187 rintro _ ⟨h, rfl⟩
188 rcases hψ h with ⟨g, rfl⟩
189 refine ⟨universalDifferential ψ g, ?_⟩
190 exact toAugmentationIdeal_d (H := H) ψ g
191 have htop : ⊤ ≤ LinearMap.range (toAugmentationIdeal (H := H) ψ) := by
192 simpa [span_augmentationGeneratorSubtype_eq_top (H := H)] using hle
193 exact eq_top_iff.mpr htop
195theorem toGroupRing_id_injective :
196 Function.Injective (toGroupRing (MonoidHom.id H)) :=
197 identityCrossedDifferentialBoundary_injective (S := ℤ) (G := H)
199/-- The inverse map from the augmentation ideal to the identity differential module, obtained by
200integrating an augmentation-zero group-ring element. -/
202 augmentationIdeal H →ₗ[GroupRing H] DifferentialModule (MonoidHom.id H) where
203 toFun x :=
204 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
205 map_add' x y := by
206 change
207 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (x.1 + y.1) =
208 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1 +
209 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) y.1
211 map_smul' r x := by
212 change
213 monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1) =
214 r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1
215 apply toGroupRing_id_injective (H := H)
216 have hxaug :
217 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
218 (mem_augmentationIdeal_iff (H := H)).1 x.2
219 have hrxaug :
220 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) (r * x.1) = 0 := by
222 calc
223 toGroupRing (MonoidHom.id H)
224 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) (r * x.1)) =
225 r * x.1 := by
226 exact
228 (S := ℤ) (G := H) hrxaug
229 _ =
230 r * toGroupRing (MonoidHom.id H)
231 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
232 exact congrArg (fun z => r * z)
234 (S := ℤ) (G := H) hxaug).symm
235 _ =
236 toGroupRing (MonoidHom.id H)
237 (r • monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) := by
239 rfl
242 (x : augmentationIdeal H) :
243 toAugmentationIdeal (H := H) (MonoidHom.id H)
244 (augmentationIdealToIdentityDifferentialModule (H := H) x) = x := by
245 apply Subtype.ext
246 change
247 toGroupRing (MonoidHom.id H)
248 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H) x.1) =
249 x.1
250 have hxaug :
251 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ)) x.1 = 0 :=
252 (mem_augmentationIdeal_iff (H := H)).1 x.2
253 exact
255 (S := ℤ) (G := H) hxaug
258 (x : DifferentialModule (MonoidHom.id H)) :
260 (toAugmentationIdeal (H := H) (MonoidHom.id H) x) = x := by
261 apply toGroupRing_id_injective (H := H)
262 change
263 toGroupRing (MonoidHom.id H)
264 (monoidAlgebraToIdentityCrossedDifferentialModule (S := ℤ) (G := H)
265 (toGroupRing (MonoidHom.id H) x)) =
266 toGroupRing (MonoidHom.id H) x
267 have hxaug :
268 (MonoidAlgebra.lift ℤ ℤ H (1 : H →* ℤ))
269 (toGroupRing (MonoidHom.id H) x) = 0 :=
270 (mem_augmentationIdeal_iff (H := H)).1
271 (toGroupRing_mem_augmentationIdeal (H := H) (MonoidHom.id H) x)
272 exact
274 (S := ℤ) (G := H) hxaug
276/-- Universe-polymorphic identity case of the Crowell differential module:
277`A_id` is the augmentation ideal of the integral group ring. -/
279 DifferentialModule (MonoidHom.id H) ≃ₗ[GroupRing H] augmentationIdeal H where
280 toLinearMap := toAugmentationIdeal (H := H) (MonoidHom.id H)
281 invFun := augmentationIdealToIdentityDifferentialModule (H := H)
282 left_inv := augmentationIdealToIdentityDifferentialModule_toAugmentationIdeal (H := H)
283 right_inv := toAugmentationIdeal_augmentationIdealToIdentityDifferentialModule (H := H)
286 (identityDifferentialModuleEquivAugmentationIdeal (H := H)).toLinearMap =
287 toAugmentationIdeal (H := H) (MonoidHom.id H) :=
288 rfl
290end
292end FoxDifferential