English
For a fixed transversal T, the transfer homomorphism equals φ composed with the diff at g, i.e., transfer ϕ g = ϕ(diff ϕ T (g • T)).
Русский
Для фиксированной трансверсали T передача ϕ g равна композиции ϕ с diff: transfer ϕ g = ϕ(diff ϕ T (g • T)).
LaTeX
$$$\mathrm{transfer}(\varphi,g) = \varphi\bigl(\mathrm{diff}(\varphi,T,g\cdot T)\bigr)$$$
Lean4
/-- Explicit computation of the transfer homomorphism. -/
theorem transfer_eq_prod_quotient_orbitRel_zpowers_quot [FiniteIndex H] (g : G)
[Fintype (Quotient (orbitRel (zpowers g) (G ⧸ H)))] :
transfer ϕ g =
∏ q : Quotient (orbitRel (zpowers g) (G ⧸ H)),
ϕ
⟨q.out.out⁻¹ * g ^ Function.minimalPeriod (g • ·) q.out * q.out.out,
QuotientGroup.out_conj_pow_minimalPeriod_mem H g q.out⟩ :=
by
classical
letI := H.fintypeQuotientOfFiniteIndex
calc
transfer ϕ g = ∏ q : G ⧸ H, _ := transfer_def ϕ (transferTransversal H g) g
_ = _ := ((quotientEquivSigmaZMod H g).symm.prod_comp _).symm
_ = _ := (Finset.prod_sigma _ _ _)
_ = _ := by
refine Fintype.prod_congr _ _ (fun q => ?_)
simp only [quotientEquivSigmaZMod_symm_apply, transferTransversal_apply', transferTransversal_apply'']
rw [Fintype.prod_eq_single (0 : ZMod (Function.minimalPeriod (g • ·) q.out)) _]
· simp only [if_pos, ZMod.cast_zero, zpow_zero, one_mul, mul_assoc]
· intro k hk
simp only [if_neg hk, inv_mul_cancel]
exact map_one ϕ
