FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore

32 Theorem | 3 Definition | 1 Abbreviation

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

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.Target

Imported by

Definition FenchelNielsen.secondReductionCanonicalSecondEdgeForwardWord GitHub

noncomputable def secondReductionCanonicalSecondEdgeForwardWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    let τ :=
      secondReductionTransportSignature (p := p) hq
        m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
    Fin q → FreeGroup (FuchsianGenerator τ) := by
  classical
  dsimp
  let τ :=
    secondReductionTransportSignature (p := p) hq
      m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail
  let A :=
    secondReductionCanonicalTransportTargetWord (p := p) (q := q)
      m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
      (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩)
  let block :=
    secondReductionCanonicalTransportZeroBlockWord (p := p) (q := q)
      m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
  intro k
  if h0 : k.val = 0 then
    exact block ⟨q - 1, by omega⟩ * A
  else
    exact block ⟨k.val - 1, by omega⟩

The second-reduction second-edge forward word associated with an index.

Definition FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchGeneratorImage GitHub

noncomputable def secondReductionCanonicalSchreierToTransportSecondBranchGeneratorImage
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
    let σ :=
      secondReductionCanonicalSourceSignature
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
    let hT :=
      secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    ↥(schreierGeneratorSet hT) →
      FreeGroup (FuchsianGenerator
        (secondReductionTransportSignature (p := p) hq
          m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)) := by
  classical
  dsimp
  letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
  let σ :=
    secondReductionCanonicalSourceSignature
      m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
  let φ :=
    secondReductionCanonicalSourceFreeQuotientHom
      m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
  let A : FreeGroup (FuchsianGenerator
      (secondReductionTransportSignature (p := p) hq
        m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)) :=
    secondReductionCanonicalTransportTargetWord (p := p) (q := q)
      m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
      (secondReductionCanonicalTransportDistinguishedIndex tailLen p q ⟨0, by decide⟩)
  let secondWord :=
    secondReductionCanonicalSecondEdgeForwardWord (p := p) (q := q)
      m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
  let targetWord :=
    secondReductionCanonicalTransportTargetWord (p := p) (q := q)
      m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
  intro z
  if hFirst :
      (z : φ.ker) =
        secondReductionCanonicalFirstPowerKernel
          m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail then
    exact A⁻¹
  else if hSecond :
      ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalSecondEdgeKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k then
    exact secondWord (Classical.choose hSecond)
  else if hHeadZero :
      ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalHeadZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k then
    let k : Fin q := Classical.choose hHeadZero
    exact
      (targetWord
        (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨0, by decide⟩ k))⁻¹
  else if hHeadOne :
      ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalHeadOneKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail k then
    let k : Fin q := Classical.choose hHeadOne
    exact
      (targetWord
        (secondReductionCanonicalTransportHeadIndex tailLen p q ⟨1, by decide⟩ k))⁻¹
  else if hMiddleRest :
      ∃ r : Fin (p - 2), ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalMiddleRestZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k then
    let r : Fin (p - 2) := Classical.choose hMiddleRest
    let hk : ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalMiddleRestZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail r k :=
      Classical.choose_spec hMiddleRest
    let k : Fin q := Classical.choose hk
    exact
      (targetWord
        (secondReductionCanonicalTransportMiddleRestIndex tailLen p q r k))⁻¹
  else if hTail :
      ∃ b : Fin p, ∃ j : Fin tailLen, ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalTailZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k then
    let b : Fin p := Classical.choose hTail
    let hj : ∃ j : Fin tailLen, ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalTailZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k :=
      Classical.choose_spec hTail
    let j : Fin tailLen := Classical.choose hj
    let hk : ∃ k : Fin q,
        (z : φ.ker) =
          secondReductionCanonicalTailZeroKernelElement
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail b j k :=
      Classical.choose_spec hj
    let k : Fin q := Classical.choose hk
    exact
      (targetWord
        (secondReductionCanonicalTransportTailIndex tailLen p q b j k))⁻¹
  else
    exact 1

The second-reduction Schreier word or generator is evaluated by the chosen transversal and equals the prescribed target word.

Definition FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom GitHub

noncomputable def secondReductionCanonicalSchreierToTransportSecondBranchHom
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
    let σ :=
      secondReductionCanonicalSourceSignature
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
    let hT :=
      secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    FreeGroup ↥(schreierGeneratorSet hT) →*
      FreeGroup (FuchsianGenerator
        (secondReductionTransportSignature (p := p) hq
          m₁' m₂' m₃' tail hm₁' hm₂' hm₃' htail)) :=
  FreeGroup.lift
    (secondReductionCanonicalSchreierToTransportSecondBranchGeneratorImage
      m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)

The homomorphism from the second-reduction canonical Schreier presentation to the transported second-branch presentation.

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_firstPowerWord GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_firstPowerWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the first-power word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_headZeroWord GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_headZeroWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the head-zero word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_headOneWord GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_headOneWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the head-one word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_middleRestWord GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_middleRestWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (r : Fin (p - 2)) (k : Fin q) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the middle-rest word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_tailWord GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_tailWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (b : Fin p) (j : Fin tailLen) (k : Fin q) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the tail word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_headZero GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_headZero
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) :
    letI : NeZero q

The inverse transport map sends the head-zero generator to its prescribed preimage.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_headOne GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_headOne
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) :
    letI : NeZero q

The inverse transport map sends the head-one generator to its prescribed preimage.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_middleRest GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_middleRest
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (r : Fin (p - 2)) (k : Fin q) :
    letI : NeZero q

The inverse transport map sends each middle-rest generator to its prescribed preimage.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_tail GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_tail
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (b : Fin p) (j : Fin tailLen) (k : Fin q) :
    letI : NeZero q

The inverse transport map sends each tail generator to its prescribed preimage.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_positiveDistinguished GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_positiveDistinguished
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The inverse transport map sends the positive distinguished generator to its prescribed preimage.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_headZero_toInv_eq GitHub

private theorem secondReductionCanonicalSecondBranch_headZero_toInv_eq
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
    letI : NeZero q

The inverse map on the second-reduction head-zero branch has the prescribed value.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_headOne_toInv_eq GitHub

private theorem secondReductionCanonicalSecondBranch_headOne_toInv_eq
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
    letI : NeZero q

The inverse map on the second-reduction head-one branch has the prescribed value.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_middleRest_toInv_eq GitHub

private theorem secondReductionCanonicalSecondBranch_middleRest_toInv_eq
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) (r : Fin (p - 2)) (k : Fin q) :
    letI : NeZero q

The inverse map on the second-reduction middle-rest branch has the prescribed value.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_tail_toInv_eq GitHub

private theorem secondReductionCanonicalSecondBranch_tail_toInv_eq
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) (b : Fin p) (j : Fin tailLen) (k : Fin q) :
    letI : NeZero q

The inverse map on the second-reduction tail branch has the prescribed value.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_zeroImage_toInv_mem_normalClosure GitHub

theorem secondReductionCanonicalSecondBranch_zeroImage_toInv_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_secondEdgeWord GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_secondEdgeWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the second-edge word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranchHom_secondPowerWord GitHub

private theorem secondReductionCanonicalSchreierToTransportSecondBranchHom_secondPowerWord
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The Schreier-to-target transport homomorphism sends the second-power word to the prescribed target word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondEdgeForwardWord_zero GitHub

private theorem secondReductionCanonicalSecondEdgeForwardWord_zero
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    let τ

At index zero, the second-reduction second-edge forward word has the stated form.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondEdgeForwardWord_of_ne_zero GitHub

private theorem secondReductionCanonicalSecondEdgeForwardWord_of_ne_zero
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) (h0 : k.val ≠ 0) :
    secondReductionCanonicalSecondEdgeForwardWord (p := p) (q := q)
        m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail k =
      secondReductionCanonicalTransportZeroBlockWord (p := p) (q := q)
        m₁' m₂' m₃' tail hq hm₁' hm₂' hm₃' htail
        ⟨k.val - 1, by omega⟩

For a nonzero index, the second-reduction second-edge forward word has the stated form.

Show proof

Abbreviation FenchelNielsen.secondReductionCanonicalSchreierRelatorSet GitHub

noncomputable abbrev secondReductionCanonicalSchreierRelatorSet
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q := ⟨Nat.ne_of_gt (lt_of_lt_of_le (by decide : 0 < 2) hq)⟩
    let σ :=
      secondReductionCanonicalSourceSignature
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    letI : DecidableEq (FuchsianGenerator σ) := Classical.decEq _
    let hT :=
      secondReductionCanonicalSchreierTransversal_isRightSchreierTransversal
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    Set (FreeGroup ↥(schreierGeneratorSet hT)) :=
  by
    classical
    let σ :=
      secondReductionCanonicalSourceSignature
        m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail
    exact
      ReidemeisterSchreier.Discrete.Presentations.freeGroupPullbackRelatorSet
        (secondReductionCanonicalSchreierBasisEquiv
          m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail)
        (ReidemeisterSchreier.Discrete.Presentations.freeKernelTransversalRelatorSet
          (f := ellipticQuotientGeneratorImage σ
            (secondReductionCanonicalSourceQuotientImage
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))
          (rels := relators σ)
          (secondReductionCanonicalSchreierTransversal
            m₁' m₂' m₃' tail hp hq hm₁' hm₂' hm₃' htail))

The Schreier relator set for the canonical second-reduction kernel presentation.

Theorem FenchelNielsen.secondReductionCanonicalTransportToSchreierHom_zeroBlock GitHub

private theorem secondReductionCanonicalTransportToSchreierHom_zeroBlock
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) (k : Fin q) :
    letI : NeZero q

The target-to-Schreier transport homomorphism sends the zero block to its prescribed Schreier word.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreier_rotatedBlockTotalProduct_mem_normalClosure GitHub

private theorem secondReductionCanonicalSchreier_rotatedBlockTotalProduct_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalTransportToSchreier_blockTotalWord_mem_normalClosure GitHub

private theorem secondReductionCanonicalTransportToSchreier_blockTotalWord_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalTransportToSchreier_mapsBlockRelators GitHub

theorem secondReductionCanonicalTransportToSchreier_mapsBlockRelators
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The transport-to-Schreier map sends the block relators to the corresponding Schreier relators.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreier_nonwrapSecondEdgeElimination_mem_normalClosure GitHub

private theorem secondReductionCanonicalSchreier_nonwrapSecondEdgeElimination_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin q) (h0 : k.val ≠ 0) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreier_wrapSecondEdgeElimination_mem_normalClosure GitHub

private theorem secondReductionCanonicalSchreier_wrapSecondEdgeElimination_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondBranch_secondEdge_toInv_mem_normalClosure GitHub

theorem secondReductionCanonicalSecondBranch_secondEdge_toInv_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_nonwrapTotalRelator_image_eq_one GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranch_nonwrapTotalRelator_image_eq_one
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j)
    (k : Fin (q - 1)) :
    letI : NeZero q

The second-reduction Schreier-to-transport map sends the nonwrapped total relator for the second branch to the identity.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_wrapTotalRelator_image_eq_one GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranch_wrapTotalRelator_image_eq_one
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The second-reduction Schreier-to-transport map sends the wrapped total relator for the second branch to the identity.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSecondEdgeForward_descendingProduct_eq_targetZeroBlocks_inv GitHub

private theorem secondReductionCanonicalSecondEdgeForward_descendingProduct_eq_targetZeroBlocks_inv
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    let τ

The descending product of second-reduction second-edge forward words equals the inverse of the target zero blocks.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalTransportBlockRelators_inverseRotated_mem_normalClosure GitHub

private theorem secondReductionCanonicalTransportBlockRelators_inverseRotated_mem_normalClosure
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    let τ

The named second-reduction relator follows from the source presentation relators and therefore lies in their normal closure.

Show proof

Theorem FenchelNielsen.secondReductionToTransportSecondBranch_toInv_negDist_mem_blockRelators GitHub

theorem secondReductionToTransportSecondBranch_toInv_negDist_mem_blockRelators
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The negative distinguished inverse image in the second-branch transport case lies in the block relator normal closure.

Show proof

Theorem FenchelNielsen.secondReductionCanonicalSchreierToTransportSecondBranch_toInv_mem_blockRelators GitHub

theorem secondReductionCanonicalSchreierToTransportSecondBranch_toInv_mem_blockRelators
    {tailLen p q : ℕ}
    (m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ)
    (hp : 2 ≤ p) (hq : 2 ≤ q)
    (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂') (hm₃' : 2 ≤ m₃')
    (htail : ∀ j, 2 ≤ tail j) :
    letI : NeZero q

The inverse image of a canonical Schreier generator in the second-branch transport case lies in the block relator normal closure.

Show proof

FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Relators.SourceCore

Declarations