Equivalences for finite indices and consecutive blocks of natural numbers

The equivalence omitting the last finite index embeds preceding indices by Fin.castSucc. The quotient-remainder equivalence identifies a natural number with a block number and a position inside that block. This file records the induced block permutations and compatibility of nested blocks with the finite-product indexing equivalence.

@[simp]

theorem TauCeti.finSuccAboveEquiv_last_apply (n : ℕ) (i : Fin n) : (finSuccAboveEquiv (Fin.last n)) i = ⟨i.castSucc, ⋯⟩

Omitting the last index embeds each preceding index by Fin.castSucc.

def Nat.blockPerm (m : ℕ) [NeZero m] (τ : Equiv.Perm ℕ) : Equiv.Perm ℕ

The permutation of path coordinates that permutes the consecutive blocks of width m by τ and preserves the position inside each block.

Equations

• m.blockPerm τ = m.divModEquiv.symm.permCongr (Equiv.prodCongr τ (Equiv.refl (Fin m)))

@[simp]

theorem Nat.blockPerm_mul_add (m : ℕ) [NeZero m] (τ : Equiv.Perm ℕ) (i : ℕ) (j : Fin m) : (m.blockPerm τ) (i * m + ↑j) = τ i * m + ↑j

The block permutation moves position j of block i to position j of block τ i.

theorem Nat.divModEquiv_symm_finProdFinEquiv (m n : ℕ) [NeZero m] [NeZero n] (i : ℕ) (r : Fin n) (j : Fin m) : (n * m).divModEquiv.symm (i, finProdFinEquiv (r, j)) = m.divModEquiv.symm (i * n + ↑r, j)

Flattening nested finite blocks agrees with the quotient-remainder inverse.