Commit 2025-08-18 09:17 4eba5edd

feat(GroupTheory/Perm/Fin): add Fin.cycleIcc and refactor cycleRange (#27014) In this PR, I define the permutation cycleIcc i j hij, which is the cycle (i i+1 .... j) leaving (0 ... i-1) and (j+1 ... n-1) unchanged. In other words, it rotates elements in [i, j] one step to the right. Also I prove some properties of cycleIcc i j hij such as the fact that it is a cycle and its cycleType is j - i. This definition is used to prove the following result:

theorem succAbove_comp_cycleIcc [NeZero n] (x : Fin (n + 1) → L) (i j : Fin (n + 1)) (eq : x i = x j) (lt : i < j)
x ∘ i.succAbove = x ∘ j.succAbove ∘ (cycleIcc hij)

More clearly, x ∘ i.succAbove and x ∘ j.succAbove are Fin n → L types. For example, when n = 6, i = 2, j = 5 and x i = x j

x ∘ i.succAbove = (x 0, x 1, x 3, x 4, x 5, x 6)
x ∘ j.succAbove = (x 0, x 1, x 2, x 3, x 4, x 6)

We have

                (x 0, x 1, x 3, x 4, x 5, x 6)
--(cycleIcc)