Finite sets repeat

Stream: Is there code for X?

[Wrenna Robson]

import Mathlib

namespace Equiv.Perm
lemma blahj (s : Finset α) (π : Equiv.Perm α) (x : α) (hsx : ∀ x, x ∈ s ↔ π x ∈ s)
  (hx : x ∈ s) :
    ∃ k, (k > 0 ∧ k ≤ s.card ∧ (π^k) x = x) := sorry
end Equiv.Perm

Do we have this (or something equivalent) anywhere? Basically the idea is - if I know that x is in s, where my permutation stays within s for s a finset, then in fact I can bound the order of x by the cardinality of x.

[Yakov Pechersky]

You can argue that s is a subset of the support (if necessary, support limited to the subtype s). There should be a lemma that relates cardinality of the support to the order

[Wrenna Robson]

It's pretty difficult to express stuff about the order actually.

[Wrenna Robson]

When you're not dealing with a fintype.

[Yakov Pechersky]

You have Fintype (s : Set alpha) however

[Wrenna Robson]

docs#cycleOf

[Wrenna Robson]

Oh, that is true...

[Wrenna Robson]

It's a pain because I don't really want to talk about the global order - or even the order on the fintype - but specifically the order of the cycle on the fintype. It's very indirect.

[Yakov Pechersky]

What I'm saying is that for a fintype, the order is less that the card of the type. You can use that in your lemma by discussing a perm that is constrained over the type s. Where definitionally, s.card will the fintype card.

[Wrenna Robson]

Right because it's a cycle

[Wrenna Robson]

Or rather the cycle of is

[Wrenna Robson]

[Wrenna Robson]

theorem SameCycle.exists_pow_eq_of_mem_support' [Fintype α] [DecidableEq α]
    (f : Perm α) (h : SameCycle f x y)
  (hx : x ∈ f.support) : ∃ i : ℕ, 0 < i ∧ i ≤ (f.cycleOf x).support.card ∧ (f ^ i) x = y := by
  obtain ⟨k, hk, hk'⟩ := h.exists_pow_eq_of_mem_support hx
  cases' k with k
  · refine ⟨(f.cycleOf x).support.card, ?_, le_rfl, ?_⟩
    · refine zero_lt_one.trans (one_lt_card_support_of_ne_one ?_)
      simpa using hx
    · simp only [Nat.zero_eq, pow_zero, coe_one, id_eq] at hk'
      subst hk'
      rw [← (isCycle_cycleOf _ <| mem_support.1 hx).orderOf, ← cycleOf_pow_apply_self,
        pow_orderOf_eq_one, one_apply]
  · exact ⟨k + 1, by simp, hk.le, hk'⟩

lemma exists_pow_eq_mem_finset_support_of_fix [DecidableEq α] (π : Equiv.Perm α) {s : Finset α}
  (hsx : ∀ x, x ∈ s ↔ π x ∈ s) (hx : x ∈ s) (hxπ : π x ≠ x) :
    ∃ k, (k > 0 ∧ k ≤ s.card ∧ (π^k) x = x) := by
  rw [← Finset.card_attach, ← Finset.univ_eq_attach]
  have H := (SameCycle.refl (π.subtypePerm hsx) ⟨x, hx⟩).exists_pow_eq_of_mem_support' _
  simp_rw [subtypePerm_pow, subtypePerm_apply, Subtype.mk.injEq, support_subtype_perm,
    Finset.mem_filter, decide_eq_true_iff, Finset.mem_attach, true_and] at H
  rcases H hxπ with ⟨k, hk, hkx, hkπ⟩
  exact ⟨k, hk, hkx.trans (Finset.card_le_univ _), hkπ⟩

[Wrenna Robson]

I don't quite understand why we don't have my SameCycle.exists_pow_eq_of_mem_support'. We have something very close (SameCycle.exists_pow_eq_of_mem_support, SameCycle.exists_pow_eq) but the precise thing I have here, I don't think so?