English
cycleIcc is defined by a case distinction: if i ≤ j, it is a lifted and extended cycleRange; otherwise it is the identity.
Русский
cycleIcc задано по разбору случая: если i ≤ j, это поднятый и расширенный cycleRange; иначе — тождество.
LaTeX
$$$cycleIcc(i,j) = \\begin{cases} cycleRange((j-i).castLT(\\text{sub\_val\_lt\_sub}(\\text{hij})) ).extendDomain( natAddCastLEEmb( Nat.sub\_le \\, n\, i) ).toEquivRange, & \\text{если } i \\le j, \\\\ 1, & \\text{иначе} \\end{cases}$$$
Lean4
/-- `cycleIcc i j` is the cycle `(i i+1 ... j)` leaving `(0 ... i-1)` and `(j+1 ... n-1)`
unchanged when `i < j` and returning the dummy value `id` when `i > j`.
In other words, it rotates elements in `[i, j]` one step to the right.
-/
/- `cycleIcc` is defined in two steps:
1. The first part is `cycleRange ((j - i).castLT (sub_val_lt_sub hij))`, which is an element of
`Perm (Fin (n - i))`. It rotates the sequence `(0 1 ... j-i)` while leaving `(j-i+1 ... n-i)`
unchanged.
2. Since `natAdd_castLEEmb (Nat.sub_le n i) : Fin (n - i) ↪ Fin n` maps each `x` to `x + i`, we can
embed the first part into `Fin n` using `extendDomain` to obtain an element of `Perm (Fin n)`.
This yields the cycle `(i i+1 ... j)` while leaving `(0 ... i-1)` and `(j+1 ... n-1)` unchanged.
-/
def cycleIcc (i j : Fin n) : Perm (Fin n) :=
if hij : i ≤ j then
(cycleRange ((j - i).castLT (sub_val_lt_sub hij))).extendDomain (natAdd_castLEEmb (Nat.sub_le n i)).toEquivRange
else 1
