FoxDifferential/Completed/FiniteStage/BoundarySubgroups.lean
1import FoxDifferential.Completed.FiniteStage.SemidirectCycles
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FoxDifferential/Completed/FiniteStage/BoundarySubgroups.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 cycle subgroups
14The completed density argument is formulated inside a semidirect product. This file upgrades the
16step can be expressed as subgroup inclusion and quotient-kernel data.
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/-- Finite semidirect boundary cycles form a subgroup. -/
32def finiteFoxStageSemidirectBoundaryCycleSubgroup [Fintype X] :
33 Subgroup (FiniteFoxStageSemidirect (X := X) N n) where
34 carrier := finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n
35 one_mem' := by
36 constructor
37 · simp only [FiniteFoxStageSemidirect.one_right]
38 · exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).zero_mem
39 mul_mem' := by
40 intro y z hy hz
41 rcases hy with ⟨hyright, hyleft⟩
42 rcases hz with ⟨hzright, hzleft⟩
43 constructor
44 · simp only [FiniteFoxStageSemidirect.mul_right, hyright, hzright, mul_one]
45 · rw [FiniteFoxStageSemidirect.mul_left, hyright]
46 have hone :
47 (MonoidAlgebra.of (ModNCompletedCoeff n)
48 (finiteFoxStageTargetQuotient (X := X) N) 1 :
49 finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
50 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
51 rw [hone, one_smul]
52 exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).add_mem hyleft hzleft
53 inv_mem' := by
54 intro y hy
55 rcases hy with ⟨hyright, hyleft⟩
56 constructor
57 · simp only [FiniteFoxStageSemidirect.inv_right, hyright, inv_one]
58 · rw [FiniteFoxStageSemidirect.inv_left, hyright, inv_one]
59 have hone :
60 (MonoidAlgebra.of (ModNCompletedCoeff n)
61 (finiteFoxStageTargetQuotient (X := X) N) 1 :
62 finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
63 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
64 rw [hone, one_smul]
65 exact (finiteFoxStageBoundaryCycleSubmodule (X := X) N n).neg_mem hyleft
67omit [DecidableEq X] in
68@[simp]
69theorem finiteFoxStageSemidirectBoundaryCycleSubgroup_coe [Fintype X] :
70 ((finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N n :
71 Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
72 Set (FiniteFoxStageSemidirect (X := X) N n)) =
73 finiteFoxStageSemidirectBoundaryCycleSet (X := X) N n :=
74 rfl
76/-- Source-kernel semidirect points are exactly points with right component `1` and left
77component in the source-kernel derivative subgroup. -/
79 {y : FiniteFoxStageSemidirect (X := X) N n} :
80 y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n ↔
81 y.right = 1 ∧
82 y.left ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n := by
83 constructor
84 · rintro ⟨q, hq, hqy⟩
85 rw [← hqy]
86 exact ⟨rfl, ⟨q, hq, rfl⟩⟩
87 · rintro ⟨hyright, q, hq, hqleft⟩
88 refine ⟨q, hq, ?_⟩
89 apply FiniteFoxStageSemidirect.ext
90 · exact hqleft
91 · simpa [finiteFoxStageSemidirectSourceKernelPoint] using hyright.symm
93/-- Finite source-kernel derivative semidirect points form a subgroup. -/
95 Subgroup (FiniteFoxStageSemidirect (X := X) N n) where
96 carrier :=
97 { y | y.right = 1 ∧
98 y.left ∈ finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n }
99 one_mem' := by
100 exact ⟨rfl, (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).zero_mem⟩
101 mul_mem' := by
102 intro y z hy hz
103 rcases hy with ⟨hyright, hyleft⟩
104 rcases hz with ⟨hzright, hzleft⟩
105 constructor
106 · simp only [FiniteFoxStageSemidirect.mul_right, hyright, hzright, mul_one]
107 · rw [FiniteFoxStageSemidirect.mul_left, hyright]
108 have hone :
109 (MonoidAlgebra.of (ModNCompletedCoeff n)
110 (finiteFoxStageTargetQuotient (X := X) N) 1 :
111 finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
112 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
113 rw [hone, one_smul]
114 exact
115 (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).add_mem hyleft hzleft
116 inv_mem' := by
117 intro y hy
118 rcases hy with ⟨hyright, hyleft⟩
119 constructor
120 · simp only [FiniteFoxStageSemidirect.inv_right, hyright, inv_one]
121 · rw [FiniteFoxStageSemidirect.inv_left, hyright, inv_one]
122 have hone :
123 (MonoidAlgebra.of (ModNCompletedCoeff n)
124 (finiteFoxStageTargetQuotient (X := X) N) 1 :
125 finiteFoxStageTargetGroupAlgebra (X := X) N n) = 1 := by
126 simp only [MonoidAlgebra.of, MonoidAlgebra.single, MonoidHom.coe_mk, OneHom.coe_mk, MonoidAlgebra.one_def]
127 rw [hone, one_smul]
128 exact (finiteFoxStageSourceKernelDerivativeAddSubgroup (X := X) N n).neg_mem hyleft
130@[simp]
132 ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
133 Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
134 Set (FiniteFoxStageSemidirect (X := X) N n)) =
135 finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n :=
136 by
137 ext y
138 change
139 (y.right = 1 ∧
140 y.left ∈ finiteFoxStageSourceKernelDerivativeSet (X := X) N n) ↔
141 y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n
142 exact (finiteFoxStageSemidirectSourceKernelDerivativeSet_iff (X := X) N n).symm
144/-- The finite source-kernel derivative subgroup lies inside finite semidirect boundary cycles. -/
146 [Fintype X] :
147 finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ≤
148 finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N n := by
149 intro y hy
150 have hyset :
151 y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n := by
152 have hy' :
153 y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
154 Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
155 Set (FiniteFoxStageSemidirect (X := X) N n)) := hy
156 rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n] at hy'
157 exact hy'
159 (X := X) N n hyset
161/-- Semidirect finite-stage coverage is equivalently subgroup inclusion. -/
163 [Fintype X] :
164 finiteFoxStageSemidirectBoundaryCycleSubgroup (X := X) N n ≤
165 finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n ↔
166 finiteFoxStageBoundaryCyclesCoveredBySourceKernel (X := X) N n := by
167 constructor
168 · intro hsub
169 exact
170 (finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).1
171 (by
172 intro y hy
173 have hy' : y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :=
174 hsub hy
175 have hyset :
176 y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
177 Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
178 Set (FiniteFoxStageSemidirect (X := X) N n)) := hy'
179 rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n] at hyset
180 exact hyset)
181 · intro hcoord y hy
182 have hyset :
183 y ∈ finiteFoxStageSemidirectSourceKernelDerivativeSet (X := X) N n :=
184 (finiteFoxStageSemidirectBoundaryCyclesCoveredBySourceKernel_iff (X := X) N n).2
185 hcoord hy
186 change
187 y ∈ ((finiteFoxStageSemidirectSourceKernelDerivativeSubgroup (X := X) N n :
188 Subgroup (FiniteFoxStageSemidirect (X := X) N n)) :
189 Set (FiniteFoxStageSemidirect (X := X) N n))
190 rw [finiteFoxStageSemidirectSourceKernelDerivativeSubgroup_coe (X := X) N n]
191 exact hyset
193end
195end FoxDifferential