FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.Signatures
import
Imported by
- FenchelNielsenZomorrodian.Discrete
- FenchelNielsenZomorrodian.Discrete.CompactFuchsian
- FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction
- FenchelNielsenZomorrodian.Discrete.CompactFuchsian.FirstReduction.QuotientAndBasis
- FenchelNielsenZomorrodian.Discrete.CompactFuchsian.PeriodOne.TargetSignatures
- FenchelNielsenZomorrodian.Discrete.CompactFuchsian.SecondReduction.Signatures
noncomputable abbrev firstReductionSourceSignature
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 0 < m₁') (hm₂' : 0 < m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
FuchsianSignature :=
originalFirstReductionSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLenThe first-reduction source signature has the displayed periods, index set, and total relation.
theorem list_prod_ofFn_mul_blocks {α : Type*} [Monoid α] {p n : ℕ}
(f : Fin (p * n) → α) :
(List.ofFn f).prod =
(List.ofFn (fun k : Fin p =>
(List.ofFn (fun j : Fin n =>
f ⟨k.val * n + j.val, by
calc
k.val * n + j.val < (k.val + 1) * n := by
calc
k.val * n + j.val < k.val * n + n :=
Nat.add_lt_add_left j.isLt _
_ = (k.val + 1) * n := by rw [Nat.add_mul, one_mul]
_ ≤ p * n := Nat.mul_le_mul_right n (Nat.succ_le_of_lt k.isLt)⟩)).prod)).prodShow proof
by
rw [List.ofFn_mul]
rw [List.prod_flatten]
rw [List.map_ofFn]
congrProof. 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. 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. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. 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.
□def firstReductionCanonicalSourcePeriod
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (i : Fin (2 + tailLen)) : ℕ :=
if h0 : i.val = 0 then
p * m₁'
else if h1 : i.val = 1 then
p * m₂'
else
tail ⟨i.val - 2, by omega⟩
@[local simp]The period function of the first-reduction canonical source signature.
theorem firstReductionCanonicalSourcePeriod_zero
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
⟨0, by omega⟩ = p * m₁'The zero-index period of the first-reduction canonical source signature.
Show proof
by
simp only [firstReductionCanonicalSourcePeriod, ↓reduceDIte]
@[local simp]Proof. 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.
□theorem firstReductionCanonicalSourcePeriod_one
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) :
firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
⟨1, by omega⟩ = p * m₂'The first distinguished period of the first-reduction canonical source signature.
Show proof
by
simp only [firstReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]
@[local simp]Proof. 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.
□theorem firstReductionCanonicalSourcePeriod_tail
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (j : Fin tailLen) :
firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
⟨2 + j.val, by omega⟩ = tail jA tail period of the first-reduction canonical source signature.
Show proof
by
unfold firstReductionCanonicalSourcePeriod
have h0 : 2 + j.val ≠ 0 := by omega
have h1 : 2 + j.val ≠ 1 := by omega
simp only [Nat.add_eq_zero_iff, OfNat.ofNat_ne_zero, false_and, ↓reduceDIte, h1, add_tsub_cancel_left,
Fin.eta]Proof. 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.
□def firstReductionCanonicalSourceSignature
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
FuchsianSignature where
orbitGenus := 0
numCusps := 0
numPeriods := 2 + tailLen
periods := firstReductionCanonicalSourcePeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
period_ge_two := by
intro i
unfold firstReductionCanonicalSourcePeriod
by_cases h0 : i.val = 0
· rw [dif_pos h0]
exact le_trans hp (Nat.le_mul_of_pos_right p (lt_of_lt_of_le (by decide) hm₁'))
· by_cases h1 : i.val = 1
· rw [dif_neg h0, dif_pos h1]
exact le_trans hp (Nat.le_mul_of_pos_right p (lt_of_lt_of_le (by decide) hm₂'))
· rw [dif_neg h0, dif_neg h1]
exact htail ⟨i.val - 2, by omega⟩
numCusps_eq_zero := rfl
numPeriods_ge_three := by omegaThe first-reduction source signature has the displayed periods, index set, and total relation.
def firstReductionCanonicalSourceZeroIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
Fin
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨0, by simp only [firstReductionCanonicalSourceSignature, add_pos_iff, Nat.ofNat_pos, true_or]⟩def firstReductionCanonicalSourceOneIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
Fin
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨1, by simp only [firstReductionCanonicalSourceSignature]; omega⟩The first distinguished source index in the first-reduction canonical signature is the one-index constructor.
def firstReductionCanonicalSourceTailIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) (j : Fin tailLen) :
Fin
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨2 + j.val, by
simp only [firstReductionCanonicalSourceSignature, add_lt_add_iff_left, Fin.is_lt]⟩The tail source index in the first-reduction canonical signature is the corresponding tail-index constructor.
@[simp 900] theorem firstReductionCanonicalSourceSignature_period_zero
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalSourceZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
p * m₁'The first-reduction canonical source signature has the prescribed zero-index period.
Show proof
by
simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalSourceZeroIndex, Fin.mk_zero',
firstReductionCanonicalSourcePeriod, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceDIte]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□@[simp 900] theorem firstReductionCanonicalSourceSignature_period_one
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalSourceOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
p * m₂'The first-reduction canonical source signature has the prescribed first distinguished period.
Show proof
by
simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalSourceOneIndex,
firstReductionCanonicalSourcePeriod, one_ne_zero, ↓reduceDIte]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□@[simp 900] theorem firstReductionCanonicalSourceSignature_period_tail
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) (j : Fin tailLen) :
(firstReductionCanonicalSourceSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalSourceTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j) =
tail jThe first-reduction canonical source signature has the prescribed tail period.
Show proof
by
simp only [firstReductionCanonicalSourceSignature, firstReductionCanonicalSourceTailIndex,
firstReductionCanonicalSourcePeriod_tail]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□theorem firstReductionCanonicalSource_totalRelation_eq
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
let σThe first-reduction canonical source total relation equals the displayed product relation.
Show proof
firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
totalRelation σ =
xWord σ
(firstReductionCanonicalSourceZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord σ
(firstReductionCanonicalSourceOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun j : Fin tailLen =>
xWord σ
(firstReductionCanonicalSourceTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j))).prod := by
classical
let σ :=
firstReductionCanonicalSourceSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
change totalRelation σ =
xWord σ
(firstReductionCanonicalSourceZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord σ
(firstReductionCanonicalSourceOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun j : Fin tailLen =>
xWord σ
(firstReductionCanonicalSourceTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen j))).prod
rw [totalRelation]
simpa [σ, firstReductionCanonicalSourceSignature, firstReductionCanonicalSourceZeroIndex,
firstReductionCanonicalSourceOneIndex, firstReductionCanonicalSourceTailIndex,
List.ofFn_eq_map, List.prod_cons, mul_assoc] using
congrArg List.prod
(list_ofFn_two_add (fun i : Fin (2 + tailLen) => xWord σ i))Proof. Unfold the named Fenchel--Nielsen reduction, cyclic-Schreier word, or total-relation definition. The equality or membership follows by evaluating the relevant generator branch, simplifying the period or product formula, and using that normal closures are closed under products, inverses, and conjugation when a relator membership is involved.
□def firstReductionCanonicalTargetPeriod
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen)
(i : Fin (2 + p * tailLen)) : ℕ :=
if i.val = 0 then
m₁'
else if i.val = 1 then
m₂'
else
tail ⟨(i.val - 2) % tailLen, Nat.mod_lt _ hTailLen⟩
@[local simp]The period function of the first-reduction canonical target signature.
theorem firstReductionCanonicalTargetPeriod_zero
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen) :
firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
hTailLen ⟨0, by omega⟩ = m₁'The zero-index period of the first-reduction canonical target signature.
Show proof
by
simp only [firstReductionCanonicalTargetPeriod, ↓reduceIte]
@[local simp]Proof. 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.
□theorem firstReductionCanonicalTargetPeriod_one
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen) :
firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
hTailLen ⟨1, by omega⟩ = m₂'The first distinguished period of the first-reduction canonical target signature.
Show proof
by
simp only [firstReductionCanonicalTargetPeriod, one_ne_zero, ↓reduceIte]
@[local simp]Proof. 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.
□theorem firstReductionCanonicalTargetPeriod_tail
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ) (hTailLen : 0 < tailLen)
(k : Fin p) (j : Fin tailLen) :
firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail
hTailLen
⟨2 + k.val * tailLen + j.val, by
have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
calc
k.val * tailLen + j.val < k.val * tailLen + tailLen :=
Nat.add_lt_add_left j.isLt _
_ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
have hmain : k.val * tailLen + j.val < p * tailLen :=
lt_of_lt_of_le hblock hle
omega⟩ = tail jA tail period of the first-reduction canonical target signature.
Show proof
by
unfold firstReductionCanonicalTargetPeriod
have h0 : 2 + k.val * tailLen + j.val ≠ 0 := by omega
have h1 : 2 + k.val * tailLen + j.val ≠ 1 := by omega
rw [if_neg h0, if_neg h1]
have hsub :
2 + k.val * tailLen + j.val - 2 = k.val * tailLen + j.val := by
omega
have hmod : (2 + k.val * tailLen + j.val - 2) % tailLen = j.val := by
rw [hsub, Nat.mul_comm k.val tailLen, Nat.mul_add_mod_self_left,
Nat.mod_eq_of_lt j.isLt]
exact congrArg tail (Fin.ext hmod)Proof. 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.
□def firstReductionCanonicalTargetSignature
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
FuchsianSignature where
orbitGenus := 0
numCusps := 0
numPeriods := 2 + p * tailLen
periods :=
firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p) m₁' m₂' tail hTailLen
period_ge_two := by
intro i
unfold firstReductionCanonicalTargetPeriod
by_cases h0 : i.val = 0
· rw [if_pos h0]
exact hm₁'
· by_cases h1 : i.val = 1
· rw [if_neg h0, if_pos h1]
exact hm₂'
· rw [if_neg h0, if_neg h1]
exact htail ⟨(i.val - 2) % tailLen, Nat.mod_lt _ hTailLen⟩
numCusps_eq_zero := rfl
numPeriods_ge_three := by
have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
nlinarith [Nat.mul_pos hp_pos hTailLen]The first-reduction canonical target signature has the displayed periods, index set, and total relation.
def firstReductionCanonicalTargetZeroIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
Fin
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨0, by simp only [firstReductionCanonicalTargetSignature, add_pos_iff, Nat.ofNat_pos, CanonicallyOrderedAdd.mul_pos,
true_or]⟩def firstReductionCanonicalTargetOneIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
Fin
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨1, by
have hp_pos : 0 < p := lt_of_lt_of_le (by decide : 0 < 2) hp
have hprod : 0 < p * tailLen := Nat.mul_pos hp_pos hTailLen
simp only [firstReductionCanonicalTargetSignature, gt_iff_lt]
omega⟩The first distinguished target index in the first-reduction canonical signature is the one-index constructor.
def firstReductionCanonicalTargetFlatTailIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(r : Fin (p * tailLen)) :
Fin
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨2 + r.val, by
simp only [firstReductionCanonicalTargetSignature, add_lt_add_iff_left, Fin.is_lt]⟩
@[local simp]The flat-tail target index in the first-reduction canonical signature is the displayed block-tail index.
theorem firstReductionCanonicalTargetSignature_period_flatTail
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(r : Fin (p * tailLen)) :
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r) =
tail ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩The first-reduction canonical target signature has the prescribed flat-tail period.
Show proof
by
change
firstReductionCanonicalTargetPeriod (tailLen := tailLen) (p := p)
m₁' m₂' tail hTailLen ⟨2 + r.val, by simp only [add_lt_add_iff_left, Fin.is_lt]⟩ =
tail ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
unfold firstReductionCanonicalTargetPeriod
have h0 : 2 + r.val ≠ 0 := by omega
have h1 : 2 + r.val ≠ 1 := by omega
rw [if_neg h0, if_neg h1]
apply congrArg tail
ext
simp only [add_tsub_cancel_left]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□def firstReductionCanonicalTargetTailIndex
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(k : Fin p) (j : Fin tailLen) :
Fin
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods :=
⟨2 + k.val * tailLen + j.val, by
have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
calc
k.val * tailLen + j.val < k.val * tailLen + tailLen :=
Nat.add_lt_add_left j.isLt _
_ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
have hmain : k.val * tailLen + j.val < p * tailLen :=
lt_of_lt_of_le hblock hle
simp only [firstReductionCanonicalTargetSignature, gt_iff_lt]
omega⟩The tail target index in the first-reduction canonical signature is the corresponding tail-index constructor.
theorem firstReductionCanonicalTargetIndex_eq_tailIndex_of_ne_zero_one
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(i :
Fin
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).numPeriods)
(h0 : i.val ≠ 0) (h1 : i.val ≠ 1) :
let r : Fin (p * tailLen)Show proof
⟨i.val - 2, by
have hi : i.val < 2 + p * tailLen := by
simp only [firstReductionCanonicalTargetSignature] at i
exact i.isLt
omega⟩
let k : Fin p := ⟨r.val / tailLen, by
exact Nat.div_lt_of_lt_mul (by simpa [Nat.mul_comm] using r.isLt)⟩
let j : Fin tailLen := ⟨r.val % tailLen, Nat.mod_lt _ hTailLen⟩
i =
firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j := by
dsimp
ext
change i.val = 2 + (i.val - 2) / tailLen * tailLen + (i.val - 2) % tailLen
have hige2 : 2 ≤ i.val := by omega
have hdecomp :
(i.val - 2) / tailLen * tailLen + (i.val - 2) % tailLen = i.val - 2 :=
Nat.div_add_mod' (i.val - 2) tailLen
omegaProof. 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. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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.
□@[simp 900] theorem firstReductionCanonicalTargetFlatTailIndex_block
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(k : Fin p) (j : Fin tailLen) :
firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
⟨k.val * tailLen + j.val, by
have hblock : k.val * tailLen + j.val < (k.val + 1) * tailLen := by
calc
k.val * tailLen + j.val < k.val * tailLen + tailLen :=
Nat.add_lt_add_left j.isLt _
_ = (k.val + 1) * tailLen := by rw [Nat.add_mul, one_mul]
have hle : (k.val + 1) * tailLen ≤ p * tailLen :=
Nat.mul_le_mul_right tailLen (Nat.succ_le_of_lt k.isLt)
exact lt_of_lt_of_le hblock hle⟩ =
firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k jThe flat-tail target index in the first-reduction canonical signature is the displayed block-tail index.
Show proof
by
ext
simp only [firstReductionCanonicalTargetFlatTailIndex, firstReductionCanonicalTargetTailIndex]
omegaProof. 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. 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. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. 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.
□private theorem firstReductionCanonicalTarget_flatTailProduct_eq_blocks
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
let τThe first-reduction canonical flat-tail product equals the displayed product of blocks.
Show proof
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
(List.ofFn (fun r : Fin (p * tailLen) =>
xWord τ
(firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod =
(List.ofFn (fun k : Fin p =>
(List.ofFn (fun j : Fin tailLen =>
xWord τ
(firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod := by
classical
let τ :=
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
change
(List.ofFn (fun r : Fin (p * tailLen) =>
xWord τ
(firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod =
(List.ofFn (fun k : Fin p =>
(List.ofFn (fun j : Fin tailLen =>
xWord τ
(firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
rw [list_prod_ofFn_mul_blocks]
congr
funext k
congr
funext j
rw [firstReductionCanonicalTargetFlatTailIndex_block]Proof. 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. 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. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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. Every map between the reduced presentations is determined by the images of elliptic, handle, and boundary generators. The period and product relators are checked explicitly after applying those images. Therefore the constructed quotient or abelianized map is well defined and has the claimed effect on the named generator or class. 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.
□private theorem firstReductionCanonicalTarget_totalRelation_eq_flat
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
let τThe first-reduction canonical target total relation equals the displayed flattened product.
Show proof
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
totalRelation τ =
xWord τ
(firstReductionCanonicalTargetZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord τ
(firstReductionCanonicalTargetOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun r : Fin (p * tailLen) =>
xWord τ
(firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod := by
classical
let τ :=
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
change totalRelation τ =
xWord τ
(firstReductionCanonicalTargetZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord τ
(firstReductionCanonicalTargetOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun r : Fin (p * tailLen) =>
xWord τ
(firstReductionCanonicalTargetFlatTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen r))).prod
rw [totalRelation]
simpa [τ, firstReductionCanonicalTargetSignature, firstReductionCanonicalTargetZeroIndex,
firstReductionCanonicalTargetOneIndex, firstReductionCanonicalTargetFlatTailIndex,
List.ofFn_eq_map, List.prod_cons, mul_assoc] using
congrArg List.prod
(list_ofFn_two_add (fun i : Fin (2 + p * tailLen) => xWord τ i))Proof. 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. 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. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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.
□theorem firstReductionCanonicalTarget_totalRelation_eq_blocks
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
let τThe first-reduction canonical target total relation splits into the displayed block product.
Show proof
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
totalRelation τ =
xWord τ
(firstReductionCanonicalTargetZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord τ
(firstReductionCanonicalTargetOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun k : Fin p =>
(List.ofFn (fun j : Fin tailLen =>
xWord τ
(firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod := by
classical
let τ :=
firstReductionCanonicalTargetSignature m₁' m₂' tail hp hm₁' hm₂' htail hTailLen
change totalRelation τ =
xWord τ
(firstReductionCanonicalTargetZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
xWord τ
(firstReductionCanonicalTargetOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) *
(List.ofFn (fun k : Fin p =>
(List.ofFn (fun j : Fin tailLen =>
xWord τ
(firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j))).prod)).prod
rw [firstReductionCanonicalTarget_totalRelation_eq_flat]
rw [firstReductionCanonicalTarget_flatTailProduct_eq_blocks]Proof. 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. 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. Kernel and normal-closure claims are proved by showing that each rewritten relator lies in the generated normal subgroup and that the quotient map kills exactly those relations required by the presentation. Finiteness and cardinality estimates use the prescribed period data and the finite quotient of the presentation determined by those periods. 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.
□@[simp 900] theorem firstReductionCanonicalTargetSignature_period_zero
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalTargetZeroIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
m₁'The first-reduction canonical target signature has the prescribed zero-index period.
Show proof
by
simp only [firstReductionCanonicalTargetSignature, firstReductionCanonicalTargetZeroIndex, Fin.mk_zero',
firstReductionCanonicalTargetPeriod, Fin.coe_ofNat_eq_mod, Nat.zero_mod, ↓reduceIte]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□@[simp 900] theorem firstReductionCanonicalTargetSignature_period_one
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen) :
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalTargetOneIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen) =
m₂'The first-reduction canonical target signature has the prescribed first distinguished period.
Show proof
by
simp only [firstReductionCanonicalTargetSignature, firstReductionCanonicalTargetOneIndex,
firstReductionCanonicalTargetPeriod, one_ne_zero, ↓reduceIte]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□@[simp 900] theorem firstReductionCanonicalTargetSignature_period_tail
{tailLen p : ℕ}
(m₁' m₂' : ℕ) (tail : Fin tailLen → ℕ)
(hp : 2 ≤ p) (hm₁' : 2 ≤ m₁') (hm₂' : 2 ≤ m₂')
(htail : ∀ j, 2 ≤ tail j) (hTailLen : 0 < tailLen)
(k : Fin p) (j : Fin tailLen) :
(firstReductionCanonicalTargetSignature
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen).periods
(firstReductionCanonicalTargetTailIndex
m₁' m₂' tail hp hm₁' hm₂' htail hTailLen k j) =
tail jThe first-reduction canonical target signature has the prescribed tail period.
Show proof
by
simp only [firstReductionCanonicalTargetSignature, firstReductionCanonicalTargetTailIndex,
firstReductionCanonicalTargetPeriod_tail]Proof. Evaluate the period function of the first-reduction canonical source or target signature at the named index.
□