FoxDifferential/Completed/FiniteStage/SourceBoundary.lean

1import FoxDifferential.Completed.FiniteStage.RelationIdeal

2import FoxDifferential.Completed.FiniteStage.BoundaryQuotient

3import FoxDifferential.Completed.FiniteStage.SemidirectCycles

5/-

6PUBLIC_PAGE_SNAPSHOT

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

8lean_source: lean4/FoxDifferential/Completed/FiniteStage/SourceBoundary.lean

9translation_root: data/translation

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

11placement: after imports, never before imports

12-/

13/-!

14# Source-coordinate lifts of finite Fox boundary cycles

16This file adds the source-side coordinate layer needed for the finite-stage exactness attack.

17A target cycle `v ∈ ker ∂` can be lifted coordinatewise to the source group algebra

18`(Z/nZ)[F/([N,N]N^n)]`; its source Fox boundary then lies in the explicit relation augmentation

19ideal generated by `q - 1` for finite-stage relations `q`.

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/-- Source-valued coordinate vectors over `(Z/nZ)[F/([N,N]N^n)]`. -/

35abbrev finiteFoxStageSourceCoordinateVector : Type u :=

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

38/-- The source Fox boundary/Euler map

39`a ↦ Σ_i a_i([x_i]-1)` over the source quotient. -/

40def finiteFoxStageSourceFoxBoundary [Fintype X] :

41 finiteFoxStageSourceCoordinateVector (X := X) N n →ₗ[

42 finiteFoxStageSourceGroupAlgebra (X := X) N n]

43 finiteFoxStageSourceGroupAlgebra (X := X) N n where

44 toFun v :=

45 ∑ i : X,

46 v i *

47 (MonoidAlgebra.of (ModNCompletedCoeff n)

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

49 (QuotientGroup.mk'

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

51 (FreeGroup.of i)) - 1)

52 map_add' := by

53 intro v w

54 simp only [Pi.add_apply, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, add_mul, Finset.sum_add_distrib]

55 map_smul' := by

56 intro r v

57 simp only [Pi.smul_apply, smul_eq_mul, QuotientGroup.mk'_apply, MonoidAlgebra.of_apply, mul_assoc,

58 RingHom.id_apply, Finset.mul_sum]

60omit [DecidableEq X] [N.Normal] in

61@[simp]

62theorem finiteFoxStageSourceFoxBoundary_apply [Fintype X]

63 (v : finiteFoxStageSourceCoordinateVector (X := X) N n) :

64 finiteFoxStageSourceFoxBoundary (X := X) N n v =

65 ∑ i : X,

66 v i *

67 (MonoidAlgebra.of (ModNCompletedCoeff n)

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

69 (QuotientGroup.mk'

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

71 (FreeGroup.of i)) - 1) :=

72 rfl

74/-- Apply the finite source-to-target group-algebra map coordinatewise. -/

75def finiteFoxStageCoordinateSourceToTarget :

76 finiteFoxStageSourceCoordinateVector (X := X) N n →ₗ[ModNCompletedCoeff n]

77 finiteFoxStageCoordinateVector (X := X) N n where

78 toFun v := fun i =>

79 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i)

80 map_add' := by

81 intro v w

82 funext i

83 simp only [Pi.add_apply, map_add]

84 map_smul' := by

85 intro a v

86 funext i

87 simp only [Pi.smul_apply, finiteFoxCommutatorPowerGroupAlgebraMap_smul, RingHom.id_apply]

89omit [DecidableEq X] in

90@[simp]

91theorem finiteFoxStageCoordinateSourceToTarget_apply

92 (v : finiteFoxStageSourceCoordinateVector (X := X) N n) (i : X) :

93 finiteFoxStageCoordinateSourceToTarget (X := X) N n v i =

94 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n (v i) :=

95 rfl

97omit [DecidableEq X] in

98/-- The source boundary commutes with the source-to-target group-algebra map. -/

99theorem finiteFoxStageFoxBoundary_coordinateSourceToTarget

100 [Fintype X]

101 (v : finiteFoxStageSourceCoordinateVector (X := X) N n) :

102 finiteFoxStageFoxBoundary (X := X) N n

103 (finiteFoxStageCoordinateSourceToTarget (X := X) N n v) =

104 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

105 (finiteFoxStageSourceFoxBoundary (X := X) N n v) := by

106 rw [finiteFoxStageFoxBoundary_apply, finiteFoxStageSourceFoxBoundary_apply]

107 rw [map_sum]

108 apply Finset.sum_congr rfl

109 intro i hi

110 rw [finiteFoxStageCoordinateSourceToTarget_apply, RingHom.map_mul, map_sub, map_one,

111 finiteFoxCommutatorPowerGroupAlgebraMap_of]

112

113omit [DecidableEq X] in

114/-- The coordinatewise source-to-target map is surjective. -/

115theorem finiteFoxStageCoordinateSourceToTarget_surjective :

116 Function.Surjective (finiteFoxStageCoordinateSourceToTarget (X := X) N n) := by

117 intro v

118 have hcoord : ∀ i : X,

119 ∃ a : finiteFoxStageSourceGroupAlgebra (X := X) N n,

120 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n a = v i := by

121 intro i

122 exact finiteFoxCommutatorPowerGroupAlgebraMap_surjective (X := X) N n (v i)

123 choose a ha using hcoord

124 refine ⟨a, ?_⟩

125 funext i

126 exact ha i

127

128omit [DecidableEq X] in

129/-- If a source coordinate vector lifts a target boundary cycle, then its source boundary lies in

130 the source-to-target group-algebra kernel. -/

131theorem finiteFoxStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle

132 [Fintype X]

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

134 {a : finiteFoxStageSourceCoordinateVector (X := X) N n}

135 (ha : finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v)

136 (hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :

137 finiteFoxStageSourceFoxBoundary (X := X) N n a ∈

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

139 rw [mem_finiteFoxStageGroupAlgebraMapKernelIdeal]

140 calc

141 finiteFoxCommutatorPowerGroupAlgebraMap (F := FreeGroup X) N n

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

143 finiteFoxStageFoxBoundary (X := X) N n

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

145 exact (finiteFoxStageFoxBoundary_coordinateSourceToTarget (X := X) N n a).symm

146 _ = finiteFoxStageFoxBoundary (X := X) N n v := by

147 rw [ha]

148 _ = 0 := hv

149

150omit [DecidableEq X] in

151/-- If a source coordinate vector lifts a target boundary cycle, then its source boundary lies in

152 the explicit relation augmentation ideal. -/

153theorem finiteFoxStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle

154 [Fintype X]

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

156 {a : finiteFoxStageSourceCoordinateVector (X := X) N n}

157 (ha : finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v)

158 (hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :

159 finiteFoxStageSourceFoxBoundary (X := X) N n a ∈

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

161 rw [← finiteFoxStage_mem_groupAlgebraMapKernelIdeal_iff_relationAugmentationIdeal (X := X) N n]

162 exact finiteFoxStageSourceFoxBoundary_mem_groupAlgebraMapKernel_of_lift_cycle

163 (X := X) N n ha hv

164

165omit [DecidableEq X] in

166/-- Every finite target boundary cycle has a source-coordinate lift whose source boundary is in the

167relation augmentation ideal. -/

168theorem exists_finiteFoxStageSourceCoordinate_lift_boundaryCycle_relationIdeal

169 [Fintype X]

170 (v : finiteFoxStageCoordinateVector (X := X) N n)

171 (hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :

172 ∃ a : finiteFoxStageSourceCoordinateVector (X := X) N n,

173 finiteFoxStageCoordinateSourceToTarget (X := X) N n a = v ∧

174 finiteFoxStageSourceFoxBoundary (X := X) N n a ∈

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

176 rcases finiteFoxStageCoordinateSourceToTarget_surjective (X := X) N n v with ⟨a, ha⟩

177 exact ⟨a, ha,

178 finiteFoxStageSourceFoxBoundary_mem_relationAugmentationIdeal_of_lift_cycle

179 (X := X) N n ha hv⟩

180

181/-- Source-boundary relation-ideal reduction: if every source coordinate vector whose source

182boundary lies in the relation augmentation ideal projects to a relation-boundary vector, then the

183finite-stage coordinate complex is exact. -/

184def finiteFoxStageSourceBoundaryRelationIdealReduction [Fintype X] : Prop :=

185 ∀ a : finiteFoxStageSourceCoordinateVector (X := X) N n,

186 finiteFoxStageSourceFoxBoundary (X := X) N n a ∈

187 finiteFoxStageRelationAugmentationIdeal (X := X) N n →

188 finiteFoxStageCoordinateSourceToTarget (X := X) N n a ∈

189 finiteFoxStageRelationBoundarySubmodule (X := X) N n

190

191/-- The source-boundary relation-ideal reduction implies finite-stage module exactness. -/

192theorem finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction

193 [Fintype X]

194 (hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :

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

196 intro v hv

197 rcases exists_finiteFoxStageSourceCoordinate_lift_boundaryCycle_relationIdeal

198 (X := X) N n v hv with ⟨a, ha, hboundary⟩

199 have hrel := hreduce a hboundary

200 simpa [ha] using hrel

201

202/-- The source-boundary relation-ideal reduction implies finite-stage coordinate coverage. -/

203theorem finiteFoxStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction

204 [Fintype X]

205 (hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :

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

207 finiteFoxStageBoundaryCyclesCoveredBySourceKernel_of_relationBoundaryModuleExact

208 (X := X) N n

209 (finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction

210 (X := X) N n hreduce)

211

212/-- The source-boundary relation-ideal reduction gives injectivity of the finite quotient

213obstruction boundary. -/

214theorem finiteFoxStageBoundaryModuloRelations_inj_of_sourceBoundaryRelReduction

215 [Fintype X]

216 (hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :

217 Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n) :=

218 finiteFoxStageBoundaryModuloRelations_injective_of_relationBoundaryModuleExact

219 (X := X) N n

220 (finiteFoxStageRelationBoundaryModuleExact_of_sourceBoundaryRelReduction

221 (X := X) N n hreduce)

222

223/-- The source-boundary relation-ideal reduction gives the finite semidirect coverage statement. -/

224theorem finiteFoxStageSemiBoundaryCyclesCovered_of_sourceBoundaryRelReduction

225 [Fintype X]

226 (hreduce : finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n) :

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

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

229 (finiteFoxStageBoundaryCyclesCovered_of_sourceBoundaryRelReduction

230 (X := X) N n hreduce)

231

232end

233

234end FoxDifferential