FoxDifferential/Completed/FiniteStage/RelationModule.lean
1import FoxDifferential.Completed.FiniteStage.BoundaryCycles
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/RelationModule.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 module for the Crowell density step
17complex over `Z/nZ[F/N]`.
18-/
20namespace FoxDifferential
22noncomputable section
24open ProCGroups.InverseSystems
25open ProCGroups.ProC
27universe u
29variable {X : Type u} [DecidableEq X]
30variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
32/-- The finite-stage relation group
34abbrev finiteFoxStageRelationGroup : Type u :=
38omit [DecidableEq X] in
39@[simp]
41 (q : finiteFoxStageRelationGroup (X := X) N n) :
43 (F := FreeGroup X) N n q.1 = 1 :=
44 q.2
46omit [DecidableEq X] in
47@[simp]
49 (q : finiteFoxStageRelationGroup (X := X) N n) :
50 finiteFoxStageQuotientCoefficient (X := X) N n q.1 = 1 :=
51 finiteFoxStageQuotientCoefficient_eq_one_of_kernel (X := X) N n q.2
53/-- The finite-stage relation boundary, written additively:
54`N/[N,N]N^n -> (Z/nZ[F/N])^X`. -/
56 Additive (finiteFoxStageRelationGroup (X := X) N n) →+
57 finiteFoxStageCoordinateVector (X := X) N n :=
58 IsCrossedDifferential.restrictTrivialSubgroupAddMonoidHom
59 (finiteFoxStageQuotientDerivativeVector_isCrossedDifferential (X := X) N n)
62 (fun q => finiteFoxStageQuotientCoefficient_relation_eq_one (X := X) N n q)
64@[simp]
66 (q : finiteFoxStageRelationGroup (X := X) N n) :
67 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n (Additive.ofMul q) =
68 finiteFoxStageQuotientDerivativeVector (X := X) N n q.1 :=
69 rfl
71/-- The relation-boundary image, as an additive subgroup of the finite coordinate module. -/
73 AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n) :=
74 finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n
76@[simp]
78 ((finiteFoxStageRelationBoundaryRange (X := X) N n :
79 AddSubgroup (finiteFoxStageCoordinateVector (X := X) N n)) :
80 Set (finiteFoxStageCoordinateVector (X := X) N n)) =
81 finiteFoxStageSourceKernelDerivativeSet (X := X) N n :=
82 rfl
84/-- Membership in the relation-boundary image is the existence of a relation whose Fox derivative
85is the given vector. -/
87 {v : finiteFoxStageCoordinateVector (X := X) N n} :
88 v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n ↔
89 ∃ q : Additive (finiteFoxStageRelationGroup (X := X) N n),
90 finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q = v := by
91 constructor
92 · intro hv
93 rcases hv with ⟨q, hq, hv⟩
94 let qrel : finiteFoxStageRelationGroup (X := X) N n := ⟨q, hq⟩
95 refine ⟨Additive.ofMul qrel, ?_⟩
96 simpa [qrel] using hv
97 · rintro ⟨q, hq⟩
98 let qrel : finiteFoxStageRelationGroup (X := X) N n := Additive.toMul q
99 refine ⟨qrel.1, qrel.2, ?_⟩
100 simpa [qrel] using hq
102/-- The finite-stage relation boundary lands in finite Fox boundary cycles. -/
104 [Fintype X] (q : Additive (finiteFoxStageRelationGroup (X := X) N n)) :
105 finiteFoxStageFoxBoundary (X := X) N n
106 (finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n q) = 0 := by
107 change
108 finiteFoxStageFoxBoundary (X := X) N n
109 (finiteFoxStageQuotientDerivativeVector (X := X) N n (Additive.toMul q).1) = 0
112 (X := X) N n (Additive.toMul q).2]
113 simp only [sub_self]
115/-- The relation-boundary range is contained in `ker ∂`. -/
117 [Fintype X] :
118 finiteFoxStageRelationBoundaryRange (X := X) N n ≤
119 (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).toAddSubgroup := by
120 intro v hv
121 rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n] at hv
122 rcases hv with ⟨q, rfl⟩
123 exact finiteFoxStageFoxBoundary_relationBoundary_eq_zero (X := X) N n q
125/-- Finite-stage exactness at the coordinate module, stated as a named proposition. -/
126def finiteFoxStageRelationBoundaryExact [Fintype X] : Prop :=
127 Function.Exact
128 (finiteFoxStageRelationBoundaryAddMonoidHom (X := X) N n)
129 (finiteFoxStageFoxBoundary (X := X) N n)
131/-- Finite-stage exactness is equivalent to the coverage statement formulated in
132`BoundaryCycles.lean`. -/
134 [Fintype X] :
135 finiteFoxStageRelationBoundaryExact (X := X) N n ↔
136 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n := by
137 constructor
138 · intro hexact v hv
139 have hvzero : finiteFoxStageFoxBoundary (X := X) N n v = 0 := hv
140 rcases (hexact v).1 hvzero with ⟨q, hq⟩
141 change v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n
142 rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n]
143 exact ⟨q, hq⟩
144 · intro hcovered v
145 constructor
146 · intro hvzero
147 have hvcycle : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n := hvzero
148 have hvsource : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n :=
149 hcovered hvcycle
150 have hvsourceRange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := by
151 change v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n
152 exact hvsource
153 rw [mem_finiteFoxStageRelationBoundaryRange_iff (X := X) N n] at hvsourceRange
154 exact hvsourceRange
155 · rintro ⟨q, hq⟩
156 rw [← hq]
157 exact finiteFoxStageFoxBoundary_relationBoundary_eq_zero (X := X) N n q
159/-- Coverage of finite boundary cycles gives finite-stage exactness in the usual function-level
160form. -/
162 [Fintype X]
163 (hcovered : finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n) :
164 finiteFoxStageRelationBoundaryExact (X := X) N n :=
166 (X := X) N n).2 hcovered
168/-- Function-level finite-stage exactness gives the set-level coverage used by the density step. -/
170 [Fintype X]
171 (hexact : finiteFoxStageRelationBoundaryExact (X := X) N n) :
172 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
174 (X := X) N n).1 hexact
176end
178end FoxDifferential