FoxDifferential/Completed/FiniteStage/RelationSubmodule.lean

1import FoxDifferential.Completed.FiniteStage.RelationAction

3/-

4PUBLIC_PAGE_SNAPSHOT

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

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

7translation_root: data/translation

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

9placement: after imports, never before imports

10-/

11/-!

12# Finite-stage relation-boundary submodule

14The finite-stage relation boundary image is naturally an additive subgroup, because it comes from

15`ker(F/[N,N]N^n -> F/N)`. The finite Blanchfield--Lyndon statement is module-theoretic, so this

16file packages the `Z/nZ[F/N]`-submodule generated by those relation-boundary vectors and separates

17module-level exactness from the stronger set-level source-kernel coverage needed in the completed

18density step.

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/-- The `Z/nZ[F/N]`-submodule generated by finite-stage relation-boundary vectors. -/

34def finiteFoxStageRelationBoundarySubmodule :

35 Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)

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

37 Submodule.span (finiteFoxStageTargetGroupAlgebra (X := X) N n)

38 (finiteFoxStageRelationBoundaryRange (X := X) N n :

39 Set (finiteFoxStageCoordinateVector (X := X) N n))

41/-- Every actual relation-boundary vector lies in the generated relation-boundary submodule. -/

42theorem finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule :

43 (finiteFoxStageRelationBoundaryRange (X := X) N n :

44 Set (finiteFoxStageCoordinateVector (X := X) N n)) ⊆

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

46 exact Submodule.subset_span

48/-- A relation boundary of a finite-stage relation lies in the generated submodule. -/

49theorem finiteFoxStageRelationBoundaryAddMonoidHom_mem_relationBoundarySubmodule

50 (q : Additive (finiteFoxStageRelationGroup (X := X) N n)) :

51 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q ∈

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

53 apply finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n

54 exact (mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n).2 ⟨q, rfl⟩

56/-- The actual relation-boundary image is stable under arbitrary finite group-algebra scalars. -/

57theorem finiteFoxStageRelationBoundaryRange_smul_mem

58 (a : finiteFoxStageTargetGroupAlgebra (X := X) N n)

59 {v : finiteFoxStageCoordinateVector (X := X) N n}

60 (hv : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n) :

61 a • v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by

62 classical

63 refine MonoidAlgebra.induction_linear

64 (M := finiteFoxStageTargetQuotient (X := X) N)

65 (R := ModNCompletedCoeff n)

66 (p := fun a : finiteFoxStageTargetGroupAlgebra (X := X) N n =>

67 a • v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n)

68 a ?zero ?add ?single

69 · simp only [zero_smul, zero_mem]

70 · intro a b ha hb

71 rw [add_smul]

72 exact (finiteFoxStageRelationBoundaryRange (X := X) N n).add_mem ha hb

73 · intro h c

74 rcases ZMod.intCast_surjective c with ⟨m, rfl⟩

75 have hbase :

76 (MonoidAlgebra.of (ModNCompletedCoeff n)

77 (finiteFoxStageTargetQuotient (X := X) N) h) • v ∈

78 finiteFoxStageRelationBoundaryRange (X := X) N n :=

79 finiteFoxStageRelationBoundaryRange_basis_smul_mem (X := X) N n h hv

80 have hsingle :

81 ((MonoidAlgebra.single h (m : ModNCompletedCoeff n) :

82 finiteFoxStageTargetGroupAlgebra (X := X) N n) • v :

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

84 (m : ℤ) •

85 ((MonoidAlgebra.of (ModNCompletedCoeff n)

86 (finiteFoxStageTargetQuotient (X := X) N) h) • v :

87 finiteFoxStageCoordinateVector (X := X) N n) := by

88 have hsingleAlg :

89 (MonoidAlgebra.single h (m : ModNCompletedCoeff n) :

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

91 (m : ModNCompletedCoeff n) •

92 MonoidAlgebra.of (ModNCompletedCoeff n)

93 (finiteFoxStageTargetQuotient (X := X) N) h := by

94 simp only [MonoidAlgebra.of, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.smul_single, smul_eq_mul, mul_one]

95 rw [hsingleAlg]

96 rw [smul_assoc]

97 exact Int.cast_smul_eq_zsmul (ModNCompletedCoeff n) m

98 ((MonoidAlgebra.of (ModNCompletedCoeff n)

99 (finiteFoxStageTargetQuotient (X := X) N) h) • v :

100 finiteFoxStageCoordinateVector (X := X) N n)

101 rw [hsingle]

102 exact (finiteFoxStageRelationBoundaryRange (X := X) N n).zsmul_mem hbase m

103

104/-- The actual relation-boundary image as a finite group-algebra submodule. -/

105def finiteFoxStageRelationBoundaryImageSubmodule :

106 Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)

107 (finiteFoxStageCoordinateVector (X := X) N n) where

108 carrier := finiteFoxStageRelationBoundaryRange (X := X) N n

109 zero_mem' := (finiteFoxStageRelationBoundaryRange (X := X) N n).zero_mem

110 add_mem' := by

111 intro x y hx hy

112 exact (finiteFoxStageRelationBoundaryRange (X := X) N n).add_mem hx hy

113 smul_mem' := by

114 intro a v hv

115 exact finiteFoxStageRelationBoundaryRange_smul_mem (X := X) N n a hv

116

117@[simp]

118theorem finiteFoxStageRelationBoundaryImageSubmodule_coe :

119 ((finiteFoxStageRelationBoundaryImageSubmodule (X := X) N n :

120 Submodule (finiteFoxStageTargetGroupAlgebra (X := X) N n)

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

122 Set (finiteFoxStageCoordinateVector (X := X) N n)) =

123 finiteFoxStageSourceKernelDerivativeSet (X := X) N n := by

124 simp only [finiteFoxStageRelationBoundaryImageSubmodule, finiteFoxStageRelationBoundaryRange_coe,

125 Submodule.coe_set_mk, AddSubmonoid.coe_set_mk, AddSubsemigroup.coe_set_mk]

126

127/-- The generated relation-boundary submodule is the actual relation-boundary image, because the

128image is already stable under the finite target group algebra. -/

129theorem finiteFoxStageRelationBoundarySubmodule_eq_imageSubmodule :

130 finiteFoxStageRelationBoundarySubmodule (X := X) N n =

131 finiteFoxStageRelationBoundaryImageSubmodule (X := X) N n := by

132 apply le_antisymm

133 · refine Submodule.span_le.2 ?_

134 intro v hv

135 exact hv

136 · intro v hv

137 exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule (X := X) N n hv

138

139

140/-- The relation-boundary submodule is contained in the finite Fox boundary cycles. -/

141theorem finiteFoxStageRelationBoundarySubmodule_le_boundaryCycleSubmodule

142 [Fintype X] :

143 finiteFoxStageRelationBoundarySubmodule (X := X) N n ≤

144 finiteFoxStageBoundaryCycleSubmodule (X := X) N n := by

145 refine Submodule.span_le.2 ?_

146 intro v hv

147 exact finiteFoxStageRelationBoundary_range_le_boundaryCycleSubmodule (X := X) N n hv

148

149/-- Module-level finite-stage exactness at the coordinate module:

150`ker ∂` is contained in the submodule generated by finite relation boundaries. -/

151def finiteFoxStageRelationBoundaryModuleExact [Fintype X] : Prop :=

152 finiteFoxStageBoundaryCycleSubmodule (X := X) N n ≤

153 finiteFoxStageRelationBoundarySubmodule (X := X) N n

154

155/-- Function-level relation-boundary exactness implies the module-level finite exactness target. -/

156theorem finiteFoxStageRelationBoundaryModuleExact_of_relationBoundaryExact

157 [Fintype X]

158 (hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :

159 finiteFoxStageRelationBoundaryModuleExact (X := X) N n := by

160 intro v hv

161 have hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=

162 finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryExact

163 (X := X) N n hexact

164 have hvsource : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n :=

165 hcovered hv

166 have hvrange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by

167 change v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n

168 exact hvsource

169 exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule

170 (X := X) N n hvrange

171

172/-- The set-level finite coverage target implies the module-level finite exactness target. -/

173theorem finiteFoxStageRelationBoundaryModuleExact_of_boundaryCyclesCoveredBySourceKernel

174 [Fintype X]

175 (hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :

176 finiteFoxStageRelationBoundaryModuleExact (X := X) N n := by

177 intro v hv

178 have hvsource : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n := hcovered hv

179 have hvrange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by

180 change v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n

181 exact hvsource

182 exact finiteFoxStageRelationBoundaryRange_subset_relationBoundarySubmodule

183 (X := X) N n hvrange

184

185/-- Module-level finite exactness is strong enough to recover the set-level source-kernel coverage,

186because the relation-boundary image is already a finite group-algebra submodule. -/

187theorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

188 [Fintype X]

189 (hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :

190 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n := by

191 intro v hv

192 have hvrel : v ∈ finiteFoxStageRelationBoundarySubmodule (X := X) N n := hexact hv

193 rw [finiteFoxStageRelationBoundarySubmodule_eq_imageSubmodule (X := X) N n] at hvrel

194 simpa [finiteFoxStageRelationBoundaryImageSubmodule] using hvrel

195

196

197/-- Module exactness is equivalent to equality between `ker ∂` and the generated relation-boundary

198submodule. -/

199theorem finiteFoxStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule

200 [Fintype X] :

201 finiteFoxStageRelationBoundaryModuleExact (X := X) N n ↔

202 finiteFoxStageRelationBoundarySubmodule (X := X) N n =

203 finiteFoxStageBoundaryCycleSubmodule (X := X) N n := by

204 constructor

205 · intro hexact

206 exact le_antisymm

207 (finiteFoxStageRelationBoundarySubmodule_le_boundaryCycleSubmodule (X := X) N n)

208 hexact

209 · intro h v hv

210 rw [h]

211 exact hv

212

213/-- Function-level finite exactness identifies `ker ∂` with the generated relation-boundary

214submodule. -/

215theorem relationBoundarySubmodule_eq_boundaryCycleSubmodule_of_relExact

216 [Fintype X]

217 (hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :

218 finiteFoxStageRelationBoundarySubmodule (X := X) N n =

219 finiteFoxStageBoundaryCycleSubmodule (X := X) N n :=

220 (finiteFoxStageRelationBoundaryModuleExact_iff_submodule_eq_boundaryCycleSubmodule

221 (X := X) N n).1

222 (finiteFoxStageRelationBoundaryModuleExact_of_relationBoundaryExact

223 (X := X) N n hexact)

224

225end

226

227end FoxDifferential