FoxDifferential/Completed/FiniteStage/RelationIdealPrimitive.lean

1import FoxDifferential.Completed.FiniteStage.SourceDerivativeVector

3/-

4PUBLIC_PAGE_SNAPSHOT

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

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

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Primitives for the finite-stage relation augmentation ideal

14A source relation augmentation element should be read as an actual source Fox boundary. This file

15packages the primitive statement: an element `x` of the source group algebra is primitive if

16`x = ∂_src p` for a source-coordinate vector `p` whose target projection is already in the

17relation-boundary submodule. The basic generators `q - 1` have such primitives by the source

18Fox fundamental formula.

19-/

21namespace FoxDifferential

23noncomputable section

25open ProCGroups.InverseSystems

26open ProCGroups.ProC

28universe u

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

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

33/-- An element of the source finite group algebra has a relation-compatible source Fox primitive

34if it is the source boundary of a vector whose target projection lies in the finite

35relation-boundary submodule. -/

36def finiteFoxStageSourceBoundaryPrimitive [Fintype X]

37 (x : finiteFoxStageSourceGroupAlgebra (X := X) N n) : Prop :=

38 ∃ p : finiteFoxStageSourceCoordinateVector (X := X) N n,

39 finiteFoxStageSourceFoxBoundary (X := X) N n p = x ∧

40 finiteFoxStageCoordinateSourceToTarget (X := X) N n p ∈

41 finiteFoxStageRelationBoundarySubmodule (X := X) N n

43/-- The zero source-boundary primitive. -/

44theorem finiteFoxStageSourceBoundaryPrimitive_zero [Fintype X] :

45 finiteFoxStageSourceBoundaryPrimitive (X := X) N n 0 := by

46 refine ⟨0, ?_, ?_⟩

47 · simp only [finiteFoxStageSourceFoxBoundary_apply, Pi.zero_apply, QuotientGroup.mk'_apply,

48 MonoidAlgebra.of_apply, zero_mul, Finset.sum_const_zero]

49 · exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).zero_mem

51/-- Source-boundary primitives are closed under addition. -/

52theorem finiteFoxStageSourceBoundaryPrimitive_add [Fintype X]

53 {x y : finiteFoxStageSourceGroupAlgebra (X := X) N n}

54 (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x)

55 (hy : finiteFoxStageSourceBoundaryPrimitive (X := X) N n y) :

56 finiteFoxStageSourceBoundaryPrimitive (X := X) N n (x + y) := by

57 rcases hx with ⟨px, hpx, hpxrel⟩

58 rcases hy with ⟨py, hpy, hpyrel⟩

59 refine ⟨px + py, ?_, ?_⟩

60 · rw [map_add, hpx, hpy]

61 · rw [map_add]

62 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).add_mem hpxrel hpyrel

64/-- Source-boundary primitives are closed under negation. -/

65theorem finiteFoxStageSourceBoundaryPrimitive_neg [Fintype X]

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

67 (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x) :

68 finiteFoxStageSourceBoundaryPrimitive (X := X) N n (-x) := by

69 rcases hx with ⟨p, hp, hprel⟩

70 refine ⟨-p, ?_, ?_⟩

71 · rw [map_neg, hp]

72 · rw [map_neg]

73 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).neg_mem hprel

75/-- Source-boundary primitives are closed under subtraction. -/

76theorem finiteFoxStageSourceBoundaryPrimitive_sub [Fintype X]

77 {x y : finiteFoxStageSourceGroupAlgebra (X := X) N n}

78 (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x)

79 (hy : finiteFoxStageSourceBoundaryPrimitive (X := X) N n y) :

80 finiteFoxStageSourceBoundaryPrimitive (X := X) N n (x - y) := by

81 simpa [sub_eq_add_neg] using

82 finiteFoxStageSourceBoundaryPrimitive_add (X := X) N n hx

83 (finiteFoxStageSourceBoundaryPrimitive_neg (X := X) N n hy)

85/-- Source-boundary primitives are closed under left multiplication by source coefficients. -/

86theorem finiteFoxStageSourceBoundaryPrimitive_smul [Fintype X]

87 (a : finiteFoxStageSourceGroupAlgebra (X := X) N n)

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

89 (hx : finiteFoxStageSourceBoundaryPrimitive (X := X) N n x) :

90 finiteFoxStageSourceBoundaryPrimitive (X := X) N n (a • x) := by

91 rcases hx with ⟨p, hp, hprel⟩

92 refine ⟨a • p, ?_, ?_⟩

93 · rw [map_smul, hp]

94 · rw [finiteFoxStageCoordinateSourceToTarget_smul_source]

95 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).smul_mem

96 (finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a) hprel

98/-- Source-boundary primitives form a left submodule of the source group algebra. -/

99def finiteFoxStageSourceBoundaryPrimitiveSubmodule [Fintype X] :

100 Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)

101 (finiteFoxStageSourceGroupAlgebra (X := X) N n) where

102 carrier := {x | finiteFoxStageSourceBoundaryPrimitive (X := X) N n x}

103 zero_mem' := finiteFoxStageSourceBoundaryPrimitive_zero (X := X) N n

104 add_mem' := by

105 intro x y hx hy

106 exact finiteFoxStageSourceBoundaryPrimitive_add (X := X) N n hx hy

107 smul_mem' := by

108 intro a x hx

109 exact finiteFoxStageSourceBoundaryPrimitive_smul (X := X) N n a hx

110

111@[simp]

112theorem finiteFoxStageSourceBoundaryPrimitiveSubmodule_coe [Fintype X] :

113 ((finiteFoxStageSourceBoundaryPrimitiveSubmodule (X := X) N n :

114 Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)

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

116 Set (finiteFoxStageSourceGroupAlgebra (X := X) N n)) =

117 {x | finiteFoxStageSourceBoundaryPrimitive (X := X) N n x} :=

118 rfl

119

120/-- The source primitive attached to a finite relation `q`. -/

121def finiteFoxStageRelationAugmentationPrimitiveVector

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

123 finiteFoxStageSourceCoordinateVector (X := X) N n :=

124 finiteFoxStageSourceDerivativeVector (X := X) N n q.1

125

126/-- The source boundary of the primitive vector for `q` is the augmentation generator `q - 1`. -/

127theorem finiteFoxStageSourceFoxBoundary_relationAugmentationPrimitiveVector

128 [Fintype X]

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

130 finiteFoxStageSourceFoxBoundary (X := X) N n

131 (finiteFoxStageRelationAugmentationPrimitiveVector (X := X) N n q) =

132 finiteFoxStageRelationAugmentationGenerator (X := X) N n q := by

133 rw [finiteFoxStageRelationAugmentationPrimitiveVector,

134 finiteFoxStageSourceFoxBoundary_sourceDerivativeVector,

135 finiteFoxStageRelationAugmentationGenerator]

136

137/-- The target projection of the primitive vector for `q` is the finite relation boundary of `q`. -/

138theorem finiteFoxStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector

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

140 finiteFoxStageCoordinateSourceToTarget (X := X) N n

141 (finiteFoxStageRelationAugmentationPrimitiveVector (X := X) N n q) =

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

143 rw [finiteFoxStageRelationAugmentationPrimitiveVector,

144 finiteFoxStageCoordinateSourceToTarget_sourceDerivativeVector,

145 finiteFoxStageRelationBoundaryAddMonoidHom_of]

146

147/-- Relation augmentation generators have relation-compatible source Fox primitives. -/

148theorem finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator

149 [Fintype X]

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

151 finiteFoxStageSourceBoundaryPrimitive (X := X) N n

152 (finiteFoxStageRelationAugmentationGenerator (X := X) N n q) := by

153 refine ⟨finiteFoxStageRelationAugmentationPrimitiveVector (X := X) N n q, ?_, ?_⟩

154 · exact finiteFoxStageSourceFoxBoundary_relationAugmentationPrimitiveVector

155 (X := X) N n q

156 · rw [finiteFoxStageCoordinateSourceToTarget_relationAugmentationPrimitiveVector]

157 exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule

158 (X := X) N n

159 ((mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n).2

160 ⟨Additive.ofMul q, rfl⟩)

161

162

163/-- Left multiplication of a relation augmentation generator by a source quotient basis element has

164an explicit relation-compatible source primitive. -/

165theorem finiteFoxStageSourceBoundaryPrimitive_sourceBasis_mul_relationAugmentationGenerator

166 [Fintype X]

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

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

169 finiteFoxStageSourceBoundaryPrimitive (X := X) N n

170 (MonoidAlgebra.of (ModNCompletedCoeff n)

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

172 finiteFoxStageRelationAugmentationGenerator (X := X) N n q) := by

173 simpa [Algebra.smul_def] using

174 finiteFoxStageSourceBoundaryPrimitive_smul (X := X) N n

175 (MonoidAlgebra.of (ModNCompletedCoeff n)

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

177 (finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator (X := X) N n q)

178

179/-- Source primitive for the right basis multiple `(q - 1)s`. The primitive is

180`D_src(qs) - D_src(s)`. -/

181def finiteFoxStageRelationAugmentationRightBasisPrimitiveVector

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

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

184 finiteFoxStageSourceCoordinateVector (X := X) N n :=

185 finiteFoxStageSourceDerivativeVector (X := X) N n (q.1 * s) -

186 finiteFoxStageSourceDerivativeVector (X := X) N n s

187

188/-- The source boundary of `D_src(qs) - D_src(s)` is `(q - 1)s`. -/

189theorem finiteFoxStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector

190 [Fintype X]

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

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

193 finiteFoxStageSourceFoxBoundary (X := X) N n

194 (finiteFoxStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =

195 finiteFoxStageRelationAugmentationGenerator (X := X) N n q *

196 MonoidAlgebra.of (ModNCompletedCoeff n)

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

198 rw [finiteFoxStageRelationAugmentationRightBasisPrimitiveVector, map_sub,

199 finiteFoxStageSourceFoxBoundary_sourceDerivativeVector,

200 finiteFoxStageSourceFoxBoundary_sourceDerivativeVector,

201 finiteFoxStageRelationAugmentationGenerator]

202 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, sub_eq_add_neg, neg_add_rev, neg_neg, add_comm,

203 add_left_comm, add_assoc, add_neg_cancel, add_zero, add_mul, MonoidAlgebra.single_mul_single, mul_one, neg_mul,

204 one_mul]

205

206/-- The target projection of `D_src(qs) - D_src(s)` is the relation boundary of `q`. -/

207theorem finiteFoxStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector

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

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

210 finiteFoxStageCoordinateSourceToTarget (X := X) N n

211 (finiteFoxStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s) =

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

213 rw [finiteFoxStageRelationAugmentationRightBasisPrimitiveVector, map_sub,

214 finiteFoxStageCoordinateSourceToTarget_sourceDerivativeVector,

215 finiteFoxStageCoordinateSourceToTarget_sourceDerivativeVector,

216 finiteFoxStageRelationBoundaryAddMonoidHom_of,

217 finiteFoxStageQuotientDerivativeVector_mul,

218 finiteFoxStageQuotientCoefficient_relation_eq_one]

219 simp only [one_smul, add_sub_cancel_right]

220

221/-- Right multiplication of a relation augmentation generator by a source quotient basis element

222has an explicit relation-compatible source primitive. -/

223theorem finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator_mul_sourceBasis

224 [Fintype X]

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

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

227 finiteFoxStageSourceBoundaryPrimitive (X := X) N n

228 (finiteFoxStageRelationAugmentationGenerator (X := X) N n q *

229 MonoidAlgebra.of (ModNCompletedCoeff n)

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

231 refine ⟨finiteFoxStageRelationAugmentationRightBasisPrimitiveVector (X := X) N n q s, ?_, ?_⟩

232 · exact finiteFoxStageSourceFoxBoundary_relationAugmentationRightBasisPrimitiveVector

233 (X := X) N n q s

234 · rw [finiteFoxStageCoordinateSourceToTarget_relationAugmentationRightBasisPrimitiveVector]

235 exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule

236 (X := X) N n

237 ((mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n).2

238 ⟨Additive.ofMul q, rfl⟩)

239

240/-- The left source-submodule generated by the relation augmentation generators. -/

241def finiteFoxStageRelationAugmentationLeftSubmodule [Fintype X] :

242 Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)

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

244 Submodule.span (finiteFoxStageSourceGroupAlgebra (X := X) N n)

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

246

247/-- The left relation-augmentation submodule is contained in the primitive submodule. -/

248theorem finiteFoxStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule

249 [Fintype X] :

250 finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n ≤

251 finiteFoxStageSourceBoundaryPrimitiveSubmodule (X := X) N n := by

252 refine Submodule.span_le.2 ?_

253 rintro x ⟨q, rfl⟩

254 exact finiteFoxStageSourceBoundaryPrimitive_relationAugmentationGenerator

255 (X := X) N n q

256

257/-- Membership in the left relation-augmentation submodule gives a relation-compatible source

258primitive. -/

259theorem finiteFoxStageSourceBoundaryPrimitive_of_mem_relationAugmentationLeftSubmodule

260 [Fintype X]

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

262 (hx : x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n) :

263 finiteFoxStageSourceBoundaryPrimitive (X := X) N n x :=

264 finiteFoxStageRelationAugmentationLeftSubmodule_le_primitiveSubmodule (X := X) N n hx

265

266end

267

268end FoxDifferential