FoxDifferential/Completed/FiniteStage/SourceCycleReduction.lean
1import FoxDifferential.Completed.FiniteStage.RelationIdealPrimitive
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/SourceCycleReduction.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
15First, relation-ideal boundary terms should have relation-compatible source primitives. Second,
16source boundary cycles should project to the relation-boundary submodule. Together they imply the
18coverage statement.
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/-- Source boundary cycles in the source coordinate module. -/
34def finiteFoxStageSourceBoundaryCycleSubmodule [Fintype X] :
35 Submodule (finiteFoxStageSourceGroupAlgebra (X := X) N n)
36 (finiteFoxStageSourceCoordinateVector (X := X) N n) :=
37 LinearMap.ker (finiteFoxStageSourceFoxBoundary (X := X) N n)
39omit [DecidableEq X] [N.Normal] in
40@[simp]
41theorem mem_finiteFoxStageSourceBoundaryCycleSubmodule [Fintype X]
42 {p : finiteFoxStageSourceCoordinateVector (X := X) N n} :
43 p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n ↔
44 finiteFoxStageSourceFoxBoundary (X := X) N n p = 0 :=
45 Iff.rfl
47/-- Source-cycle projection exactness: every source Fox cycle maps to the target relation-boundary
48submodule. This is the source-quotient analogue of exactness before the relation-ideal
49correction. -/
50def finiteFoxStageSourceCycleProjectionExact [Fintype X] : Prop :=
51 ∀ p : finiteFoxStageSourceCoordinateVector (X := X) N n,
52 p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n →
53 finiteFoxStageCoordinateSourceToTarget (X := X) N n p ∈
54 finiteFoxStageRelationBoundarySubmodule (X := X) N n
56/-- Left-submodule version of the source-boundary reduction. -/
57def finiteFoxStageSourceBoundaryLeftRelationReduction [Fintype X] : Prop :=
58 ∀ a : finiteFoxStageSourceCoordinateVector (X := X) N n,
59 finiteFoxStageSourceFoxBoundary (X := X) N n a ∈
60 finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n →
61 finiteFoxStageCoordinateSourceToTarget (X := X) N n a ∈
62 finiteFoxStageRelationBoundarySubmodule (X := X) N n
64/-- Source-cycle projection exactness implies the reduction for the left relation-augmentation
65submodule, because elements of the left relation-augmentation submodule have explicit
66relation-compatible primitives. -/
68 [Fintype X]
69 (hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
70 finiteFoxStageSourceBoundaryLeftRelationReduction (X := X) N n := by
71 intro a ha
73 (X := X) N n ha with ⟨p, hpboundary, hprel⟩
74 have hcycle_ap :
75 a - p ∈ finiteFoxStageSourceBoundaryCycleSubmodule (X := X) N n := by
76 change finiteFoxStageSourceFoxBoundary (X := X) N n (a - p) = 0
77 rw [map_sub, hpboundary]
78 exact sub_self _
79 have haprel := hcycle (a - p) hcycle_ap
80 have hmap :
81 finiteFoxStageCoordinateSourceToTarget (X := X) N n a =
82 finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
83 finiteFoxStageCoordinateSourceToTarget (X := X) N n (a - p) := by
84 have hsub := map_sub (finiteFoxStageCoordinateSourceToTarget (X := X) N n) a p
85 calc
86 finiteFoxStageCoordinateSourceToTarget (X := X) N n a =
87 finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
88 (finiteFoxStageCoordinateSourceToTarget (X := X) N n a -
89 finiteFoxStageCoordinateSourceToTarget (X := X) N n p) := by
90 abel
91 _ = finiteFoxStageCoordinateSourceToTarget (X := X) N n p +
92 finiteFoxStageCoordinateSourceToTarget (X := X) N n (a - p) := by
93 rw [← hsub]
94 rw [hmap]
95 exact (finiteFoxStageRelationBoundarySubmodule (X := X) N n).add_mem hprel haprel
97/-- If the two-sided relation augmentation ideal is already generated by the same relation
98augmentation elements as a left source-submodule, source-cycle projection exactness implies the
101 [Fintype X]
102 (hideal_left :
103 ∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
104 x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
105 x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
106 (hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
107 finiteFoxStageSourceBoundaryRelationIdealReduction (X := X) N n := by
108 intro a ha
110 (X := X) N n hcycle a (hideal_left _ ha)
112/-- Finite-stage source-cycle projection exactness gives relation-boundary module exactness. -/
114 [Fintype X]
115 (hideal_left :
116 ∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
117 x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
118 x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
119 (hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
120 finiteFoxStageRelationBoundaryModuleExact (X := X) N n :=
122 (X := X) N n
124 (X := X) N n hideal_left hcycle)
126/-- The same inputs give finite coordinate coverage. -/
128 [Fintype X]
129 (hideal_left :
130 ∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
131 x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
132 x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
133 (hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
134 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
136 (X := X) N n
138 (X := X) N n hideal_left hcycle)
140/-- The same inputs give finite semidirect coverage. -/
142 [Fintype X]
143 (hideal_left :
144 ∀ x : finiteFoxStageSourceGroupAlgebra (X := X) N n,
145 x ∈ finiteFoxStageRelationAugmentationIdeal (X := X) N n →
146 x ∈ finiteFoxStageRelationAugmentationLeftSubmodule (X := X) N n)
147 (hcycle : finiteFoxStageSourceCycleProjectionExact (X := X) N n) :
148 finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
150 (X := X) N n
152 (X := X) N n hideal_left hcycle)
154end
156end FoxDifferential