FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodFamilies
This module studies period families for fenchel nielsen zomorrodian. The two-entry period family has the prescribed periods. The zero-index value of the two-entry period family.
def twoPeriods {α : Type*} (a b : α) : Fin 2 → α :=
Fin.cases a (fun _ => b)The two-entry period family has the prescribed periods.
@[simp 900] theorem twoPeriods_zero {α : Type*} (a b : α) :
twoPeriods a b 0 = aThe zero-index value of the two-entry period family.
Show proof
rflProof. Unfold the relevant period-family or signature definition and split on the finite index cases. Each branch reduces to the stored period entry or to the specified reindexing or transport map, so the displayed period value follows directly.
□@[simp 900] theorem twoPeriods_one {α : Type*} (a b : α) :
twoPeriods a b 1 = bThe one-index value of the two-entry period family.
Show proof
rflProof. Unfold the relevant period-family or signature definition and split on the finite index cases. Each branch reduces to the stored period entry or to the specified reindexing or transport map, so the displayed period value follows directly.
□@[simp 900] theorem fin_cases_const_one {α : Type*} (a b : α) :
Fin.cases a (fun _ : Fin 1 => b) 1 = bShow proof
rflProof. 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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
□abbrev OriginalFirstReductionIndex (tailLen : ℕ) := Sum (Fin 2) (Fin tailLen)The index type for the original first-reduction period family.
def originalFirstReductionPeriods {tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
OriginalFirstReductionIndex tailLen → ℕ
| .inl i => twoPeriods (p * m₁') (p * m₂') i
| .inr j => tail jThe original period family transported for the first reduction.
abbrev FirstReductionIndex (tailLen p : ℕ) := Sum (Fin 2) (Fin tailLen × Fin p)Index type used for the first reduction of period families.
def firstReductionPeriods {tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
FirstReductionIndex tailLen p → ℕ
| .inl i => twoPeriods m₁' m₂' i
| .inr jk => tail jk.1The period family used in the first reduction.
abbrev FirstSecondInputIndex (tailLen p : ℕ) := Sum (Fin 2) (Sum (Fin p) (Fin tailLen × Fin p))Index type combining the first and second period-family inputs.
abbrev SecondReductionSourceIndex (tailLen p : ℕ) :=
Sum (Fin 2) (Sum (Fin 2) (Sum (Fin (p - 2)) (Fin tailLen × Fin p)))The index type for the source periods in the second reduction.
def secondReductionSourcePeriods {tailLen p q : ℕ}
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
SecondReductionSourceIndex tailLen p → ℕ
| .inl i => twoPeriods m₁' m₂' i
| .inr (.inl _) => q * m₃'
| .inr (.inr (.inl _)) => q * m₃'
| .inr (.inr (.inr jk)) => tail jk.1The source period family used in the second reduction.
def secondReductionSourceCycleCount {tailLen p q : ℕ} :
SecondReductionSourceIndex tailLen p → ℕ
| .inl _ => q
| .inr (.inl _) => 1
| .inr (.inr (.inl _)) => q
| .inr (.inr (.inr _)) => qThe source cycle count for the second reduction is the expected period-family cycle length.
def secondReductionSourceTransportPeriods {tailLen p q : ℕ}
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
∀ i : SecondReductionSourceIndex tailLen p,
Fin (secondReductionSourceCycleCount (q := q) i) → ℕ
| .inl i, _ => twoPeriods m₁' m₂' i
| .inr (.inl _), _ => m₃'
| .inr (.inr (.inl _)), _ => q * m₃'
| .inr (.inr (.inr jk)), _ => tail jk.1The transported source period family used in the second reduction.
abbrev SecondReductionTransportIndex (tailLen p q : ℕ) :=
Σ i : SecondReductionSourceIndex tailLen p,
Fin (secondReductionSourceCycleCount (tailLen := tailLen) (p := p) (q := q) i)The index type for transported periods in the second reduction.
abbrev secondReductionTransportPeriods {tailLen p q : ℕ}
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
SecondReductionTransportIndex tailLen p q → ℕ :=
singermanTransportPeriodsFamily
(secondReductionSourceTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)The transported period family used in the second reduction.
theorem secondReductionTransport_hasEqualPartnerFamily
{tailLen p q : ℕ} (hq : 2 ≤ q)
(m₁' m₂' m₃' : ℕ) (tail : Fin tailLen → ℕ) :
HasEqualPartnerFamily (secondReductionTransportPeriods (p := p) (q := q) m₁' m₂' m₃' tail)The transported second-reduction period family has the required equal-partner pairing.
Show proof
by
intro x
rcases x with ⟨i, k⟩
cases i with
| inl i =>
refine ⟨⟨.inl i, finPartner hq k⟩, ?_, ?_⟩
· intro h
have hk : finPartner hq k = k := by
simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
exact finPartner_ne hq k hk
· rfl
| inr s =>
cases s with
| inl j =>
refine ⟨⟨.inr (.inl (finPartner (by decide : 2 ≤ 2) j)),
by simpa [secondReductionSourceCycleCount] using (0 : Fin 1)⟩, ?_, ?_⟩
· intro h
have hj : finPartner (by decide : 2 ≤ 2) j = j := by
simpa using (Sigma.mk.inj_iff.mp h).1
exact finPartner_ne (by decide : 2 ≤ 2) j hj
· rfl
| inr s =>
cases s with
| inl j =>
refine ⟨⟨.inr (.inr (.inl j)), finPartner hq k⟩, ?_, ?_⟩
· intro h
have hk : finPartner hq k = k := by
simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
exact finPartner_ne hq k hk
· rfl
| inr jk =>
refine ⟨⟨.inr (.inr (.inr jk)), finPartner hq k⟩, ?_, ?_⟩
· intro h
have hk : finPartner hq k = k := by
simpa using eq_of_heq (Sigma.mk.inj_iff.mp h).2
exact finPartner_ne hq k hk
· rflProof. 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. 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. The topological assertion is checked by the initial topology of the inverse limit. After composing with each finite-stage projection, the relevant map is a continuous finite-stage homomorphism or an operation on a finite product; compactness, Hausdorffness, total disconnectedness, and profiniteness are then inherited from the finite stages by the standard inverse-limit argument. 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.
□