FenchelNielsenZomorrodian.Discrete.Singerman.KernelTransport
This module develops the rewriting and basis constructions behind the subgroup calculations. It tracks words and relations through the chosen transversal to obtain the required presentation or basis statements.
def singermanTransportPeriodsFamily
{ι : Type*} {ρ : ι → ℕ}
(n : ∀ i : ι, Fin (ρ i) → ℕ) :
(Σ i : ι, Fin (ρ i)) → ℕ
| ⟨i, k⟩ => n i kThe Singerman transport periods family is the finite family of periods, products, or least common multiple data used in the period reduction in the Fenchel--Nielsen--Zomorrodian presentation.