FoxDifferential/Completed/FiniteStage/RelationRealization.lean
1import FoxDifferential.Completed.FiniteStage.RelationSubmodule
2import FoxDifferential.Completed.FiniteStage.BoundarySubgroups
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FoxDifferential/Completed/FiniteStage/RelationRealization.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
16This file proves that the generated submodule is not larger than the actual source-kernel
18conjugating relations.
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 additive source-kernel derivative set is closed under integer multiples. -/
35 (m : ℤ) {v : finiteFoxStageCoordinateVector (X := X) N n}
36 (hv : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) :
37 m • v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n := by
38 have hv' : v ∈ finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n := hv
39 exact (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).zsmul_mem hv' m
41/-- The source-kernel derivative set is stable under multiplication by target-group basis
43target quotient element. -/
45 (h : finiteFoxStageTargetQuotient (X := X) N)
46 {v : finiteFoxStageCoordinateVector (X := X) N n}
47 (hv : v ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) :
48 (MonoidAlgebra.of (ModNCompletedCoeff n)
49 (finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
50 finiteFoxStageSourceKernelDerivativeSet (X := X) N n := by
51 have hvRange : v ∈ finiteFoxStageRelationBoundaryRange (X := X) N n := hv
52 exact finiteFoxStageRelationBoundaryRange_basis_smul_mem (X := X) N n h hvRange
54/-- Word-level finite relation derivatives are stable under multiplication by target-group basis
55coefficients, after rewriting the source-kernel and word-level descriptions. -/
57 (h : finiteFoxStageTargetQuotient (X := X) N)
58 {v : finiteFoxStageCoordinateVector (X := X) N n}
59 (hv : v ∈ finiteFoxStageKernelWordDerivativeSet (X := X) N n) :
60 (MonoidAlgebra.of (ModNCompletedCoeff n)
61 (finiteFoxStageTargetQuotient (X := X) N) h) • v ∈
62 finiteFoxStageKernelWordDerivativeSet (X := X) N n := by
63 rw [← finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n]
64 rw [← finiteFoxStageSourceKernelDerivativeSet_eq_kernelWordDerivativeSet (X := X) N n] at hv
65 exact finiteFoxStageSourceKernelDerivativeSet_basis_smul_mem (X := X) N n h hv
67/-- Module-level finite exactness gives function-level finite exactness for the relation boundary
68followed by the Fox boundary. -/
70 [Fintype X]
71 (hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
72 finiteFoxStageRelationBoundaryExact (X := X) N n :=
74 (X := X) N n
76 (X := X) N n hexact)
78/-- Module-level finite exactness gives finite semidirect coverage of boundary cycles `(v,1)`. -/
80 [Fintype X]
81 (hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
82 finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n :=
83 (finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2
85 (X := X) N n hexact)
88end
90end FoxDifferential