FoxDifferential/Completed/FiniteStage/BoundaryCycles.lean

1import FoxDifferential.Completed.FiniteStage.Stage.Derivative.Quotient.Fundamental

3/-

4PUBLIC_PAGE_SNAPSHOT

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

6lean_source: lean4/FoxDifferential/Completed/FiniteStage/BoundaryCycles.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 Fox boundary cycles

14This file packages the finite quotient algebra that sits below the completed density frontier.

15For a normal subgroup `N ≤ FreeGroup X` and modulus `n`, the source quotient

16`F / ([N,N] N^n)` carries a descended Fox derivative. Its kernel over `F/N` gives a concrete

17finite-stage relation-cycle subgroup inside the kernel of the finite Fox boundary

18`∂ : R[F/N]^X → R[F/N]`.

20The point of this file is to make the finite-stage exactness target explicit. The completed

21Crowell density step should be attacked by proving that every completed boundary cycle is detected

22at finite stages and then approximated by these finite source-kernel derivatives.

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 finite-stage Fox boundary-cycle submodule `ker ∂`. -/

38def finiteFoxStageBoundaryCycleSubmodule [Fintype X] :

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

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

41 LinearMap.ker (finiteFoxStageFoxBoundary (X := X) N n)

43omit [DecidableEq X] in

44@[simp]

45theorem mem_finiteFoxStageBoundaryCycleSubmodule [Fintype X]

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

47 v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n ↔

48 finiteFoxStageFoxBoundary (X := X) N n v = 0 :=

49 Iff.rfl

51/-- Quotient-level source-kernel derivatives in the finite stage. These are the finite-stage

52relation cycles coming from the kernel of `F/[N,N]N^n → F/N`. -/

53def finiteFoxStageSourceKernelDerivativeSet :

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

55 { v | ∃ q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n,

56 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧

57 finiteFoxStageQuotientDerivativeVector (X := X) N n q = v }

59/-- Word-level kernel derivatives in the finite stage. This is the algebraic form obtained from

60actual relation words `w ∈ N`. -/

61def finiteFoxStageKernelWordDerivativeSet :

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

63 { v | ∃ w : FreeGroup X,

64 w ∈ N ∧ finiteFoxStageDerivativeVector (X := X) N n w = v }

66omit [DecidableEq X] in

67@[simp]

68theorem finiteFoxStageCoefficient_eq_one_of_mem

69 {w : FreeGroup X} (hw : w ∈ N) :

70 finiteFoxStageCoefficient (X := X) N n w = 1 := by

71 rw [finiteFoxStageCoefficient_apply]

72 have hq : QuotientGroup.mk' N w = 1 :=

73 (QuotientGroup.eq_one_iff (N := N) w).2 hw

74 rw [hq]

75 rfl

77omit [DecidableEq X] in

78@[simp]

79theorem finiteFoxStageQuotientCoefficient_eq_one_of_kernel

80 {q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n}

81 (hq : finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1) :

82 finiteFoxStageQuotientCoefficient (X := X) N n q = 1 := by

83 rw [finiteFoxStageQuotientCoefficient_apply, hq]

84 rfl

86/-- Source-kernel derivatives form an additive subgroup of the finite coordinate module. -/

87def finiteFoxStageSourceKernelDerivativeAddSubgroup :

88 AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) where

89 carrier := finiteFoxStageSourceKernelDerivativeSet (X := X) N n

90 zero_mem' := by

91 refine ⟨1, ?_, ?_⟩

92 · simp only [map_one]

93 · simp only [finiteFoxStageQuotientDerivativeVector_one]

94 add_mem' := by

95 intro a b ha hb

96 rcases ha with ⟨q, hq, hqa⟩

97 rcases hb with ⟨r, hr, hrb⟩

98 refine ⟨q * r, ?_, ?_⟩

99 · rw [map_mul, hq, hr, one_mul]

100 · rw [finiteFoxStageQuotientDerivativeVector_mul]

101 rw [finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]

102 simp only [hqa, hrb, one_smul]

103 neg_mem' := by

104 intro a ha

105 rcases ha with ⟨q, hq, hqa⟩

106 refine ⟨q⁻¹, ?_, ?_⟩

107 · rw [map_inv, hq]

108 simp only [inv_one]

109 · rw [IsCrossedDifferential.inv

110 (finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)]

111 have hcoeff :

112 finiteFoxStageQuotientCoefficient (X := X) N n q⁻¹ = 1 := by

113 apply finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n

114 rw [map_inv, hq]

115 simp only [inv_one]

116 rw [hcoeff]

117 simp only [hqa, one_smul]

118

119@[simp]

120theorem finiteFoxStageSourceKernelDerivativeAddSubgroup_coe :

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

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

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

124 finiteFoxStageSourceKernelDerivativeSet (X := X) N n :=

125 rfl

126

127/-- The quotient-level and word-level descriptions of finite-stage source-kernel derivatives

128coincide. -/

129theorem finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet :

130 finiteFoxStageSourceKernelDerivativeSet (X := X) N n =

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

132 ext v

133 constructor

134 · rintro ⟨q, hq, hv⟩

135 rcases QuotientGroup.mk'_surjective

136 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q with ⟨w, rfl⟩

137 have hwN : w ∈ N := by

138 have hwq : QuotientGroup.mk' N w = 1 := by

139 simpa only [finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk] using hq

140 exact (QuotientGroup.eq_one_iff (N := N) w).1 hwq

141 refine ⟨w, hwN, ?_⟩

142 simpa using hv

143 · rintro ⟨w, hwN, hv⟩

144 refine ⟨QuotientGroup.mk'

145 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) w, ?_, ?_⟩

146 · rw [finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk]

147 exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN

148 · simpa [finiteFoxStageQuotientDerivativeVector_mk] using hv

149

150/-- Word-level kernel derivatives form an additive subgroup, transported from the quotient-level

151source-kernel subgroup. -/

152def finiteFoxStageKernelWordDerivativeAddSubgroup :

153 AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) :=

154 finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n

155

156@[simp]

157theorem finiteFoxStageKernelWordDerivativeAddSubgroup_coe :

158 ((finiteFoxStageKernelWordDerivativeAddSubgroup (X := X) N n :

159 AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n)) :

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

161 finiteFoxStageKernelWordDerivativeSet (X := X) N n := by

162 rw [finiteFoxStageKernelWordDerivativeAddSubgroup,

163 finiteFoxStageSourceKernelDerivativeAddSubgroup_coe,

164 finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet]

165

166/-- Every finite-stage source-kernel derivative is a finite Fox boundary cycle. -/

167theorem finiteFoxStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule

168 [Fintype X] :

169 finiteFoxStageSourceKernelDerivativeSet (X := X) N n ⊆

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

171 Set (finiteFoxStageCoordinateVector (X := X) N n)) := by

172 intro v hv

173 rcases hv with ⟨q, hq, rfl⟩

174 change finiteFoxStageFoxBoundary (X := X) N n

175 (finiteFoxStageQuotientDerivativeVector (X := X) N n q) = 0

176 rw [finiteFoxStageFoxBoundary_quotientDerivativeVector]

177 rw [finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n hq]

178 simp only [sub_self]

179

180/-- The finite-stage exactness target: every finite Fox boundary cycle is represented by a

181source-kernel derivative in `F/[N,N]N^n`. -/

182def finiteFoxStageBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=

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

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

185 finiteFoxStageSourceKernelDerivativeSet (X := X) N n

186

187/-- The finite-stage exactness target may equivalently be read using honest kernel words. -/

188theorem finiteFoxStageBoundaryCyclesCoveredBySourceKernel_iff_words

189 [Fintype X] :

190 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔

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

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

193 finiteFoxStageKernelWordDerivativeSet (X := X) N n := by

194 rw [finiteFoxStageBoundaryCyclesCoveredBySourceKernel,

195 finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet]

196

197/-- The finite-stage source-kernel derivative set is equal to `ker ∂` exactly when the reverse

198coverage inclusion holds. -/

199theorem finiteFoxStageSourceKernelDerivativeSet_eq_boundaryCycleSubmodule_iff

200 [Fintype X] :

201 finiteFoxStageSourceKernelDerivativeSet (X := X) N n =

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

203 Set (finiteFoxStageCoordinateVector (X := X) N n)) ↔

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

205 constructor

206 · intro h v hv

207 rw [h]

208 exact hv

209 · intro h

210 apply le_antisymm

211 · exact finiteFoxStageSourceKernelDerivativeSet_subset_boundaryCycleSubmodule (X := X) N n

212 · exact h

213

214end

215

216end FoxDifferential