large permutation

Stream: new members

[vxctyxeha]

i try to prove the follow,but how to constructor σ that
Implement a cycle of length 673 on 0 to 672 (0→1→2→...→672→0).
Implement a cycle of length 3 on 673, 674, 675 (673→674→675→673).
The remaining points (676 to 2019) remain fixed.

import Mathlib

open scoped Finset

namespace Equiv.Perm

open Equiv List Multiset


theorem h_exists : ∃ σ : Equiv.Perm (Fin 2020),
    orderOf σ = 2019 ∧ Fintype.card (Function.fixedPoints σ) = 1344 := by sorry

[Matt Diamond]

this should work:

import Mathlib

open scoped Finset

namespace Equiv.Perm

open Equiv List Multiset

theorem h_exists : ∃ σ : Equiv.Perm (Fin 2020),
    orderOf σ = 2019 ∧ Fintype.card (Function.fixedPoints σ) = 1344 :=
⟨
  finSumFinEquiv.permCongr ((finRotate 673).sumCongr (finRotate 3))
    |>.extendDomain (Fin.castLEquiv (by decide)),
  sorry
⟩

[Matt Diamond]

(on a side note, that function should probably be called Fin.castLEEquiv...)

[vxctyxeha]

another question ，how to prove that (finRotate 673) ^ 673 = 1

[Weiyi Wang]

I am surprised I couldn't find this in mathlib, but should be provable for general n using finRotate_succ_apply and induction

[Matt Diamond]

here's a proof if you still need one:

import Mathlib

lemma finRotate_pow (m n : ℕ) (k : Fin (m + 1)) : ((finRotate (m + 1)) ^ n) k = Fin.ofNat (m + 1) (k + n) :=
by
  rw [← Equiv.Perm.iterate_eq_pow]
  induction n with
  | zero => simp
  | succ d IH =>
    rw [Function.iterate_succ_apply', finRotate_succ_apply, IH]
    apply Fin.eq_of_val_eq
    simp [Fin.val_add, add_assoc]

lemma finRotate_pow_self_eq_one (n : ℕ) : (finRotate n) ^ n = 1 :=
by
  cases n with
  | zero => simp
  | succ d => ext k; simp [finRotate_pow]