FenchelNielsenZomorrodian/Discrete/Core/FamilySignature.lean
1import FenchelNielsenZomorrodian.Discrete.Core.CompactFuchsianPresentation
3/-
4PUBLIC_PAGE_SNAPSHOT
5generated_at: 2026-05-27T09:47:29+09:00
6lean_source: lean4/FenchelNielsenZomorrodian/Discrete/Core/FamilySignature.lean
7translation_root: data/translation
8purpose: identifies the local data snapshot used to build pages/
9placement: after imports, never before imports
10-/
11/-!
12# Discrete Fenchel and compact Fuchsian core definitions
14Signatures, generator indices, presentations, elliptic generators, quotient homomorphisms, and family-signature transformations.
15-/
17namespace FenchelNielsen
19noncomputable def familyFuchsianSignature
20 {ι : Type*} [Fintype ι]
21 (periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
22 (hcard : 3 ≤ Fintype.card ι) :
23 FuchsianSignature where
24 orbitGenus := 0
25 numCusps := 0
26 numPeriods := Fintype.card ι
27 periods := fun i => periods ((Fintype.equivFin ι).symm i)
28 period_ge_two := by
29 intro i
30 simpa using hperiods ((Fintype.equivFin ι).symm i)
31 numCusps_eq_zero := rfl
32 numPeriods_ge_three := hcard
34@[simp] theorem familyFuchsianSignature_periods
35 {ι : Type*} [Fintype ι]
36 (periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
37 (hcard : 3 ≤ Fintype.card ι) (i : ι) :
38 (familyFuchsianSignature periods hperiods hcard).periods
39 (Fintype.equivFin ι i) = periods i := by
40 simp only [familyFuchsianSignature, Equiv.symm_apply_apply]
43 {ι : Type*} [Fintype ι] [DecidableEq ι]
44 (periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
45 (hcard : 3 ≤ Fintype.card ι)
46 (hLCM : LCMConditionFamily periods) :
47 LCMCondition (familyFuchsianSignature periods hperiods hcard).toFenchelSignature := by
48 classical
49 let e : Fin (Fintype.card ι) ≃ ι := (Fintype.equivFin ι).symm
50 change LCMConditionFamily (familyFuchsianSignature periods hperiods hcard).periods
51 intro i
52 have hi : periods (e i) ∣ otherPeriodsLcmFamily periods (e i) := hLCM (e i)
53 have hOtherDiv :
54 otherPeriodsLcmFamily periods (e i) ∣
56 (familyFuchsianSignature periods hperiods hcard).periods i := by
57 rw [otherPeriodsLcmFamily]
58 apply Finset.lcm_dvd
59 intro j hj
60 let j' : Fin (Fintype.card ι) := e.symm j
61 have hjNe : j ≠ e i := (Finset.mem_erase.mp hj).1
62 have hj'Mem :
63 j' ∈ (Finset.univ.erase i : Finset (Fin (Fintype.card ι))) := by
64 refine Finset.mem_erase.mpr ⟨?_, Finset.mem_univ j'⟩
65 intro hji
66 apply hjNe
67 have h := congrArg e hji
68 simpa [j', e] using h
69 have hdiv :=
70 Finset.dvd_lcm
71 (s := Finset.univ.erase i)
72 (f := (familyFuchsianSignature periods hperiods hcard).periods)
73 hj'Mem
74 simpa [familyFuchsianSignature, j', e] using hdiv
75 simpa [familyFuchsianSignature, e] using hi.trans hOtherDiv
77end FenchelNielsen