English
If a certain combinatorial equality holds at the level of transversals (involving a function key), then g^H.index ∈ H, i.e., the index-th power of g lies in H.
Русский
Если выполняется вспомогательная лемма о степени, тогда g^{|H|} принадлежит H.
LaTeX
$$$g^{|H|} \in H$ under the given key condition$$
Lean4
/-- Auxiliary lemma in order to state `transfer_eq_pow`. -/
theorem transfer_eq_pow_aux (g : G) (key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g₀⁻¹ * g ^ k * g₀ = g ^ k) :
g ^ H.index ∈ H := by
by_cases hH : H.index = 0
· rw [hH, pow_zero]
exact H.one_mem
letI := fintypeOfIndexNeZero hH
classical
replace key : ∀ (k : ℕ) (g₀ : G), g₀⁻¹ * g ^ k * g₀ ∈ H → g ^ k ∈ H := fun k g₀ hk =>
(congr_arg (· ∈ H) (key k g₀ hk)).mp hk
replace key : ∀ q : G ⧸ H, g ^ Function.minimalPeriod (g • ·) q ∈ H := fun q =>
key (Function.minimalPeriod (g • ·) q) q.out (QuotientGroup.out_conj_pow_minimalPeriod_mem H g q)
let f : Quotient (orbitRel (zpowers g) (G ⧸ H)) → zpowers g := fun q =>
(⟨g, mem_zpowers g⟩ : zpowers g) ^ Function.minimalPeriod (g • ·) q.out
have hf : ∀ q, f q ∈ H.subgroupOf (zpowers g) := fun q => key q.out
replace key := Subgroup.prod_mem (H.subgroupOf (zpowers g)) fun q (_ : q ∈ Finset.univ) => hf q
simpa only [f, minimalPeriod_eq_card, Finset.prod_pow_eq_pow_sum, Fintype.card_sigma,
Fintype.card_congr (selfEquivSigmaOrbits (zpowers g) (G ⧸ H)), index_eq_card, Nat.card_eq_fintype_card] using key
