FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetSignatures

1 Theorem | 4 Definition | 1 Abbreviation

This module studies target signatures for fenchel nielsen zomorrodian. The target signature obtained by replicating the tail in the double-period-one case. The tail-replicated double-period-one target signature satisfies the LCM condition.

Open this file on GitHub

import

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures

Imported by

Definition FenchelNielsen.doublePeriodOneTailReplicatedSignature GitHub

noncomputable def doublePeriodOneTailReplicatedSignature
    {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
    (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
    FuchsianSignature where
  orbitGenus := 0
  numCusps := 0
  numPeriods := p * tailLen
  periods := fun i => tail ((finProdFinEquiv.symm i).2)
  period_ge_two := by
    intro i
    exact htail ((finProdFinEquiv.symm i).2)
  numCusps_eq_zero := rfl
  numPeriods_ge_three := hHigh

The target signature obtained by replicating the tail in the double-period-one case.

Theorem FenchelNielsen.doublePeriodOneTailReplicatedSignature_lcmCondition GitHub

theorem doublePeriodOneTailReplicatedSignature_lcmCondition
    {tailLen p : ℕ} (tail : Fin tailLen → ℕ)
    (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
    2 ≤ p →
    LCMCondition
      (doublePeriodOneTailReplicatedSignature tail htail hHigh).toFenchelSignature

The tail-replicated double-period-one target signature satisfies the LCM condition.

Show proof

Abbreviation FenchelNielsen.OneHeadPeriodOneTargetIndex GitHub

abbrev OneHeadPeriodOneTargetIndex (tailLen p : ℕ) :=
  Sum (Fin 1) (Fin p × Fin tailLen)

The index type used for the one-head period-one target signature.

Definition FenchelNielsen.oneHeadPeriodOneTargetOrderedIndexEquiv GitHub

def oneHeadPeriodOneTargetOrderedIndexEquiv (tailLen p : ℕ) :
    OneHeadPeriodOneTargetIndex tailLen p ≃ Fin (1 + p * tailLen) :=
  (Equiv.sumCongr (Equiv.refl (Fin 1))
      (finProdFinEquiv : Fin p × Fin tailLen ≃ Fin (p * tailLen))).trans
    finSumFinEquiv

The finite-index equivalence orders the period-one target indices.

Definition FenchelNielsen.oneHeadPeriodOneTargetPeriods GitHub

def oneHeadPeriodOneTargetPeriods
    {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ) :
    OneHeadPeriodOneTargetIndex tailLen p → ℕ
  | .inl _ => m₂'
  | .inr kj => tail kj.2

The period family of the one-head period-one target signature.

Definition FenchelNielsen.oneHeadPeriodOneTargetSignature GitHub

noncomputable def oneHeadPeriodOneTargetSignature
    {tailLen p : ℕ} (m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₂' : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
    (hTailLen : 0 < tailLen) : FuchsianSignature where
  orbitGenus := 0
  numCusps := 0
  numPeriods := 1 + p * tailLen
  periods := fun i =>
    oneHeadPeriodOneTargetPeriods (p := p) m₂' tail
      ((oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i)
  period_ge_two := by
    intro i
    cases h :
      (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i with
    | inl head =>
        fin_cases head
        exact hm₂'
    | inr kj =>
        exact htail kj.2
  numCusps_eq_zero := rfl
  numPeriods_ge_three := by
    have htailOne : 1 ≤ tailLen := Nat.succ_le_of_lt hTailLen
    have hprod : 2 ≤ p * tailLen := by
      exact Nat.mul_le_mul hp htailOne
    omega

The target signature in the one-head period-one case.

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetSignatures

Declarations