English
A companion auxiliary lemma asserts the existence of an integer i for a negative power scenario, ensuring the same kind of reachability as in Lemma1 but with negative indices.
Русский
Сопутствующая вспомогательная лемма утверждает существование целого числа i для случая с отрицательным степенным индексом, обеспечивая достижимость как в Лемме 1, но с отрицательными индексами.
LaTeX
$$$ \\exists i : \\mathbb{Z}, ((\\text{swap } x (f x) \\cdot f)^i)(f x) = b $$$
Lean4
theorem isCycle_swap_mul_aux₂ {α : Type*} [DecidableEq α] :
∀ (n : ℤ) {b x : α} {f : Perm α} (_ : (swap x (f x) * f) b ≠ b) (_ : (f ^ n) (f x) = b),
∃ i : ℤ, ((swap x (f x) * f) ^ i) (f x) = b :=
by
intro n
cases n with
| ofNat n => exact isCycle_swap_mul_aux₁ n
| negSucc n =>
intro b x f hb h
exact
if hfbx' : f x = b then ⟨0, hfbx'⟩
else
have : f b ≠ b ∧ b ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hb
have hb : (swap x (f⁻¹ x) * f⁻¹) (f⁻¹ b) ≠ f⁻¹ b :=
by
rw [mul_apply, swap_apply_def]
split_ifs <;> simp only [inv_eq_iff_eq, Perm.mul_apply, zpow_negSucc, Ne, Perm.apply_inv_self] at * <;> tauto
let ⟨i, hi⟩ :=
isCycle_swap_mul_aux₁ n hb
(show (f⁻¹ ^ n) (f⁻¹ x) = f⁻¹ b by
rw [← zpow_natCast, ← h, ← mul_apply, ← mul_apply, ← mul_apply, zpow_negSucc, ← inv_pow, pow_succ,
mul_assoc, mul_assoc, inv_mul_cancel, mul_one, zpow_natCast, ← pow_succ', ← pow_succ])
have h : (swap x (f⁻¹ x) * f⁻¹) (f x) = f⁻¹ x := by rw [mul_apply, inv_apply_self, swap_apply_left]
⟨-i, by
rw [← add_sub_cancel_right i 1, neg_sub, sub_eq_add_neg, zpow_add, zpow_one, zpow_neg, ← inv_zpow,
mul_inv_rev, swap_inv, mul_swap_eq_swap_mul, inv_apply_self, swap_comm _ x, zpow_add, zpow_one, mul_apply,
mul_apply (_ ^ i), h, hi, mul_apply, apply_inv_self, swap_apply_of_ne_of_ne this.2 (Ne.symm hfbx')]⟩
