FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/TargetMaps.lean
1import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.QuotientAndBasis
2import FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetSignatures
4/-
5PUBLIC_PAGE_SNAPSHOT
6generated_at: 2026-05-27T09:47:29+09:00
7lean_source: lean4/FenchelNielsenZomorrodian/Discrete/CompactFuchsian/PeriodOne/TargetMaps.lean
8translation_root: data/translation
9purpose: identifies the local data snapshot used to build pages/
10placement: after imports, never before imports
11-/
12/-!
15Handles the cleanup of period-one target entries using quotient maps, kernel equivalences, low-cardinality dihedral cases, source subgroups, and relator proofs.
16-/
18open scoped BigOperators
20namespace FenchelNielsen
22noncomputable def oneHeadPeriodOneTargetToSchreierGeneratorImage
23 {tailLen p : ℕ}
24 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
25 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
26 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
27 (e :
28 OriginalFirstReductionIndex tailLen ≃
29 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
30 hTailLen).numPeriods) :
31 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
32 let source :=
33 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
34 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
35 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
36 let hT :=
38 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
39 FuchsianGenerator target → FreeGroup ↥(schreierGeneratorSet hT) := by
40 classical
41 dsimp
42 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
43 let source :=
44 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
45 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
46 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
47 let hT :=
49 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
50 let basis :=
52 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
53 intro g
54 cases g with
55 | elliptic i =>
56 exact
57 match (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i with
58 | .inl _ =>
59 basis.symm
61 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e)
62 | .inr jk =>
63 basis.symm
65 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e jk.2 jk.1)
66 | surfaceA _ => exact 1
67 | surfaceB _ => exact 1
69noncomputable def oneHeadPeriodOneTargetToSchreierHom
70 {tailLen p : ℕ}
71 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
72 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
73 (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
74 (e :
75 OriginalFirstReductionIndex tailLen ≃
76 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
77 hTailLen).numPeriods) :
78 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
79 let source :=
80 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
81 let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
82 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
83 let hT :=
85 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
86 FreeGroup (FuchsianGenerator target) →* FreeGroup ↥(schreierGeneratorSet hT) :=
87 FreeGroup.lift
89 m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)
91noncomputable def doublePeriodOneTargetToSchreierGeneratorImage
92 {tailLen p : ℕ}
93 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
94 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
95 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
96 (hHigh : 3 ≤ p * tailLen)
97 (e :
98 OriginalFirstReductionIndex tailLen ≃
99 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
100 hTailLen).numPeriods) :
101 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
102 let source :=
103 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
104 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
105 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
106 let hT :=
108 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
109 FuchsianGenerator target → FreeGroup ↥(schreierGeneratorSet hT) := by
110 classical
111 dsimp
112 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
113 let source :=
114 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
115 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
116 let hT :=
118 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
119 let basis :=
121 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
122 intro g
123 cases g with
124 | elliptic i =>
125 let jk : Fin p × Fin tailLen :=
126 finProdFinEquiv.symm i
127 exact basis.symm
129 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e jk.2 jk.1)
130 | surfaceA _ => exact 1
131 | surfaceB _ => exact 1
133noncomputable def doublePeriodOneTargetToSchreierHom
134 {tailLen p : ℕ}
135 (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
136 (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
137 (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
138 (hHigh : 3 ≤ p * tailLen)
139 (e :
140 OriginalFirstReductionIndex tailLen ≃
141 Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
142 hTailLen).numPeriods) :
143 letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
144 let source :=
145 originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
146 let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
147 letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
148 let hT :=
150 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
151 FreeGroup (FuchsianGenerator target) →* FreeGroup ↥(schreierGeneratorSet hT) :=
152 FreeGroup.lift
154 m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)
156end FenchelNielsen