FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/KernelEquivalence.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.ActualTransport
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.RelatorProofs
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/FirstReduction/KernelEquivalence.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15The first explicit finite quotient reduction for compact zero-genus Fuchsian presentations, including quotient maps, basis transport, signatures, and relator verification.
16-/
18namespace FenchelNielsen
20 (tailLen : ℕ) :
21 OriginalFirstReductionIndex tailLen ≃ Fin (2 + tailLen) :=
22 (Equiv.sumCongr (Equiv.refl (Fin 2)) (Equiv.refl (Fin tailLen))).trans
23 finSumFinEquiv
25 {tailLen p : ℕ}
26 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
27 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
28 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
29 Nonempty
31 (firstReductionSourceSignature m₁' m₂' tail hp
32 (lt_of_lt_of_le (by decide : 0 < 2) hm₁')
33 (lt_of_lt_of_le (by decide : 0 < 2) hm₂') htail hTailLen)
34 ≃*
37 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) := by
38 classical
39 refine
41 (firstReductionSourceSignature m₁' m₂' tail hp
42 (lt_of_lt_of_le (by decide : 0 < 2) hm₁')
43 (lt_of_lt_of_le (by decide : 0 < 2) hm₂') htail hTailLen)
45 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
46 ?_ ?_
47 (originalFirstReductionOrderedIndexEquiv tailLen)
48 (originalFirstReductionIndexEquivCanonicalSourceFin tailLen) ?_
49 · simp only [firstReductionSourceSignature, originalFirstReductionSignature]
50 · simp only [firstReductionCanonicalSourceSignature]
51 · intro x
52 cases x using Sum.casesOn <;> rename_i x
53 · fin_cases x
54 · calc
55 (firstReductionSourceSignature m₁' m₂' tail hp
56 (lt_of_lt_of_le (by decide : 0 < 2) hm₁')
57 (lt_of_lt_of_le (by decide : 0 < 2) hm₂') htail hTailLen).periods
58 (originalFirstReductionOrderedIndexEquiv tailLen (.inl (0 : Fin 2))) =
59 p * m₁' := by
61 simp only [originalFirstReductionSignature, originalFirstReductionSignaturePeriod, Fin.coe_ofNat_eq_mod,
62 Nat.zero_mod, ↓reduceDIte]
63 _ =
65 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
66 (originalFirstReductionIndexEquivCanonicalSourceFin tailLen (.inl (0 : Fin 2))) := by
67 simpa [firstReductionCanonicalSourceZeroIndex] using
69 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).symm
70 · calc
71 (firstReductionSourceSignature m₁' m₂' tail hp
72 (lt_of_lt_of_le (by decide : 0 < 2) hm₁')
73 (lt_of_lt_of_le (by decide : 0 < 2) hm₂') htail hTailLen).periods
74 (originalFirstReductionOrderedIndexEquiv tailLen (.inl (1 : Fin 2))) =
75 p * m₂' := by
77 have hOneFin : (1 : Fin (2 + tailLen)) = ⟨1, by omega⟩ := by
78 apply Fin.ext
79 simp only [Fin.coe_ofNat_eq_mod]
80 rw [Nat.mod_eq_of_lt (by omega : 1 < 2 + tailLen)]
81 rw [hOneFin]
82 simp only [originalFirstReductionSignature, originalFirstReductionSignaturePeriod, one_ne_zero, ↓reduceDIte]
83 _ =
85 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
86 (originalFirstReductionIndexEquivCanonicalSourceFin tailLen (.inl (1 : Fin 2))) := by
87 simpa [firstReductionCanonicalSourceOneIndex] using
89 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).symm
90 · calc
91 (firstReductionSourceSignature m₁' m₂' tail hp
92 (lt_of_lt_of_le (by decide : 0 < 2) hm₁')
93 (lt_of_lt_of_le (by decide : 0 < 2) hm₂') htail hTailLen).periods
94 (originalFirstReductionOrderedIndexEquiv tailLen (.inr x)) =
95 tail x := by
97 simp only [originalFirstReductionSignature, originalFirstReductionSignaturePeriod, Nat.add_eq_zero_iff,
98 OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, add_tsub_cancel_left, Fin.eta, dite_eq_ite, ite_eq_right_iff]
99 omega
100 _ =
102 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
103 (originalFirstReductionIndexEquivCanonicalSourceFin tailLen (.inr x)) := by
104 simpa [firstReductionCanonicalSourceTailIndex] using
106 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen x).symm
107noncomputable def firstReductionCanonicalSourceQuotientHom
108 {tailLen p : ℕ}
109 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
110 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
111 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
114 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) →*
115 Multiplicative (ZMod p) := by
116 classical
117 let σ :=
118 firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
119 let ξ :=
121 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
122 exact ellipticQuotientHom σ ξ
124 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
126 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
127noncomputable def firstReductionCanonicalSourceKernelEquiv_targetSignature
128 {tailLen p : ℕ}
129 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
130 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
131 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
136 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) := by
137 simpa [firstReductionCanonicalSourceQuotientHom] using
139 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
141 (tailLen p : ℕ) :
142 FirstReductionIndex tailLen p ≃ Fin (2 + p * tailLen) :=
143 (Equiv.sumCongr (Equiv.refl (Fin 2))
144 ((Equiv.prodComm (Fin tailLen) (Fin p)).trans finProdFinEquiv)).trans
145 finSumFinEquiv
147 {tailLen p : ℕ}
148 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
149 (hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
150 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
151 Nonempty
154 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
155 ≃*
158 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)) := by
159 classical
160 refine
163 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
165 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen)
166 ?_ ?_
167 (firstReductionIndexEquivCanonicalTargetFin tailLen p)
168 (Fintype.equivFin (FirstReductionIndex tailLen p)) ?_
169 · simp only [firstReductionCanonicalTargetSignature]
170 · simp only [firstReductionTransportSignature, familyFuchsianSignature]
171 · intro x
172 cases x using Sum.casesOn <;> rename_i x
173 · fin_cases x
174 · calc
176 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
177 (firstReductionIndexEquivCanonicalTargetFin tailLen p (.inl (0 : Fin 2))) =
178 m₁' := by
182 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
183 _ =
185 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
186 ((Fintype.equivFin (FirstReductionIndex tailLen p)) (.inl (0 : Fin 2))) := by
187 simp only [firstReductionTransportSignature, Fin.isValue, familyFuchsianSignature_periods,
188 firstReductionPeriods, twoPeriods, Nat.reduceAdd, Fin.cases_zero]
189 · calc
191 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
192 (firstReductionIndexEquivCanonicalTargetFin tailLen p (.inl (1 : Fin 2))) =
193 m₂' := by
197 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
198 _ =
200 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
201 ((Fintype.equivFin (FirstReductionIndex tailLen p)) (.inl (1 : Fin 2))) := by
202 simp only [firstReductionTransportSignature, Fin.isValue, familyFuchsianSignature_periods,
203 firstReductionPeriods, twoPeriods, Nat.reduceAdd, fin_cases_const_one]
204 · rcases x with ⟨j, k⟩
205 calc
207 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
208 (firstReductionIndexEquivCanonicalTargetFin tailLen p (.inr (j, k))) =
209 tail j := by
211 firstReductionIndexEquivCanonicalTargetFin, finProdFinEquiv,
212 Nat.add_assoc, Nat.add_comm, Nat.mul_comm] using
214 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j
215 _ =
217 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
218 ((Fintype.equivFin (FirstReductionIndex tailLen p)) (.inr (j, k))) := by
219 simp only [firstReductionTransportSignature, familyFuchsianSignature_periods, firstReductionPeriods]
220private theorem firstReductionCanonicalTargetSignature_mulEquiv_secondReductionSourceSignature_exists
221 {tailLen p q : ℕ}
222 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
223 (hp : 2 ≤ p) (hq : 2 ≤ q)
224 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 0 < m₃')
225 (htail : ∀ j, 2 ≤ tail j) :
226 Nonempty
229 (firstReductionTailIncludingThird (q := q) m₃' tail)
230 hp hm₁' hm₂'
231 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
232 (Nat.succ_pos _))
233 ≃*
235 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
236 hm₃' htail)) := by
238 m₁' m₂' (firstReductionTailIncludingThird (q := q) m₃' tail)
239 hp hm₁' hm₂' (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
240 (Nat.succ_pos _) with ⟨e₁⟩
242 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail with ⟨e₂⟩
243 exact ⟨e₁.trans e₂⟩
244noncomputable def firstReductionCanonicalKernelEquiv_secondReductionSourceSignature
245 {tailLen p q : ℕ}
246 (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
247 (hp : 2 ≤ p) (hq : 2 ≤ q)
248 (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 0 < m₃')
249 (htail : ∀ j, 2 ≤ tail j) :
251 (firstReductionTailIncludingThird (q := q) m₃' tail)
252 hp hm₁' hm₂'
253 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
256 (secondReductionSourceSignature (p := p) m₁' m₂' m₃' tail hq hm₁' hm₂'
257 hm₃' htail) :=
259 m₁' m₂' (firstReductionTailIncludingThird (q := q) m₃' tail)
260 hp hm₁' hm₂'
261 (firstReductionTailIncludingThird_ge_two_of_pos hq m₃' tail hm₃' htail)
262 (Nat.succ_pos _)).trans
263 (Classical.choice
265 m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))