FenchelNielsenZomorrodian.Discrete.Core.FamilySignature
This module studies family signature for fenchel nielsen zomorrodian. The Fuchsian signature assembled from a family of period data. The period function of the family Fuchsian signature.
noncomputable def familyFuchsianSignature
{ι : Type*} [Fintype ι]
(periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
(hcard : 3 ≤ Fintype.card ι) :
FuchsianSignature where
orbitGenus := 0
numCusps := 0
numPeriods := Fintype.card ι
periods := fun i => periods ((Fintype.equivFin ι).symm i)
period_ge_two := by
intro i
simpa using hperiods ((Fintype.equivFin ι).symm i)
numCusps_eq_zero := rfl
numPeriods_ge_three := hcardThe Fuchsian signature assembled from a family of period data.
@[simp] theorem familyFuchsianSignature_periods
{ι : Type*} [Fintype ι]
(periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
(hcard : 3 ≤ Fintype.card ι) (i : ι) :
(familyFuchsianSignature periods hperiods hcard).periods
(Fintype.equivFin ι i) = periods iThe period function of the family Fuchsian signature.
Show proof
by
simp only [familyFuchsianSignature, Equiv.symm_apply_apply]Proof. Unfold the family Fuchsian signature and evaluate its period function at the chosen family index.
□theorem familyFuchsianSignature_lcmCondition_of_lcmConditionFamily
{ι : Type*} [Fintype ι] [DecidableEq ι]
(periods : ι → ℕ) (hperiods : ∀ i, 2 ≤ periods i)
(hcard : 3 ≤ Fintype.card ι)
(hLCM : LCMConditionFamily periods) :
LCMCondition (familyFuchsianSignature periods hperiods hcard).toFenchelSignatureThe family signature inherits the LCM condition from the period-family LCM hypotheses.
Show proof
by
classical
let e : Fin (Fintype.card ι) ≃ ι := (Fintype.equivFin ι).symm
change LCMConditionFamily (familyFuchsianSignature periods hperiods hcard).periods
intro i
have hi : periods (e i) ∣ otherPeriodsLcmFamily periods (e i) := hLCM (e i)
have hOtherDiv :
otherPeriodsLcmFamily periods (e i) ∣
otherPeriodsLcmFamily
(familyFuchsianSignature periods hperiods hcard).periods i := by
rw [otherPeriodsLcmFamily]
apply Finset.lcm_dvd
intro j hj
let j' : Fin (Fintype.card ι) := e.symm j
have hjNe : j ≠ e i := (Finset.mem_erase.mp hj).1
have hj'Mem :
j' ∈ (Finset.univ.erase i : Finset (Fin (Fintype.card ι))) := by
refine Finset.mem_erase.mpr ⟨?_, Finset.mem_univ j'⟩
intro hji
apply hjNe
have h := congrArg e hji
simpa [j', e] using h
have hdiv :=
Finset.dvd_lcm
(s := Finset.univ.erase i)
(f := (familyFuchsianSignature periods hperiods hcard).periods)
hj'Mem
simpa [familyFuchsianSignature, j', e] using hdiv
simpa [familyFuchsianSignature, e] using hi.trans hOtherDivProof. Use the Fenchel--Nielsen--Zomorrodian presentation with elliptic generators of prescribed periods, handle and boundary generators, and the defining product relation. The proof checks the images of the named generators and verifies that every presentation relator is preserved in the target quotient, abelianization, or reduced presentation. For period-class statements, the relevant lcm or gcd divisibility is converted into a scalar multiple of the abelianized elliptic generator, and the defining period relation makes that multiple vanish. Schreier-rewriting steps are performed with the chosen transversal; the letter-by-letter formula sends each relator to the corresponding canonical word in the subgroup presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. Because the generator images satisfy all defining relations and agree with the displayed quotient data, the presentation universal property yields the asserted identity. The reductions preserve the ordering of the canonical generators and the period data, so the image of every relator can be read directly in the target presentation. In the abelianized arguments, commutators vanish and only the period coefficients remain. The divisibility or lcm calculation then gives the required scalar multiple, while the presentation relation supplies its vanishing. For quotient and subgroup claims, representatives are chosen in the ambient group and the induced map is checked to send the class of an element to the class of its image. Normality, openness, and membership in the finite quotient class are preserved by the subgroup, quotient, intersection, or inverse-image closure property being invoked. For the Fenchel--Nielsen--Zomorrodian relations, the period calculation checks that each elliptic generator has image of the prescribed order, and the product relation is verified by multiplying the images in the stated order. Divisibility, lcm, or gcd hypotheses are used precisely to make the period relators vanish in the target quotient.
□