FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceMaps

8 Definition

This module studies source maps for fenchel nielsen zomorrodian. The tail-block word used for the one-head period-one target source map. The second-edge forward word used for the one-head period-one source map.

Open this file on GitHub

import

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetMaps

Imported by

Definition FenchelNielsen.oneHeadPeriodOneTargetTailBlockWord GitHub

noncomputable def oneHeadPeriodOneTargetTailBlockWord
    {tailLen p : ℕ}
    (m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
    (hTailLen : 0 < tailLen) :
    let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
    Fin p → FreeGroup (FuchsianGenerator target) := by
  classical
  dsimp
  let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
  intro k
  exact
    (List.ofFn (fun j : Fin tailLen =>
      xWord target (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p (.inr (k, j))))).prod

The tail-block word used for the one-head period-one target source map.

Definition FenchelNielsen.oneHeadPeriodOneSecondEdgeForwardWord GitHub

noncomputable def oneHeadPeriodOneSecondEdgeForwardWord
    {tailLen p : ℕ}
    (m₂' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hm₂'ge : 2 ≤ m₂') (htail : ∀ j, 2 ≤ tail j)
    (hTailLen : 0 < tailLen) :
    let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
    Fin p → FreeGroup (FuchsianGenerator target) := by
  classical
  dsimp
  let target := oneHeadPeriodOneTargetSignature m₂' tail hp hm₂'ge htail hTailLen
  let block := oneHeadPeriodOneTargetTailBlockWord m₂' tail hp hm₂'ge htail hTailLen
  intro k
  if h0 : k.val = 0 then
    exact block ⟨p - 1, by omega⟩
  else
    exact block ⟨k.val - 1, by omega⟩

The second-edge forward word used for the one-head period-one source map.

Definition FenchelNielsen.doublePeriodOneTargetTailBlockWord GitHub

noncomputable def doublePeriodOneTargetTailBlockWord
    {tailLen p : ℕ}
    (tail : Fin tailLen → ℕ)
    (htail : ∀ j, 2 ≤ tail j) (hHigh : 3 ≤ p * tailLen) :
    let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
    Fin p → FreeGroup (FuchsianGenerator target) := by
  classical
  dsimp
  let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
  intro k
  exact
    (List.ofFn (fun j : Fin tailLen =>
      xWord target (finProdFinEquiv (k, j)))).prod

The tail-block word used for the double-period-one target source map.

Definition FenchelNielsen.doublePeriodOneSecondEdgeForwardWord GitHub

noncomputable def doublePeriodOneSecondEdgeForwardWord
    {tailLen p : ℕ}
    (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (htail : ∀ j, 2 ≤ tail j)
    (hHigh : 3 ≤ p * tailLen) :
    let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
    Fin p → FreeGroup (FuchsianGenerator target) := by
  classical
  dsimp
  let target := doublePeriodOneTailReplicatedSignature tail htail hHigh
  let block := doublePeriodOneTargetTailBlockWord tail htail hHigh
  intro k
  if h0 : k.val = 0 then
    exact block ⟨p - 1, by omega⟩
  else
    exact block ⟨k.val - 1, by omega⟩

The second-edge forward word used for the double-period-one source map.

Definition FenchelNielsen.oneHeadPeriodOneSchreierToTargetGeneratorImage GitHub

noncomputable def oneHeadPeriodOneSchreierToTargetGeneratorImage
    {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
    ↥(schreierGeneratorSet hT) → FreeGroup (FuchsianGenerator target) := 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 φ :=
    originalFirstReductionPeriodOneFreeQuotientHom
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let hT :=
    originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let secondWord :=
    oneHeadPeriodOneSecondEdgeForwardWord m₂' tail hp hm₂'ge htail hTailLen
  intro z
  if hFirst :
      (z : φ.ker) =
        originalFirstReductionPeriodOneFirstPowerKernel
          m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e then
    exact 1
  else if hSecond :
      ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneSecondEdgeKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k then
    exact secondWord (Classical.choose hSecond)
  else if hTail :
      ∃ j : Fin tailLen, ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneTailKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k then
    let j : Fin tailLen := Classical.choose hTail
    let hk : ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneTailKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k :=
      Classical.choose_spec hTail
    let k : Fin p := Classical.choose hk
    exact
      (xWord target
        (oneHeadPeriodOneTargetOrderedIndexEquiv tailLen p (.inr (k, j))))⁻¹
  else
    exact 1

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

Definition FenchelNielsen.oneHeadPeriodOneSchreierToTargetHom GitHub

noncomputable def oneHeadPeriodOneSchreierToTargetHom
    {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 ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator target) :=
  FreeGroup.lift
    (oneHeadPeriodOneSchreierToTargetGeneratorImage
      m₁' m₂' tail hp hm₁' hm₂' hm₂'ge htail hTailLen e)

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

Definition FenchelNielsen.doublePeriodOneSchreierToTargetGeneratorImage GitHub

noncomputable def doublePeriodOneSchreierToTargetGeneratorImage
    {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
    ↥(schreierGeneratorSet hT) → FreeGroup (FuchsianGenerator target) := 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 := doublePeriodOneTailReplicatedSignature tail htail hHigh
  letI : DecidableEq (FuchsianGenerator source) := Classical.decEq _
  let φ :=
    originalFirstReductionPeriodOneFreeQuotientHom
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let hT :=
    originalFirstReductionPeriodOneSchreierTransversal_isRightSchreierTransversal
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e
  let secondWord :=
    doublePeriodOneSecondEdgeForwardWord tail hp htail hHigh
  intro z
  if hFirst :
      (z : φ.ker) =
        originalFirstReductionPeriodOneFirstPowerKernel
          m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e then
    exact 1
  else if hSecond :
      ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneSecondEdgeKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e k then
    exact secondWord (Classical.choose hSecond)
  else if hTail :
      ∃ j : Fin tailLen, ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneTailKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k then
    let j : Fin tailLen := Classical.choose hTail
    let hk : ∃ k : Fin p,
        (z : φ.ker) =
          originalFirstReductionPeriodOneTailKernelElement
            m₁' m₂' tail hp hm₁' hm₂' htail hTailLen e j k :=
      Classical.choose_spec hTail
    let k : Fin p := Classical.choose hk
    exact (xWord target (finProdFinEquiv (k, j)))⁻¹
  else
    exact 1

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

Definition FenchelNielsen.doublePeriodOneSchreierToTargetHom GitHub

noncomputable def doublePeriodOneSchreierToTargetHom
    {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 ↥(schreierGeneratorSet hT) →* FreeGroup (FuchsianGenerator target) :=
  FreeGroup.lift
    (doublePeriodOneSchreierToTargetGeneratorImage
      m₁' m₂' tail hp hm₁' hm₂' htail hTailLen hHigh e)

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

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.SourceMaps

Declarations