FoxDifferential/Completed/FiniteStage/SemidirectCycles.lean
1import FoxDifferential.Completed.FiniteStage.BoundaryCycleHom
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/SemidirectCycles.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 semidirect boundary cycles
14The completed density argument takes place in a semidirect product. This file supplies the
17-/
19namespace FoxDifferential
21noncomputable section
23open ProCGroups.InverseSystems
24open ProCGroups.ProC
26universe u
28variable {X : Type u} [DecidableEq X]
29variable (N : Subgroup (FreeGroup X)) [N.Normal] (n : ℕ)
31/-- The finite semidirect point `(Dq,1)` attached to a source-quotient element. -/
33 (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
34 FiniteFoxStageSemidirect (X := X) N n :=
35 { left := finiteFoxStageQuotientDerivativeVector (X := X) N n q,
36 right := 1 }
38@[simp]
40 (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
41 (finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q).left =
42 finiteFoxStageQuotientDerivativeVector (X := X) N n q :=
43 rfl
45@[simp]
47 (q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) :
48 (finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q).right = 1 :=
49 rfl
51/-- The finite semidirect point `(Dw,1)` attached to a word. -/
52def finiteFoxStageSemidirectKernelWordPoint (w : FreeGroup X) :
53 FiniteFoxStageSemidirect (X := X) N n :=
54 { left := finiteFoxStageDerivativeVector (X := X) N n w,
55 right := 1 }
57@[simp]
58theorem finiteFoxStageSemidirectKernelWordPoint_left (w : FreeGroup X) :
59 (finiteFoxStageSemidirectKernelWordPoint (X := X) N n w).left =
60 finiteFoxStageDerivativeVector (X := X) N n w :=
61 rfl
63@[simp]
64theorem finiteFoxStageSemidirectKernelWordPoint_right (w : FreeGroup X) :
65 (finiteFoxStageSemidirectKernelWordPoint (X := X) N n w).right = 1 :=
66 rfl
68/-- Finite-stage boundary cycles as semidirect points `(v,1)` with `∂v = 0`. -/
69def finiteFoxStageSemidirectBoundaryCycleSet [Fintype X] :
70 Set (FiniteFoxStageSemidirect (X := X) N n) :=
71 { y | y.right = 1 ∧
72 y.left ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n }
74omit [DecidableEq X] in
75@[simp]
76theorem mem_finiteFoxStageSemidirectBoundaryCycleSet [Fintype X]
77 {y : FiniteFoxStageSemidirect (X := X) N n} :
78 y ∈ finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ↔
79 y.right = 1 ∧ y.left ∈ finiteFoxStageBoundaryCycleSubmodule (X := X) N n :=
80 Iff.rfl
82/-- Semidirect source-kernel derivative points in the finite stage. -/
84 Set (FiniteFoxStageSemidirect (X := X) N n) :=
85 { y | ∃ q : FreeGroup X ⧸ finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n,
86 finiteFoxCommutatorPowerQuotientMapToNormalQuotient (F := FreeGroup X) N n q = 1 ∧
87 finiteFoxStageSemidirectSourceKernelPoint (X := X) N n q = y }
89/-- Semidirect kernel-word derivative points in the finite stage. -/
91 Set (FiniteFoxStageSemidirect (X := X) N n) :=
92 { y | ∃ w : FreeGroup X,
93 w ∈ N ∧ finiteFoxStageSemidirectKernelWordPoint (X := X) N n w = y }
95/-- Source-kernel semidirect points and honest kernel-word semidirect points coincide. -/
97 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n =
98 finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n := by
99 ext y
100 constructor
101 · rintro ⟨q, hq, hy⟩
102 rcases QuotientGroup.mk'_surjective
103 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) q with ⟨w, rfl⟩
104 have hwN : w ∈ N := by
105 have hwq : QuotientGroup.mk' N w = 1 := by
106 simpa only [finiteFoxCommutatorPowerQuotientMapToNormalQuotient_mk] using hq
107 exact (QuotientGroup.eq_one_iff (N := N) w).1 hwq
108 refine ⟨w, hwN, ?_⟩
109 rw [← hy]
110 apply FiniteFoxStageSemidirect.ext
111 · exact (finiteFoxStageQuotientDerivativeVector_mk (X := X) N n w).symm
112 · simp only [finiteFoxStageSemidirectKernelWordPoint, finiteFoxStageSemidirectSourceKernelPoint,
113 QuotientGroup.mk'_apply]
114 · rintro ⟨w, hwN, hy⟩
115 refine ⟨QuotientGroup.mk'
116 (finiteFoxCommutatorPowerSubgroup (F := FreeGroup X) N n) w, ?_, ?_⟩
118 exact (QuotientGroup.eq_one_iff (N := N) w).2 hwN
119 · rw [← hy]
120 apply FiniteFoxStageSemidirect.ext
121 · exact finiteFoxStageQuotientDerivativeVector_mk (X := X) N n w
122 · simp only [finiteFoxStageSemidirectSourceKernelPoint, QuotientGroup.mk'_apply,
125/-- Every finite semidirect source-kernel derivative point is a semidirect boundary cycle. -/
127 [Fintype X] :
128 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ⊆
129 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n := by
130 intro y hy
131 rcases hy with ⟨q, hq, hy⟩
132 rw [← hy]
133 constructor
134 · simp only [finiteFoxStageSemidirectSourceKernelPoint]
136 (X := X) N n ⟨q, hq, rfl⟩
138/-- Every finite semidirect kernel-word derivative point is a semidirect boundary cycle. -/
140 [Fintype X] :
141 finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ⊆
142 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n := by
144 (X := X) N n]
146 (X := X) N n
148/-- Semidirect finite-stage coverage: every semidirect boundary cycle is represented by a
149source-kernel derivative point. -/
150def finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel [Fintype X] : Prop :=
151 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ⊆
152 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n
154/-- The semidirect finite-stage coverage target is equivalent to the coordinate coverage target. -/
156 [Fintype X] :
157 finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel (X := X) N n ↔
158 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n := by
159 constructor
160 · intro hcover v hv
161 have hy :
162 ({ left := v, right := (1 : finiteFoxStageTargetQuotient (X := X) N) } :
163 FiniteFoxStageSemidirect (X := X) N n) ∈
164 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n := by
165 exact ⟨rfl, hv⟩
166 rcases hcover hy with ⟨q, hq, hqy⟩
167 refine ⟨q, hq, ?_⟩
168 have hleft := congrArg (fun z : FiniteFoxStageSemidirect (X := X) N n => z.left) hqy
169 simpa [finiteFoxStageSemidirectSourceKernelPoint] using hleft
170 · intro hcover y hy
171 rcases hy with ⟨hyright, hyleft⟩
172 rcases hcover hyleft with ⟨q, hq, hqleft⟩
173 refine ⟨q, hq, ?_⟩
174 apply FiniteFoxStageSemidirect.ext
175 · simpa [finiteFoxStageSemidirectSourceKernelPoint] using hqleft
176 · simpa [finiteFoxStageSemidirectSourceKernelPoint] using hyright.symm
178/-- Finite-stage coverage may equivalently be read with honest kernel words. -/
180 [Fintype X] :
181 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n ⊆
182 finiteFoxStageSemidirectKernelWordDerivativeSet (X := X) N n ↔
183 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n := by
185 (X := X) N n]
186 exact finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n
188end
190end FoxDifferential