FoxDifferential/Discrete/DifferentialModule/Basic.lean
1import FoxDifferential.Common.CrossedDifferentialModule
2import Mathlib.Algebra.MonoidAlgebra.MapDomain
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Discrete/DifferentialModule/Basic.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
13# Discrete group-ring Fox calculus
15The completed differential module is organized separately from coefficient algebras; its universal and quotient maps are used by completed crossed differentials.
16-/
17namespace FoxDifferential
19noncomputable section
21/-- The integral group ring `ℤ[H]`, realized as a monoid algebra. -/
24/-- The group-ring map induced by a group homomorphism. -/
25def groupRingMap {H K : Type*} [Group H] [Group K] (φ : H →* K) :
27 MonoidAlgebra.mapDomainRingHom ℤ φ
29/-- The induced group-ring map sends monomials to monomials. -/
30@[simp]
31theorem groupRingMap_of {H K : Type*} [Group H] [Group K]
32 (φ : H →* K) (h : H) :
33 groupRingMap φ (MonoidAlgebra.of ℤ H h) =
34 MonoidAlgebra.of ℤ K (φ h) := by
35 simp only [groupRingMap, MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk,
36 MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
38/-- The induced group-ring map sends `Finsupp.single` basis terms along the group map. -/
39@[simp]
40theorem groupRingMap_single {H K : Type*} [Group H] [Group K]
41 (φ : H →* K) (h : H) (z : ℤ) :
42 groupRingMap φ (MonoidAlgebra.single h z : GroupRing H) =
44 simp only [groupRingMap, MonoidAlgebra.mapDomainRingHom_apply, Finsupp.mapDomain_single]
46/-- The free `ℤ[H]`-module on the underlying set of `G`. -/
47abbrev DifferentialPreModule (H : Type*) (G : Type*) : Type _ :=
51variable {H G : Type*} [Group H] [Group G]
53/-- The group-ring monomial attached to the group identity is the ring identity. -/
54@[simp]
55theorem groupRing_of_one : (MonoidAlgebra.of ℤ H (1 : H) : GroupRing H) = 1 := by
56 classical
57 ext a
58 by_cases ha : a = 1
59 · subst ha
60 simp only [MonoidAlgebra.of_apply, Finsupp.single_eq_same, MonoidAlgebra.one_def]
61 · simp only [MonoidAlgebra.of_apply, ne_eq, ha, not_false_eq_true, Finsupp.single_eq_of_ne,
62 MonoidAlgebra.one_def]
64/-- The basic Fox differential relation
65`universalDifferential(g₁ g₂) =
66 universalDifferential(g₁) + ψ(g₁) • universalDifferential(g₂)`. -/
67def relationElement (ψ : G →* H) (g₁ g₂ : G) : DifferentialPreModule H G :=
68 Finsupp.single (g₁ * g₂) 1 -
69 (Finsupp.single g₁ 1 + (MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)
71/-- The submodule generated by the Fox differential relations. -/
72def relationSubmodule (ψ : G →* H) : Submodule (GroupRing H) (DifferentialPreModule H G) :=
73 Submodule.span (GroupRing H) (Set.range fun p : G × G => relationElement ψ p.1 p.2)
75/-- The `ψ`-differential module. -/
76abbrev DifferentialModule (ψ : G →* H) : Type _ := DifferentialPreModule H G ⧸ relationSubmodule ψ
78/-- The universal differential `universalDifferential : G → A_ψ`. -/
79def universalDifferential (ψ : G →* H) (g : G) : DifferentialModule ψ :=
80 (relationSubmodule ψ).mkQ (Finsupp.single g 1)
82/-- Every defining Fox relation belongs to the relation submodule. -/
83theorem relationElement_mem (ψ : G →* H) (g₁ g₂ : G) :
84 relationElement ψ g₁ g₂ ∈ relationSubmodule ψ := by
85 exact Submodule.subset_span ⟨(g₁, g₂), rfl⟩
87/-- The universal differential satisfies the Fox product rule. -/
88theorem universalDifferential_mul (ψ : G →* H) (g₁ g₂ : G) :
89 universalDifferential ψ (g₁ * g₂) =
90 universalDifferential ψ g₁ +
91 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂ := by
92 have hzero : (relationSubmodule ψ).mkQ (relationElement ψ g₁ g₂) = 0 := by
93 exact
94 (Submodule.Quotient.mk_eq_zero (p := relationSubmodule ψ) (x := relationElement ψ g₁ g₂)).2
95 (relationElement_mem ψ g₁ g₂)
96 have hzero' :
97 universalDifferential ψ (g₁ * g₂) -
98 (universalDifferential ψ g₁ +
99 (relationSubmodule ψ).mkQ
100 ((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1)) = 0 := by
101 simpa [universalDifferential, relationElement] using hzero
102 have hsmul :
103 (relationSubmodule ψ).mkQ ((MonoidAlgebra.of ℤ H (ψ g₁)) • Finsupp.single g₂ 1) =
104 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂ := by
105 simpa [universalDifferential, Submodule.mkQ_apply] using
106 (Submodule.Quotient.mk_smul (p := relationSubmodule ψ)
107 (r := MonoidAlgebra.of ℤ H (ψ g₁)) (x := Finsupp.single g₂ 1))
108 have hzero'' :
109 universalDifferential ψ (g₁ * g₂) -
110 (universalDifferential ψ g₁ +
111 (MonoidAlgebra.of ℤ H (ψ g₁)) • universalDifferential ψ g₂) = 0 := by
112 rw [hsmul] at hzero'
113 exact hzero'
114 exact sub_eq_zero.mp hzero''
116/-- The universal differential vanishes at the group identity. -/
117@[simp]
118theorem universalDifferential_one (ψ : G →* H) : universalDifferential ψ (1 : G) = 0 := by
119 have h := universalDifferential_mul ψ (1 : G) (1 : G)
120 rw [map_one, groupRing_of_one (H := H), one_smul] at h
121 have h' := congrArg (fun z : DifferentialModule ψ => z - universalDifferential ψ (1 : G)) h
122 have h'' : 0 = universalDifferential ψ (1 : G) := by
123 simpa [sub_eq_add_neg, add_assoc, add_left_comm, add_comm] using h'
124 simpa using h''.symm
126/-- The universal differential of `g` and `g⁻¹` add to zero with the Fox twist. -/
127theorem universalDifferential_mul_inv_right (ψ : G →* H) (g : G) :
128 universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ = 0 := by
129 have h : 0 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹ := by
130 simpa using universalDifferential_mul ψ g g⁻¹
131 simpa using h.symm
133/-- Conjugation by `g` acts on the differential of a kernel element by the `ψ(g)` scalar. -/
134theorem universalDifferential_conj_of_mem_ker (ψ : G →* H) (g n : G) (hn : ψ n = 1) :
135 universalDifferential ψ (g * n * g⁻¹) = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
136 calc
137 universalDifferential ψ (g * n * g⁻¹)
138 = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ (n * g⁻¹) := by
139 simpa [mul_assoc] using universalDifferential_mul ψ g (n * g⁻¹)
140 _ = universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) •
141 (universalDifferential ψ n + (MonoidAlgebra.of ℤ H (ψ n)) • universalDifferential ψ g⁻¹) := by
143 _ = universalDifferential ψ g +
144 (MonoidAlgebra.of ℤ H (ψ g)) •
145 (universalDifferential ψ n + universalDifferential ψ g⁻¹) := by
146 rw [hn, groupRing_of_one (H := H), one_smul]
147 _ = (universalDifferential ψ g + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ g⁻¹) +
148 (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
149 simp only [MonoidAlgebra.of_apply, smul_add, add_comm, add_left_comm]
150 _ = (0 : DifferentialModule ψ) + (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
152 _ = (MonoidAlgebra.of ℤ H (ψ g)) • universalDifferential ψ n := by
153 simp only [MonoidAlgebra.of_apply, zero_add]
155/-- The coefficient homomorphism `G -> ℤ[H]` induced by `ψ : G ->* H`. -/
156def groupRingScalar (ψ : G →* H) : G →* GroupRing H :=
157 (MonoidAlgebra.of ℤ H).comp ψ
159/-- The scalar coefficient homomorphism is definitionally `g ↦ [ψ g]`. -/
160@[simp]
161theorem groupRingScalar_apply (ψ : G →* H) (g : G) :
162 groupRingScalar ψ g = (MonoidAlgebra.of ℤ H (ψ g) : GroupRing H) :=
163 rfl
165/-- The discrete Fox relation is the coefficient-ring-agnostic crossed-differential relation for
166the group-ring coefficient homomorphism. -/
167@[simp]
169 (ψ : G →* H) (g₁ g₂ : G) :
170 relationElement ψ g₁ g₂ =
171 crossedDifferentialRelationElement (groupRingScalar ψ) g₁ g₂ :=
172 rfl
174/-- The discrete Fox relation submodule agrees with the generic crossed-differential relation
175submodule for the group-ring coefficient homomorphism. -/
176@[simp]
177theorem relationSubmodule_eq_crossedDifferentialRelationSubmodule (ψ : G →* H) :
178 relationSubmodule ψ =
180 rfl
182/-- The discrete universal differential module is linearly equivalent to the generic universal
183crossed-differential module for the group-ring coefficient homomorphism. -/
184def differentialModuleEquivCrossedDifferentialModule (ψ : G →* H) :
185 DifferentialModule ψ ≃ₗ[GroupRing H]
187 LinearEquiv.refl _ _
189/-- The generic universal crossed-differential module for `groupRingScalar ψ` is linearly
190equivalent to the discrete universal differential module `A_ψ`. -/
191def crossedDifferentialModuleEquivDifferentialModule (ψ : G →* H) :
192 CrossedDifferentialModule (groupRingScalar ψ) ≃ₗ[GroupRing H]
193 DifferentialModule ψ :=
196/-- The discrete universal differential is the generic universal crossed differential under the
197canonical linear equivalence. -/
198@[simp]
200 (ψ : G →* H) (g : G) :
203 rfl
205/-- The generic universal crossed differential maps back to the discrete universal differential
206under the canonical linear equivalence. -/
207@[simp]
209 (ψ : G →* H) (g : G) :
211 (universalCrossedDifferential (groupRingScalar ψ) g) =
212 universalDifferential ψ g :=
213 rfl
216end
218end FoxDifferential