FoxDifferential/Completed/FiniteStage/RelationIdealDerivative.lean

1import FoxDifferential.Completed.FiniteStage.SourceBoundary

3/-

4PUBLIC_PAGE_SNAPSHOT

5generated_at: 2026-05-27T09:47:29+09:00

6lean_source: lean4/FoxDifferential/Completed/FiniteStage/RelationIdealDerivative.lean

7translation_root: data/translation

8purpose: identifies the local data snapshot used to build pages/

9placement: after imports, never before imports

10-/

11/-!

12# Derivatives of the finite-stage relation ideal

14This file attacks the last finite algebra layer in the completed Crowell density proof.

15The source-to-target group-algebra kernel has already been identified with the relation

16augmentation ideal generated by `q - 1`. Here we differentiate that ideal and prove that its

17finite Fox derivatives land in the relation-boundary submodule. Combining this with the

18calculation that differentiating the source boundary `Σ a_i([x_i]-1)` recovers the target

19coordinate vector closes the source-boundary relation-ideal reduction.

20-/

22namespace FoxDifferential

24noncomputable section

26open ProCGroups.InverseSystems

27open ProCGroups.ProC

29universe u

31variable {X : Type u} [DecidableEq X]

32variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)

34/-- The vector of target-valued finite Fox derivatives of a source group-algebra element. -/

35def finiteFoxStageGroupAlgebraDerivativeVector

36 (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :

37 finiteFoxStageCoordinateVector (X := X) N n :=

38 fun i => finiteFoxStageGroupAlgebraDerivative (X := X) N n i x

40@[simp]

41theorem finiteFoxStageGroupAlgebraDerivativeVector_apply

42 (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) (i : X) :

43 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x i =

44 finiteFoxStageGroupAlgebraDerivative (X := X) N n i x :=

45 rfl

47@[simp]

48theorem finiteFoxStageGroupAlgebraDerivativeVector_zero :

49 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n 0 = 0 := by

50 funext i

51 simp only [finiteFoxStageGroupAlgebraDerivativeVector_apply, map_zero, Pi.zero_apply]

53@[simp]

54theorem finiteFoxStageGroupAlgebraDerivativeVector_add

55 (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :

56 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x + y) =

57 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x +

58 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y := by

59 funext i

60 simp only [finiteFoxStageGroupAlgebraDerivativeVector, map_add, Pi.add_apply]

62@[simp]

63theorem finiteFoxStageGroupAlgebraDerivativeVector_neg

64 (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) :

65 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (-x) =

66 -finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x := by

67 funext i

68 simp only [finiteFoxStageGroupAlgebraDerivativeVector_apply, map_neg, Pi.neg_apply]

70@[simp]

71theorem finiteFoxStageGroupAlgebraDerivativeVector_sub

72 (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :

73 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x - y) =

74 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x -

75 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y := by

76 funext i

77 simp only [finiteFoxStageGroupAlgebraDerivativeVector, map_sub, Pi.sub_apply]

79/-- Product rule for the vector of target-valued derivatives. -/

80theorem finiteFoxStageGroupAlgebraDerivativeVector_mul

81 (x y : finiteFoxStageSourceGroupAlgebra (X := X) N n) :

82 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (x * y) =

83 (algebraMap (ModNCompletedCoeff n)

84 (finiteFoxStageTargetGroupAlgebra (X := X) N n)

85 (finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation

86 (F := FreeGroup X) N n y)) •

87 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x +

88 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x •

89 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n y := by

90 funext i

91 simp only [finiteFoxStageGroupAlgebraDerivativeVector, finiteFoxStageGroupAlgebraDerivative_mul,

92 Algebra.smul_def, MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,

93 Pi.add_apply, Pi.smul_apply, smul_eq_mul]

95/-- The derivative vector of a relation augmentation generator is the corresponding relation

96boundary vector. -/

97theorem finiteFoxStageGroupAlgebraDerivativeVector_relationAugmentationGenerator

98 (q : finiteFoxStageRelationGroup (X := X) N n) :

99 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n

100 (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) =

101 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) := by

102 funext i

103 rw [finiteFoxStageGroupAlgebraDerivativeVector_apply,

104 finiteFoxStageRelationBoundaryAddMonoidHom_of]

105 rw [finiteFoxStageRelationAugmentationGenerator, map_sub,

106 finiteFoxStageGroupAlgebraDerivative_of_quotient,

107 finiteFoxStageGroupAlgebraDerivative_one, sub_zero]

108 rfl

109

110omit [DecidableEq X] in

111/-- Relation augmentation generators have zero source augmentation. -/

112theorem finiteFoxStageRelationAugmentationGenerator_sourceAugmentation_eq_zero

113 (q : finiteFoxStageRelationGroup (X := X) N n) :

114 finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation

115 (F := FreeGroup X) N n

116 (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) = 0 := by

117 rw [finiteFoxStageRelationAugmentationGenerator, map_sub, map_one,

118 finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient]

119 simp only [sub_self]

120

121omit [DecidableEq X] in

122/-- Relation augmentation generators have zero target image. -/

123theorem finiteFoxStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero

124 (q : finiteFoxStageRelationGroup (X := X) N n) :

125 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

126 (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) = 0 := by

127 exact

128 (mem_finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) (N := N) (n := n)).1

129 (finiteFoxStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel

130 (X := X) N n q)

131

132/-- The derivative vector of every element of the finite relation augmentation ideal lies in the

133relation-boundary submodule. The proof keeps the two extra invariants used by the product rule:

134elements of this ideal have zero target image and zero augmentation. -/

135theorem finiteFoxGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal

136 {x : finiteFoxStageSourceGroupAlgebra (X := X) N n}

137 (hx : x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n) :

138 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n x ∈

139 finiteFoxStageRelationBoundarySubmodule (X := X) N n := by

140 let P : finiteFoxStageSourceGroupAlgebra (X := X) N n → Prop := fun z =>

141 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n z = 0 ∧

142 finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation (F := FreeGroup X) N n z = 0 ∧

143 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n z ∈

144 finiteFoxStageRelationBoundarySubmodule (X := X) N n

145 have hP : P x := by

146 change x ∈ Submodule.span (finiteFoxStageSourceGroupAlgebra (X := X) N n)

147 (Set.range (finiteFoxStageRelationAugmentationGenerator (X := X) N n)) at hx

148 refine Submodule.span_induction (p := fun z _ => P z) ?hgen ?hzero ?hadd ?hsmul hx

149 · rintro z ⟨q, rfl⟩

150 refine ⟨?_, ?_, ?_⟩

151 · exact finiteFoxStageRelationAugmentationGenerator_groupAlgebraMap_eq_zero

152 (X := X) N n q

153 · exact finiteFoxStageRelationAugmentationGenerator_sourceAugmentation_eq_zero

154 (X := X) N n q

155 · rw [finiteFoxStageGroupAlgebraDerivativeVector_relationAugmentationGenerator]

156 exact finiteFoxStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule

157 (X := X) N n (Additive.ofMul q)

158 · refine ⟨?_, ?_, ?_⟩

159 · simp only [map_zero]

160 · simp only [map_zero]

161 · simp only [finiteFoxStageGroupAlgebraDerivativeVector_zero, zero_mem]

162 · intro a b _ _ ha hb

163 rcases ha with ⟨ha_map, ha_aug, ha_der⟩

164 rcases hb with ⟨hb_map, hb_aug, hb_der⟩

165 refine ⟨?_, ?_, ?_⟩

166 · rw [map_add, ha_map, hb_map, add_zero]

167 · rw [map_add, ha_aug, hb_aug, add_zero]

168 · rw [finiteFoxStageGroupAlgebraDerivativeVector_add]

169 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).add_mem ha_der hb_der

170 · intro a z _ hz

171 rcases hz with ⟨hz_map, hz_aug, hz_der⟩

172 refine ⟨?_, ?_, ?_⟩

173 · change finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a * z) = 0

174 rw [RingHom.map_mul, hz_map, mul_zero]

175 · change finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation

176 (F := FreeGroup X) N n (a * z) = 0

177 rw [map_mul, hz_aug, mul_zero]

178 · have hderivative :

179 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (a * z) =

180 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a •

181 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n z := by

182 rw [finiteFoxStageGroupAlgebraDerivativeVector_mul]

183 rw [hz_aug]

184 simp only [MonoidAlgebra.coe_algebraMap, Algebra.algebraMap_self, RingHom.coe_id, Function.comp_apply, id_eq,

185 Finsupp.single_zero, zero_smul, zero_add]

186 change finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n (a * z) ∈

187 finiteFoxStageRelationBoundarySubmodule (X := X) N n

188 rw [hderivative]

189 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).smul_mem _ hz_der

190 exact hP.2.2

191

192/-- Differentiating the source Fox boundary recovers the coordinatewise source-to-target image. -/

193theorem finiteFoxStageGroupAlgebraDerivativeVector_sourceFoxBoundary

194 [Fintype X]

195 (a : finiteFoxStageSourceCoordinateVector (X := X) N n) :

196 finiteFoxStageGroupAlgebraDerivativeVector (X := X) N n

197 (finiteFoxStageSourceFoxBoundary (X := X) N n a) =

198 finiteFoxStageCoordinateSourceToTarget (X := X) N n a := by

199 funext j

200 rw [finiteFoxStageGroupAlgebraDerivativeVector_apply,

201 finiteFoxStageSourceFoxBoundary_apply,

202 finiteFoxStageCoordinateSourceToTarget_apply]

203 have hgen_aug (i : X) :

204 finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation

205 (F := FreeGroup X) N n

206 (MonoidAlgebra.of (ModNCompletedCoeff n)

207 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

208 (QuotientGroup.mk'

209 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

210 (FreeGroup.of i)) - 1) = 0 := by

211 rw [map_sub, map_one, finiteFoxCommutatorPowerSourceGroupAlgebraAugmentation_of_quotient]

212 simp only [sub_self]

213 have hgen_derivative (i : X) :

214 finiteFoxStageGroupAlgebraDerivative (X := X) N n j

215 (MonoidAlgebra.of (ModNCompletedCoeff n)

216 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

217 (QuotientGroup.mk'

218 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

219 (FreeGroup.of i)) - 1) =

220 (Pi.single i (1 : finiteFoxStageTargetGroupAlgebra (X := X) N n) :

221 X → finiteFoxStageTargetGroupAlgebra (X := X) N n) j := by

222 rw [map_sub, finiteFoxStageGroupAlgebraDerivative_of,

223 finiteFoxStageGroupAlgebraDerivative_one, sub_zero]

224 simp only [finiteFoxStageDerivative, finiteFoxStageDerivativeVector_of]

225 calc

226 finiteFoxStageGroupAlgebraDerivative (X := X) N n j

227 (∑ i : X,

228 a i *

229 (MonoidAlgebra.of (ModNCompletedCoeff n)

230 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

231 (QuotientGroup.mk'

232 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n)

233 (FreeGroup.of i)) - 1))

234 =

235 ∑ i : X,

236 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a i) *

237 ((Pi.single i (1 : finiteFoxStageTargetGroupAlgebra (X := X) N n) :

238 X → finiteFoxStageTargetGroupAlgebra (X := X) N n) j) := by

239 rw [map_sum]

240 apply Finset.sum_congr rfl

241 intro i hi

242 rw [finiteFoxStageGroupAlgebraDerivative_mul]

243 rw [hgen_aug i, zero_smul, zero_add, hgen_derivative i]

244 _ = finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (a j) := by

245 rw [Finset.sum_eq_single j]

246 · simp only [Pi.single_eq_same, mul_one]

247 · intro i _ hij

248 rw [Pi.single_eq_of_ne hij.symm]

249 simp only [mul_zero]

250 · simp only [Finset.mem_univ, not_true_eq_false, Pi.single_eq_same, mul_one, IsEmpty.forall_iff]

251

252/-- The source-boundary relation-ideal reduction is a theorem: if the source boundary of a lift is

253in the relation ideal, differentiating that boundary gives the desired relation-boundary vector. -/

254theorem finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives

255 [Fintype X] :

256 finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n := by

257 intro a ha

258 have hderivative :=

259 finiteFoxGADeriv_mem_relBoundarySubmodule_of_mem_relAugIdeal

260 (X := X) N n (x := finiteFoxStageSourceFoxBoundary (X := X) N n a) ha

261 rw [finiteFoxStageGroupAlgebraDerivativeVector_sourceFoxBoundary (X := X) N n a] at hderivative

262 exact hderivative

263

264/-- Finite-stage relation-boundary module exactness follows from differentiating the relation

265augmentation ideal. -/

266theorem finiteFoxStageRelationBoundaryModuleExact_of_relationIdeal_derivatives

267 [Fintype X] :

268 finiteFoxStageRelationBoundaryModuleExact (X := X) N n :=

269 finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction

270 (X := X) N n

271 (finiteFoxStageSourceBoundaryRelationIdealReduction_of_relationIdeal_derivatives

272 (X := X) N n)

273

274/-- Finite-stage coordinate coverage follows from the relation-ideal derivative calculation. -/

275theorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives

276 [Fintype X] :

277 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=

278 finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

279 (X := X) N n

280 (finiteFoxStageRelationBoundaryModuleExact_of_relationIdeal_derivatives (X := X) N n)

281

282/-- Finite-stage semidirect coverage follows from the relation-ideal derivative calculation. -/

283theorem finiteFoxStageSemiBoundaryCyclesCovered_of_relDeriv

284 [Fintype X] :

285 finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n :=

286 (finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2

287 (finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationIdeal_derivatives

288 (X := X) N n)

289

290end

291

292end FoxDifferential