FoxDifferential/Completed/FiniteStage/RelationIdeal.lean

1import FoxDifferential.Completed.FiniteStage.RelationAction

2import FoxDifferential.Completed.FiniteStage.Stage.Source

4/-

5PUBLIC_PAGE_SNAPSHOT

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

7lean_source: lean4/FoxDifferential/Completed/FiniteStage/RelationIdeal.lean

8translation_root: data/translation

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

10placement: after imports, never before imports

11-/

12/-!

13# Finite-stage relation augmentation ideal

15The finite-stage source quotient

16`F / ([N,N] N^n)` maps onto the target quotient `F/N`. The kernel of the induced group-algebra

17map is the two-sided ideal generated by the augmentation elements `q - 1` for relations

18`q ∈ ker(F/([N,N]N^n) -> F/N)`.

20This is the algebraic input used before the remaining finite Fox exactness step: a lifted target

21boundary cycle has source boundary in this concrete relation ideal, not merely in an anonymous

22kernel ideal.

23-/

25namespace FoxDifferential

27noncomputable section

29open ProCGroups.InverseSystems

30open ProCGroups.ProC

32universe u

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

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

37/-- The augmentation generator `q - 1` attached to a finite-stage relation

38`q ∈ ker(F/[N,N]N^n -> F/N)`. -/

39def finiteFoxStageRelationAugmentationGenerator

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

41 finiteFoxStageSourceGroupAlgebra (X := X) N n :=

42 MonoidAlgebra.of (ModNCompletedCoeff n)

43 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1

45/-- The source group-algebra ideal generated by finite-stage relation augmentation generators. -/

46def finiteFoxStageRelationAugmentationIdeal :

47 Ideal (finiteFoxStageSourceGroupAlgebra (X := X) N n) :=

48 Ideal.span

49 (Set.range (finiteFoxStageRelationAugmentationGenerator (X := X) N n))

51omit [DecidableEq X] in

52/-- A relation augmentation generator belongs to the relation augmentation ideal. -/

53theorem finiteFoxStageRelationAugmentationGenerator_mem_relationAugmentationIdeal

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

55 finiteFoxStageRelationAugmentationGenerator (X := X) N n q ∈

56 finiteFoxStageRelationAugmentationIdeal (X := X) N n := by

57 exact Ideal.subset_span ⟨q, rfl⟩

59omit [DecidableEq X] in

60/-- A relation augmentation generator maps to zero in the target group algebra. -/

61theorem finiteFoxStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel

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

63 finiteFoxStageRelationAugmentationGenerator (X := X) N n q ∈

64 finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n := by

65 rw [mem_finiteFoxStageGroupAlgebraMapKernelIdeal]

66 change finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

67 (MonoidAlgebra.of (ModNCompletedCoeff n)

68 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q.1 - 1) = 0

69 rw [map_sub, map_one, finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,

70 finiteFoxStageRelationGroup_target_eq_one]

71 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def, sub_self]

73omit [DecidableEq X] in

74/-- The generated relation augmentation ideal is contained in the kernel of the source-to-target

75finite group-algebra map. -/

76theorem finiteFoxStageRelationAugmentationIdeal_le_groupAlgebraMapKernel :

77 finiteFoxStageRelationAugmentationIdeal (X := X) N n ≤

78 finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n := by

79 refine Ideal.span_le.2 ?_

80 rintro x ⟨q, rfl⟩

81 exact finiteFoxStageRelationAugmentationGenerator_mem_groupAlgebraMapKernel (X := X) N n q

83/-- A section of the source-to-target finite group-algebra map, obtained by choosing a source

84quotient lift for each target quotient basis element. This is only a `Z/nZ`-linear section; no

85multiplicativity is asserted. -/

86def finiteFoxStageTargetGroupAlgebraSection :

87 finiteFoxStageTargetGroupAlgebra (X := X) N n →ₗ[ModNCompletedCoeff n]

88 finiteFoxStageSourceGroupAlgebra (X := X) N n :=

89 Finsupp.linearCombination (ModNCompletedCoeff n)

90 (fun h : finiteFoxStageTargetQuotient (X := X) N =>

91 MonoidAlgebra.of (ModNCompletedCoeff n)

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

93 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h))

95omit [DecidableEq X] in

96@[simp]

97theorem finiteFoxStageTargetGroupAlgebraSection_of

98 (h : finiteFoxStageTargetQuotient (X := X) N) :

99 finiteFoxStageTargetGroupAlgebraSection (X := X) N n

100 (MonoidAlgebra.of (ModNCompletedCoeff n)

101 (finiteFoxStageTargetQuotient (X := X) N) h) =

102 MonoidAlgebra.of (ModNCompletedCoeff n)

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

104 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h) := by

105 change

106 (Finsupp.linearCombination (ModNCompletedCoeff n)

107 (fun h : finiteFoxStageTargetQuotient (X := X) N =>

108 MonoidAlgebra.of (ModNCompletedCoeff n)

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

110 (finiteFoxStageTargetQuotientLiftToSource (X := X) N n h)))

111 (Finsupp.single h (1 : ModNCompletedCoeff n)) = _

112 rw [Finsupp.linearCombination_single, one_smul]

113

114omit [DecidableEq X] in

115/-- The chosen group-algebra section is a right inverse to the finite source-to-target map. -/

116theorem finiteFoxCommutatorPowerGroupAlgebraMap_section

117 (y : finiteFoxStageTargetGroupAlgebra (X := X) N n) :

118 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

119 (finiteFoxStageTargetGroupAlgebraSection (X := X) N n y) = y := by

120 classical

121 refine MonoidAlgebra.induction_on

122 (p := fun y : finiteFoxStageTargetGroupAlgebra (X := X) N n =>

123 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

124 (finiteFoxStageTargetGroupAlgebraSection (X := X) N n y) = y)

125 y ?single ?add ?smul

126 · intro h

127 rw [finiteFoxStageTargetGroupAlgebraSection_of,

128 finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,

129 finiteFoxStageTargetQuotientLiftToSource_spec]

130 · intro x y hx hy

131 simp only [map_add, hx, hy]

132 · intro a x hx

133 rw [map_smul, finiteFoxCommutatorPowerGroupAlgebraMap_smul]

134 simp only [hx]

135

136omit [DecidableEq X] in

137/-- The finite source-to-target group-algebra map is surjective. -/

138theorem finiteFoxCommutatorPowerGroupAlgebraMap_surjective :

139 Function.Surjective (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n) := by

140 intro y

141 exact ⟨finiteFoxStageTargetGroupAlgebraSection (X := X) N n y,

142 finiteFoxCommutatorPowerGroupAlgebraMap_section (X := X) N n y⟩

143

144omit [DecidableEq X] in

145/-- For a source basis element `s`, subtracting the chosen lift of its target image gives a

146relation-augmentation element. -/

147theorem finiteFoxStage_sourceBasis_sub_section_mem_relationAugmentationIdeal

148 (s : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :

149 MonoidAlgebra.of (ModNCompletedCoeff n)

150 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -

151 finiteFoxStageTargetGroupAlgebraSection (X := X) N n

152 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

153 (MonoidAlgebra.of (ModNCompletedCoeff n)

154 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) ∈

155 finiteFoxStageRelationAugmentationIdeal (X := X) N n := by

156 let t : finiteFoxStageTargetQuotient (X := X) N :=

157 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n s

158 let lift : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n :=

159 finiteFoxStageTargetQuotientLiftToSource (X := X) N n t

160 let q : finiteFoxStageRelationGroup (X := X) N n :=

161 ⟨lift⁻¹ * s, by

162 change finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n

163 (lift⁻¹ * s) = 1

164 rw [map_mul, map_inv]

165 have hlift :

166 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n lift = t := by

167 simp only [finiteFoxStageTargetQuotientLiftToSource_spec, lift, t]

168 rw [hlift]

169 simp only [inv_mul_cancel, t]⟩

170 have hsection :

171 finiteFoxStageTargetGroupAlgebraSection (X := X) N n

172 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

173 (MonoidAlgebra.of (ModNCompletedCoeff n)

174 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s)) =

175 MonoidAlgebra.of (ModNCompletedCoeff n)

176 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by

177 rw [finiteFoxCommutatorPowerGroupAlgebraMap_of_quotient,

178 finiteFoxStageTargetGroupAlgebraSection_of]

179 rw [hsection]

180 have hmul :

181 MonoidAlgebra.of (ModNCompletedCoeff n)

182 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift *

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

184 MonoidAlgebra.of (ModNCompletedCoeff n)

185 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) s -

186 MonoidAlgebra.of (ModNCompletedCoeff n)

187 (FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) lift := by

188 simp only [finiteFoxStageRelationAugmentationGenerator, q, MonoidAlgebra.of_apply]

189 rw [mul_sub, MonoidAlgebra.single_mul_single, mul_one]

190 simp only [mul_inv_cancel_left, mul_one]

191 rw [← hmul]

192 exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _

193 (finiteFoxStageRelationAugmentationGenerator_mem_relationAugmentationIdeal (X := X) N n q)

194

195omit [DecidableEq X] in

196/-- Every source group-algebra element differs from the chosen lift of its target image by a

197relation-augmentation element. -/

198theorem finiteFoxStage_sub_section_map_mem_relationAugmentationIdeal

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

200 x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

201 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈

202 finiteFoxStageRelationAugmentationIdeal (X := X) N n := by

203 classical

204 refine MonoidAlgebra.induction_on

205 (p := fun x : finiteFoxStageSourceGroupAlgebra (X := X) N n =>

206 x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

207 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x) ∈

208 finiteFoxStageRelationAugmentationIdeal (X := X) N n)

209 x ?single ?add ?smul

210 · intro s

211 exact finiteFoxStage_sourceBasis_sub_section_mem_relationAugmentationIdeal (X := X) N n s

212 · intro x y hx hy

213 have hcalc :

214 x + y - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

215 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (x + y)) =

216 (x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

217 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) +

218 (y - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

219 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n y)) := by

220 rw [map_add, map_add]

221 abel

222 rw [hcalc]

223 exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).add_mem hx hy

224 · intro a x hx

225 have hcalc :

226 a • x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

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

228 a • (x - finiteFoxStageTargetGroupAlgebraSection (X := X) N n

229 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x)) := by

230 rw [finiteFoxCommutatorPowerGroupAlgebraMap_smul, map_smul, smul_sub]

231 rw [hcalc]

232 rw [Algebra.smul_def]

233 exact (finiteFoxStageRelationAugmentationIdeal (X := X) N n).mul_mem_left _ hx

234

235omit [DecidableEq X] in

236/-- The kernel ideal of the finite source-to-target group-algebra map is exactly the ideal

237spanned by relation augmentation generators. -/

238theorem finiteFoxStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal :

239 finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n =

240 finiteFoxStageRelationAugmentationIdeal (X := X) N n := by

241 apply le_antisymm

242 · intro x hx

243 have hxmap :

244 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n x = 0 :=

245 (mem_finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) (N := N) (n := n)).1 hx

246 have hdiff :=

247 finiteFoxStage_sub_section_map_mem_relationAugmentationIdeal (X := X) N n x

248 rw [hxmap, map_zero, sub_zero] at hdiff

249 exact hdiff

250 · exact finiteFoxStageRelationAugmentationIdeal_le_groupAlgebraMapKernel (X := X) N n

251

252omit [DecidableEq X] in

253/-- Kernel membership may be rewritten as membership in the explicit relation augmentation ideal. -/

254theorem finiteFoxStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal

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

256 x ∈ finiteFoxStageGroupAlgebraMapKernelIdeal (X := X) N n ↔

257 x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n := by

258 rw [finiteFoxStageGroupAlgebraMapKernelIdeal_eq_relationAugmentationIdeal]

259

260end

261

262end FoxDifferential