English
The transferFunction is a function from the quotient G/H to G, defined by selecting, for each coset, a canonical representative built from a fixed transversal and the orbit structure.
Русский
Функция transferFunction есть отображение из фактор-группы G/H в G, задаваемое выбором фиксированной трансверсали и канонического представителя каждой косеты.
LaTeX
$$$\mathrm{transferFunction}: (G \!\middle|\! H) \to G$ with $\mathrm{transferFunction}(q) = g^{m(q)} \cdot g_0(q)$, where $q$ is a coset and $m(q), g_0(q)$ come from the canonical left quotient data.$$
Lean4
/-- The transfer transversal as a function. Given a `⟨g⟩`-orbit `q₀, g • q₀, ..., g ^ (m - 1) • q₀`
in `G ⧸ H`, an element `g ^ k • q₀` is mapped to `g ^ k • g₀` for a fixed choice of
representative `g₀` of `q₀`. -/
noncomputable def transferFunction : G ⧸ H → G := fun q =>
g ^ (cast (quotientEquivSigmaZMod H g q).2 : ℤ) * (quotientEquivSigmaZMod H g q).1.out.out
