FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/SourceMaps.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetMaps
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/SourceMaps.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
14Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
15-/
17open scoped BigOperators
19namespace FenchelNielsen
21noncomputable def oneHeadPeriodOneTargetTailBlockWord
22 {tailLen p : ℕ}
23 (m₂' : ℕ) (tail : Fin tailLen → ℕ)
24 (hp : 2 ≤ p) (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
25 (hTailLen : 0 < tailLen) :
26 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
27 Fin p → FreeGroup (FuchsianGenerator target) := by
28 classical
29 dsimp
30 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
31 intro k
32 exact
33 (List.ofFn (fun j : Fin tailLen =>
34 xWord target (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p (.inr (k, j))))).prod
36noncomputable def oneHeadPeriodOneSecondEdgeForwardWord
37 {tailLen p : ℕ}
38 (m₂' : ℕ) (tail : Fin tailLen → ℕ)
39 (hp : 2 ≤ p) (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
40 (hTailLen : 0 < tailLen) :
41 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
42 Fin p → FreeGroup (FuchsianGenerator target) := by
43 classical
44 dsimp
45 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
46 let block := oneHeadPeriodOneTargetTailBlockWord m₂' tail hp hm₂'ge htail hTailLen
47 intro k
48 if h0 : k.val = 0 then
49 exact block ⟨p - 1, by omega⟩
50 else
51 exact block ⟨k.val - 1, by omega⟩
53noncomputable def doublePeriodOneTargetTailBlockWord
54 {tailLen p : ℕ}
55 (tail : Fin tailLen → ℕ)
56 (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
57 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
58 Fin p → FreeGroup (FuchsianGenerator target) := by
59 classical
60 dsimp
61 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
62 intro k
63 exact
64 (List.ofFn (fun j : Fin tailLen =>
67noncomputable def doublePeriodOneSecondEdgeForwardWord
68 {tailLen p : ℕ}
69 (tail : Fin tailLen → ℕ)
70 (hp : 2 ≤ p) (htail : ∀ j, 2 ≤ tail j)
71 (hHigh : 3 ≤ p * tailLen) :
72 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
73 Fin p → FreeGroup (FuchsianGenerator target) := by
74 classical
75 dsimp
76 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
77 let block := doublePeriodOneTargetTailBlockWord tail htail hHigh
78 intro k
79 if h0 : k.val = 0 then
80 exact block ⟨p - 1, by omega⟩
81 else
82 exact block ⟨k.val - 1, by omega⟩
84noncomputable def oneHeadPeriodOneSchreierToTargetGeneratorImage
85 {tailLen p : ℕ}
86 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
87 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
88 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
89 (e :
90 OriginalFirstReductionIndex tailLen ≃
91 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
92 hTailLen).numPeriods) :
93 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
94 let source :=
95 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
96 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
97 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
98 let hT :=
100 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
101 ↥(schreierGeneratorSet hT) → FreeGroup (FuchsianGenerator target) := by
102 classical
103 dsimp
104 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
105 let source :=
106 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
107 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
108 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
109 let φ :=
111 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
112 let hT :=
114 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
115 let secondWord :=
116 oneHeadPeriodOneSecondEdgeForwardWord m₂' tail hp hm₂'ge htail hTailLen
117 intro z
118 if hFirst :
119 (z : φ.ker) =
121 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e then
122 exact 1
123 else if hSecond :
124 ∃ k : Fin p,
125 (z : φ.ker) =
127 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k then
128 exact secondWord (Classical.choose hSecond)
129 else if hTail :
130 ∃ j : Fin tailLen, ∃ k : Fin p,
131 (z : φ.ker) =
133 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k then
134 let j : Fin tailLen := Classical.choose hTail
135 let hk : ∃ k : Fin p,
136 (z : φ.ker) =
138 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k :=
139 Classical.choose_spec hTail
140 let k : Fin p := Classical.choose hk
141 exact
143 (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p (.inr (k, j))))⁻¹
144 else
145 exact 1
147noncomputable def oneHeadPeriodOneSchreierToTargetHom
148 {tailLen p : ℕ}
149 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
150 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
151 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
152 (e :
153 OriginalFirstReductionIndex tailLen ≃
154 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
155 hTailLen).numPeriods) :
156 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
157 let source :=
158 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
159 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
160 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
161 let hT :=
163 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
164 FreeGroup ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator target) :=
165 FreeGroup.lift
167 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)
169noncomputable def doublePeriodOneSchreierToTargetGeneratorImage
170 {tailLen p : ℕ}
171 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
172 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
173 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
174 (hHigh : 3 ≤ p * tailLen)
175 (e :
176 OriginalFirstReductionIndex tailLen ≃
177 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
178 hTailLen).numPeriods) :
179 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
180 let source :=
181 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
182 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
183 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
184 let hT :=
186 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
187 ↥(schreierGeneratorSet hT) → FreeGroup (FuchsianGenerator target) := by
188 classical
189 dsimp
190 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
191 let source :=
192 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
193 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
194 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
195 let φ :=
197 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
198 let hT :=
200 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
201 let secondWord :=
202 doublePeriodOneSecondEdgeForwardWord tail hp htail hHigh
203 intro z
204 if hFirst :
205 (z : φ.ker) =
207 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e then
208 exact 1
209 else if hSecond :
210 ∃ k : Fin p,
211 (z : φ.ker) =
213 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k then
214 exact secondWord (Classical.choose hSecond)
215 else if hTail :
216 ∃ j : Fin tailLen, ∃ k : Fin p,
217 (z : φ.ker) =
219 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k then
220 let j : Fin tailLen := Classical.choose hTail
221 let hk : ∃ k : Fin p,
222 (z : φ.ker) =
224 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k :=
225 Classical.choose_spec hTail
226 let k : Fin p := Classical.choose hk
228 else
229 exact 1
231noncomputable def doublePeriodOneSchreierToTargetHom
232 {tailLen p : ℕ}
233 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
234 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
235 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
236 (hHigh : 3 ≤ p * tailLen)
237 (e :
238 OriginalFirstReductionIndex tailLen ≃
239 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
240 hTailLen).numPeriods) :
241 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
242 let source :=
243 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
244 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
245 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
246 let hT :=
248 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
249 FreeGroup ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator target) :=
250 FreeGroup.lift
252 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)
254end FenchelNielsen