English
Under the same finite-index hypothesis, transfer ϕ g equals ϕ of the paired power element with a proof that its power lies in H.
Русский
При той же конечной по индексу гипотезе передача ϕ g равна ϕ от соответствующего элемента-степени с доказательством того, что эта степень лежит в H.
LaTeX
$$$\mathrm{transfer}(\varphi,g) = \varphi\langle g^{|H|}, \text{proof}\rangle$$$
Lean4
theorem transfer_eq_pow [FiniteIndex H] (g : G)
(key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) :
transfer ϕ g = ϕ ⟨g ^ H.index, transfer_eq_pow_aux g key⟩ := by
classical
letI := H.fintypeQuotientOfFiniteIndex
change ∀ (k g₀) (hk : g₀⁻¹ * g ^ k * g₀ ∈ H), ↑(⟨g₀⁻¹ * g ^ k * g₀, hk⟩ : H) = g ^ k at key
rw [transfer_eq_prod_quotient_orbitRel_zpowers_quot, ← Finset.prod_map_toList, ← Function.comp_def ϕ,
List.prod_map_hom]
refine congrArg ϕ (Subtype.coe_injective ?_)
dsimp only
rw [H.coe_mk, ← (zpowers g).coe_mk g (mem_zpowers g), ← (zpowers g).coe_pow, index_eq_card, Nat.card_eq_fintype_card,
Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), Fintype.card_sigma, ← Finset.prod_pow_eq_pow_sum, ←
Finset.prod_map_toList]
simp only [Subgroup.val_list_prod, List.map_map, ← minimalPeriod_eq_card]
congr 2
funext
apply key
