English
A refined version of the previous identities holds in the orbitRel quotient by zpowers, distinguishing cases when the exponent is zero or nonzero.
Русский
Уточнённое тождество в фактор-группе по zpowers различает нулевой и ненулевой случаи степени экспоненты.
LaTeX
$$$\uparrow\Bigl((g\cdot \mathrm{transferTransversal}(H,g)).2.leftQuotientEquiv (g^{\! (cast k : \mathbb{Z})} \cdot q.out)\Bigr) = \begin{cases} g^{\text{minimalPeriod}(g\cdot \cdot) q.out} \cdot q.out, & k=0 \\ g^{\! (cast k : \mathbb{Z})} \cdot q.out, & k\neq 0 \end{cases}$$$
Lean4
theorem transferTransversal_apply' (q : orbitRel.Quotient (zpowers g) (G ⧸ H))
(k : ZMod (minimalPeriod (g • ·) q.out)) :
↑((transferTransversal H g).2.leftQuotientEquiv (g ^ (cast k : ℤ) • q.out)) = g ^ (cast k : ℤ) * q.out.out := by
rw [transferTransversal_apply, transferFunction_apply, ← quotientEquivSigmaZMod_symm_apply, apply_symm_apply]
