FoxDifferential/Completed/FiniteStage/BoundaryQuotient.lean
1import FoxDifferential.Completed.FiniteStage.RelationSubmodule
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/BoundaryQuotient.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 boundary quotient
14This file adds the quotient-obstruction formulation of the finite-stage problem. After quotienting
16`∂` descends. Injectivity of the descended boundary is equivalent to module-level exactness at the
17coordinate module.
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/-- Finite coordinate vectors modulo the submodule generated by finite relation boundaries. -/
33abbrev finiteFoxStageCoordinateModuloRelations : Type u :=
34 finiteFoxStageCoordinateVector (X := X) N n ⧸
35 finiteFoxStageRelationBoundarySubmodule (X := X) N n
37/-- The finite Fox boundary descends to the quotient by relation boundaries. -/
38def finiteFoxStageBoundaryModuloRelations [Fintype X] :
39 finiteFoxStageCoordinateModuloRelations (X := X) N n →ₗ[
40 finiteFoxStageTargetGroupAlgebra (X := X) N n]
41 finiteFoxStageTargetGroupAlgebra (X := X) N n :=
42 Submodule.liftQ (finiteFoxStageRelationBoundarySubmodule (X := X) N n)
43 (finiteFoxStageFoxBoundary (X := X) N n)
46@[simp]
48 [Fintype X] (v : finiteFoxStageCoordinateVector (X := X) N n) :
49 finiteFoxStageBoundaryModuloRelations (X := X) N n
50 (Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) =
51 finiteFoxStageFoxBoundary (X := X) N n v := by
52 rfl
54/-- A boundary cycle represents zero in the relation quotient when module-level finite exactness
55holds. -/
57 [Fintype X]
58 (hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n)
59 {v : finiteFoxStageCoordinateVector (X := X) N n}
60 (hv : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n) :
61 (Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) = 0 := by
62 exact (Submodule.Quotient.mk_eq_zero
63 (p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) (x := v)).2
64 (hexact hv)
66/-- If module-level finite exactness holds, the descended finite boundary has trivial kernel. -/
68 [Fintype X]
69 (hexact : finiteFoxStageRelationBoundaryModuleExact (X := X) N n) :
70 Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n) := by
71 have hker : ∀ q : finiteFoxStageCoordinateModuloRelations (X := X) N n,
72 finiteFoxStageBoundaryModuloRelations (X := X) N n q = 0 → q = 0 := by
73 intro q
74 refine Submodule.Quotient.induction_on
75 (p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) q ?_
76 intro v hv
77 rw [finiteFoxStageBoundaryModuloRelations_mk] at hv
78 have hvcycle : v ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n := hv
80 (X := X) N n hexact hvcycle
81 intro x y hxy
82 have hsub : finiteFoxStageBoundaryModuloRelations (X := X) N n (x - y) = 0 := by
83 rw [map_sub, hxy, sub_self]
84 exact sub_eq_zero.mp (hker (x - y) hsub)
86/-- Injectivity of the descended finite boundary implies module-level finite exactness. -/
88 [Fintype X]
89 (hinj : Function.Injective (finiteFoxStageBoundaryModuloRelations (X := X) N n)) :
90 finiteFoxStageRelationBoundaryModuleExact (X := X) N n := by
91 intro v hv
92 have hq :
93 (Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) = 0 := by
94 apply hinj
95 calc
96 finiteFoxStageBoundaryModuloRelations (X := X) N n
97 (Submodule.Quotient.mk v : finiteFoxStageCoordinateModuloRelations (X := X) N n) =
98 finiteFoxStageFoxBoundary (X := X) N n v := by
100 _ = 0 := hv
101 _ = finiteFoxStageBoundaryModuloRelations (X := X) N n
102 (0 : finiteFoxStageCoordinateModuloRelations (X := X) N n) := by
104 exact (Submodule.Quotient.mk_eq_zero
105 (p := finiteFoxStageRelationBoundarySubmodule (X := X) N n) (x := v)).1 hq
107end
109end FoxDifferential