FenchelNielsenZomorrodian/Profinite/CuspedQuotient.lean
1import FenchelNielsenZomorrodian.Discrete.Coordinates.FenchelPeriodCoordinate
2import FenchelNielsenZomorrodian.Profinite.SmoothQuotient
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Profinite/CuspedQuotient.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15Constructs direct finite abelian quotients for profinite Fenchel groups with cusps, preserving every inertia order and giving derived length one.
16-/
18namespace FenchelNielsen
20universe u v
22namespace ProfiniteFGroup
24open scoped BigOperators
26private theorem ulift_list_prod_down {α : Type v} [Monoid α]
27 (xs : List (ULift.{u, v} α)) :
28 xs.prod.down = (xs.map (fun x => x.down)).prod := by
29 induction xs with
30 | nil =>
31 rfl
32 | cons x xs ih =>
33 simp only [List.prod_cons, ULift.mul_down, ih, List.map_cons]
35/-- Private witness: the distinguished cusp used to cancel the total relation in the direct cusped
36quotient. -/
37private def firstCusp (σ : FenchelSignature) (hCusps : σ.HasCusps) : Fin σ.numCusps :=
38 ⟨0, hCusps⟩
40/-- The finite abelian target used in the cusped one-step quotient. -/
41abbrev CuspedSmoothQuotient (σ : FenchelSignature) :=
42 Multiplicative (FenchelPeriodCoordinate σ)
44instance instTopologicalSpaceCuspedSmoothQuotient (σ : FenchelSignature) :
45 TopologicalSpace (CuspedSmoothQuotient σ) :=
46 ⊥
48instance instDiscreteTopologyCuspedSmoothQuotient (σ : FenchelSignature) :
49 DiscreteTopology (CuspedSmoothQuotient σ) :=
50 ⟨rfl⟩
52noncomputable instance instFiniteULiftCuspedSmoothQuotient (σ : FenchelSignature) :
53 Finite (ULift.{u, 0} (CuspedSmoothQuotient σ)) := by
54 letI : Finite (FenchelPeriodCoordinate σ) :=
55 zmodCoordinateFamily_finite σ.periods
56 (fun i => lt_of_lt_of_le (by decide : 0 < 2) (σ.period_ge_two i))
57 infer_instance
59/-- Direct cusped quotient on profinite Fenchel generators.
61This replaces the previous detour through the general discrete cusped presentation. The cusped
63homomorphism is used downstream. -/
65 (σ : FenchelSignature) (hCusps : σ.HasCusps) :
66 ProfiniteFenchelGeneratorIndex.{u} σ → CuspedSmoothQuotient σ
67 | ULift.up (.surfaceA _) => 1
68 | ULift.up (.surfaceB _) => 1
69 | ULift.up (.cusp j) =>
71 Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ))
72 else
73 1
74 | ULift.up (.inertia k) =>
75 Multiplicative.ofAdd (fenchelPeriodBasisVector σ k)
77/-- The direct cusped quotient, universe-lifted to match `Δ.carrier`. -/
79 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
80 ProfiniteFenchelGeneratorIndex.{u} Δ.signature →
81 ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) :=
82 fun x => ULift.up (cuspedSmoothGeneratorImageCore Δ.signature hCusps x)
84private theorem cuspedSmooth_inertia_list_product
85 (σ : FenchelSignature) (hCusps : σ.HasCusps) :
86 (List.map
87 (fun k : Fin σ.numPeriods =>
88 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
89 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))
90 (List.finRange σ.numPeriods)).prod =
91 Multiplicative.ofAdd (fenchelPeriodBasisSum σ) := by
92 rw [show
93 (fun k : Fin σ.numPeriods =>
94 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
95 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
96 fun k : Fin σ.numPeriods =>
97 Multiplicative.ofAdd (fenchelPeriodBasisVector σ k) by
98 funext k
99 simp only [cuspedSmoothGeneratorImageCore]]
100 calc
101 (List.map
102 (fun k : Fin σ.numPeriods =>
103 Multiplicative.ofAdd (fenchelPeriodBasisVector σ k))
104 (List.finRange σ.numPeriods)).prod =
105 ∏ k : Fin σ.numPeriods,
106 Multiplicative.ofAdd (fenchelPeriodBasisVector σ k) := by
107 simpa using
108 (Fin.prod_univ_def
109 (f := fun k : Fin σ.numPeriods =>
110 Multiplicative.ofAdd (fenchelPeriodBasisVector σ k))).symm
111 _ = Multiplicative.ofAdd (fenchelPeriodBasisSum σ) := by
112 symm
113 exact ofAdd_sum
114 (s := Finset.univ)
115 (f := fun k : Fin σ.numPeriods => fenchelPeriodBasisVector σ k)
117private theorem cuspedSmooth_cusp_list_product
118 (σ : FenchelSignature) (hCusps : σ.HasCusps) :
119 (List.map
120 (fun j : Fin σ.numCusps =>
121 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
122 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
123 (List.finRange σ.numCusps)).prod =
124 Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ)) := by
125 classical
126 calc
127 (List.map
128 (fun j : Fin σ.numCusps =>
129 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
130 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
131 (List.finRange σ.numCusps)).prod =
132 ∏ j : Fin σ.numCusps,
133 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
134 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)) := by
135 simpa using
136 (Fin.prod_univ_def
137 (f := fun j : Fin σ.numCusps =>
138 cuspedSmoothGeneratorImageCore (σ := σ) hCusps
139 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))).symm
140 _ = Multiplicative.ofAdd (-(fenchelPeriodBasisSum σ)) := by
142 · simp only [cuspedSmoothGeneratorImageCore, ↓reduceIte, ofAdd_neg]
143 · intro j _hj hj
144 simp only [cuspedSmoothGeneratorImageCore, hj, ↓reduceIte]
145 · intro hnot
146 exact False.elim (hnot (Finset.mem_univ _))
148private theorem cuspedSmoothGeneratorImage_total_relation
149 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
151 (fun i => cuspedSmoothGeneratorImageCore Δ.signature hCusps
152 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceA i)))
153 (fun i => cuspedSmoothGeneratorImageCore Δ.signature hCusps
154 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceB i)))
155 (fun j => cuspedSmoothGeneratorImageCore Δ.signature hCusps
156 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
157 (fun k => cuspedSmoothGeneratorImageCore Δ.signature hCusps
158 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) = 1 := by
159 dsimp [profiniteFenchelTotalRelation]
161 simp only [cuspedSmoothGeneratorImageCore, commutatorElement_self, List.map_const', List.length_finRange,
162 List.prod_replicate, one_pow, ofAdd_neg, one_mul, inv_mul_cancel]
164private theorem cuspedSmoothGeneratorImage_lifted_total_relation
165 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
167 (fun i => cuspedSmoothGeneratorImage Δ hCusps
168 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceA i)))
169 (fun i => cuspedSmoothGeneratorImage Δ hCusps
170 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.surfaceB i)))
171 (fun j => cuspedSmoothGeneratorImage Δ hCusps
172 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.cusp j)))
173 (fun k => cuspedSmoothGeneratorImage Δ hCusps
174 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) = 1 := by
175 let e :
176 ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
177 CuspedSmoothQuotient Δ.signature :=
178 MulEquiv.ulift
179 apply e.injective
180 simp only [MulEquiv.ulift, profiniteFenchelTotalRelation, cuspedSmoothGeneratorImage, MulEquiv.coe_mk,
181 Equiv.ulift_apply, ULift.mul_down, ULift.one_down, e]
183 have h := cuspedSmoothGeneratorImage_total_relation Δ hCusps
184 dsimp [profiniteFenchelTotalRelation] at h
185 simpa [List.map_map, Function.comp_def, commutatorElement,
186 cuspedSmoothGeneratorImageCore] using h
188private theorem cuspedSmoothGeneratorImage_period_relation
189 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
190 (k : Fin Δ.signature.numPeriods) :
191 cuspedSmoothGeneratorImageCore Δ.signature hCusps
192 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)) ^
193 Δ.signature.periods k = 1 := by
194 change
195 Multiplicative.ofAdd (fenchelPeriodBasisVector Δ.signature k) ^
196 Δ.signature.periods k = 1
197 rw [← ofAdd_nsmul]
198 rw [show
199 Δ.signature.periods k • fenchelPeriodBasisVector Δ.signature k = 0 by
200 simpa [fenchelPeriodBasisVector] using
201 zmodBasisVector_nsmul_eq_zero Δ.signature.periods k]
202 rfl
204private theorem cuspedSmoothGeneratorImage_lifted_period_relation
205 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
206 (k : Fin Δ.signature.numPeriods) :
207 cuspedSmoothGeneratorImage Δ hCusps
208 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)) ^
209 Δ.signature.periods k = 1 := by
210 let e :
211 ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
212 CuspedSmoothQuotient Δ.signature :=
213 MulEquiv.ulift
214 apply e.injective
215 simp only [MulEquiv.ulift, cuspedSmoothGeneratorImage, MulEquiv.coe_mk, Equiv.ulift_apply, ULift.pow_down,
216 ULift.one_down, e]
217 exact cuspedSmoothGeneratorImage_period_relation Δ hCusps k
219private theorem cuspedSmoothGeneratorImage_inertia_order
220 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
221 (k : Fin Δ.signature.numPeriods) :
222 orderOf
223 (cuspedSmoothGeneratorImageCore Δ.signature hCusps
224 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
225 Δ.signature.periods k := by
226 rw [cuspedSmoothGeneratorImageCore, orderOf_ofAdd_eq_addOrderOf]
227 exact zmodBasisVector_addOrderOf Δ.signature.periods k
229private theorem cuspedSmoothGeneratorImage_lifted_inertia_order
230 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps)
231 (k : Fin Δ.signature.numPeriods) :
232 orderOf
233 (cuspedSmoothGeneratorImage Δ hCusps
234 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k))) =
235 Δ.signature.periods k := by
236 let e :
237 ULift.{u, 0} (CuspedSmoothQuotient Δ.signature) ≃*
238 CuspedSmoothQuotient Δ.signature :=
239 MulEquiv.ulift
240 have horder :=
241 orderOf_injective
242 e.toMonoidHom
243 e.injective
244 (cuspedSmoothGeneratorImage Δ hCusps
245 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))
246 have hcore :
247 orderOf
248 (e.toMonoidHom (cuspedSmoothGeneratorImage Δ hCusps
249 (ULift.up.{u, 0} (ProfiniteFenchelGenerator.inertia k)))) =
250 Δ.signature.periods k := by
251 exact cuspedSmoothGeneratorImage_inertia_order Δ hCusps k
252 exact horder.symm.trans hcore
254noncomputable def cuspedSmoothQuotientData
255 (Δ : ProfiniteFGroup.{u}) (hCusps : Δ.signature.HasCusps) :
256 ProfiniteSmoothQuotientData Δ 1 :=
257 ProfiniteSmoothQuotientData.ofPresentationLiftToFiniteOfRelations
258 Δ (cuspedSmoothGeneratorImage Δ hCusps)
262 (ULift.{u, 0} (CuspedSmoothQuotient Δ.signature)))
267end FenchelNielsen