FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetMaps

4 Definition

This module develops the maps induced by continuous homomorphisms. It organizes the relevant quotient pullbacks and finite-stage maps, then proves the compatibility statements needed for the completed construction.

Open this file on GitHub

import

Imported by

Definition FenchelNielsen.oneHeadPeriodOneTargetToSchreierGeneratorImage GitHub

noncomputable def oneHeadPeriodOneTargetToSchreierGeneratorImage
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
    (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
    (e :
      OriginalFirstReductionIndex tailLen ≃
        Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
          hTailLen).numPeriods) :
    letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
    let source :=
      originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
    let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
    letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
    let hT :=
      originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
    FuchsianGenerator target → FreeGroup ↥(schreierGeneratorSet hT) := by
  classical
  dsimp
  letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
  let source :=
    originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
  let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
  letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
  let hT :=
    originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let basis :=
    originalFirstReductionPeriodOneSchreierBasisEquiv
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  intro g
  cases g with
  | elliptic i =>
      exact
        match (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p).symm i with
        | .inl _ =>
            basis.symm
              (originalFirstReductionPeriodOneSecondPowerKernel
                m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e)
        | .inr jk =>
            basis.symm
              (originalFirstReductionPeriodOneTailKernelElement
                m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e jk.2 jk.1)
  | surfaceA _ => exact 1
  | surfaceB _ => exact 1

Generator images for the map from the one-head period-one target presentation to the Schreier presentation.

Definition FenchelNielsen.oneHeadPeriodOneTargetToSchreierHom GitHub

noncomputable def oneHeadPeriodOneTargetToSchreierHom
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
    (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
    (e :
      OriginalFirstReductionIndex tailLen ≃
        Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
          hTailLen).numPeriods) :
    letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
    let source :=
      originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
    let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
    letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
    let hT :=
      originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
    FreeGroup (FuchsianGenerator target) →* FreeGroup ↥(schreierGeneratorSet hT) :=
  FreeGroup.lift
    (oneHeadPeriodOneTargetToSchreierGeneratorImage
      m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)

The homomorphism from the one-head period-one target presentation back to the Schreier presentation.

Definition FenchelNielsen.doublePeriodOneTargetToSchreierGeneratorImage GitHub

noncomputable def doublePeriodOneTargetToSchreierGeneratorImage
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
    (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
    (hHigh : 3 ≤ p * tailLen)
    (e :
      OriginalFirstReductionIndex tailLen ≃
        Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
          hTailLen).numPeriods) :
    letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
    let source :=
      originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
    let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
    letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
    let hT :=
      originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
    FuchsianGenerator target → FreeGroup ↥(schreierGeneratorSet hT) := by
  classical
  dsimp
  letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
  let source :=
    originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
  letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
  let hT :=
    originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let basis :=
    originalFirstReductionPeriodOneSchreierBasisEquiv
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  intro g
  cases g with
  | elliptic i =>
      let jk : Fin p × Fin tailLen :=
        finProdFinEquiv.symm i
      exact basis.symm
        (originalFirstReductionPeriodOneTailKernelElement
          m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e jk.2 jk.1)
  | surfaceA _ => exact 1
  | surfaceB _ => exact 1

Generator images for the map from the double period-one target presentation to the Schreier presentation.

Definition FenchelNielsen.doublePeriodOneTargetToSchreierHom GitHub

noncomputable def doublePeriodOneTargetToSchreierHom
    {tailLen p : ℕ}
    (m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
    (htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
    (hHigh : 3 ≤ p * tailLen)
    (e :
      OriginalFirstReductionIndex tailLen ≃
        Fin (originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail
          hTailLen).numPeriods) :
    letI : NeZero p := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hp)⟩
    let source :=
      originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
    let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
    letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
    let hT :=
      originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
    FreeGroup (FuchsianGenerator target) →* FreeGroup ↥(schreierGeneratorSet hT) :=
  FreeGroup.lift
    (doublePeriodOneTargetToSchreierGeneratorImage
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)

The homomorphism from the double-period-one target presentation back to the Schreier presentation.

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetMaps

Declarations