Permutations of Fin n

def Equiv.Perm.decomposeFin {n : ℕ} : Perm (Fin n.succ) ≃ Fin n.succ × Perm (Fin n)

Permutations of Fin (n + 1) are equivalent to fixing a single Fin (n + 1) and permuting the remaining with a Perm (Fin n). The fixed Fin (n + 1) is swapped with 0. (See also Equiv.Perm.decomposeFin' for a slightly different bijection.)

Equations

• Equiv.Perm.decomposeFin = ((finSuccEquiv n).permCongr.trans Equiv.Perm.decomposeOption).trans ((finSuccEquiv n).symm.prodCongr (Equiv.refl (Equiv.Perm (Fin n))))

@[simp]

theorem Equiv.Perm.decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) : decomposeFin.symm (p, Equiv.refl (Fin n)) = swap 0 p

@[simp]

theorem Equiv.Perm.decomposeFin_symm_of_one {n : ℕ} (p : Fin (n + 1)) : decomposeFin.symm (p, 1) = swap 0 p

@[simp]

theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) : (decomposeFin.symm (p, e)) 0 = p

@[simp]

theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : ℕ} (e : Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n) : (decomposeFin.symm (p, e)) x.succ = (swap 0 p) (e x).succ

@[simp]

theorem Equiv.Perm.decomposeFin_symm_apply_one {n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) : (decomposeFin.symm (p, e)) 1 = (swap 0 p) (e 0).succ

@[simp]

theorem Equiv.Perm.decomposeFin.symm_sign {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) : sign (decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * sign e

theorem Finset.univ_perm_fin_succ {n : ℕ} : univ = map Equiv.Perm.decomposeFin.symm.toEmbedding univ

The set of all permutations of Fin (n + 1) can be constructed by augmenting the set of permutations of Fin n by each element of Fin (n + 1) in turn.

cycleRange section

Define the permutations Fin.cycleRange i, the cycle (0 1 2 ... i).

theorem finRotate_succ_eq_decomposeFin {n : ℕ} : finRotate n.succ = Equiv.Perm.decomposeFin.symm (1, finRotate n)

@[simp]

theorem sign_finRotate (n : ℕ) : Equiv.Perm.sign (finRotate n) = (-1) ^ (n - 1)

@[simp]

theorem support_finRotate {n : ℕ} : (finRotate (n + 2)).support = Finset.univ

theorem support_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : (finRotate n).support = Finset.univ

theorem isCycle_finRotate {n : ℕ} : (finRotate (n + 2)).IsCycle

theorem isCycle_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : (finRotate n).IsCycle

@[simp]

theorem cycleType_finRotate {n : ℕ} : (finRotate (n + 2)).cycleType = {n + 2}

theorem cycleType_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : (finRotate n).cycleType = {n}

def Fin.cycleRange {n : ℕ} (i : Fin n) : Equiv.Perm (Fin n)

Fin.cycleRange i is the cycle (0 1 2 ... i) leaving (i+1 ... (n-1)) unchanged.

Equations

• i.cycleRange = (finRotate (↑i + 1)).extendDomain (Fin.castLEEmb ⋯).toEquivRange

theorem Fin.cycleRange_of_gt {n : ℕ} {i j : Fin n} (h : i < j) : i.cycleRange j = j

theorem Fin.cycleRange_of_le {n : ℕ} {i j : Fin n} [NeZero n] (h : i ≤ j) : j.cycleRange i = if i = j then 0 else i + 1

theorem Fin.coe_cycleRange_of_le {n : ℕ} {i j : Fin n} (h : i ≤ j) : ↑(j.cycleRange i) = if i = j then 0 else ↑i + 1

theorem Fin.cycleRange_of_lt {n : ℕ} {i j : Fin n} [NeZero n] (h : i < j) : j.cycleRange i = i + 1

theorem Fin.coe_cycleRange_of_lt {n : ℕ} {i j : Fin n} (h : i < j) : ↑(j.cycleRange i) = ↑i + 1

theorem Fin.cycleRange_of_eq {n : ℕ} {i j : Fin n} [NeZero n] (h : i = j) : j.cycleRange i = 0

@[simp]

theorem Fin.cycleRange_self {n : ℕ} [NeZero n] (i : Fin n) : i.cycleRange i = 0

theorem Fin.cycleRange_apply {n : ℕ} [NeZero n] (i j : Fin n) : i.cycleRange j = if j < i then j + 1 else if j = i then 0 else j

@[simp]

theorem Fin.cycleRange_zero (n : ℕ) [NeZero n] : cycleRange 0 = 1

@[simp]

theorem Fin.cycleRange_last (n : ℕ) : (last n).cycleRange = finRotate (n + 1)

@[simp]

theorem Fin.cycleRange_mk_zero {n : ℕ} (h : 0 < n) : ⟨0, h⟩.cycleRange = 1

@[simp]

theorem Fin.sign_cycleRange {n : ℕ} (i : Fin n) : Equiv.Perm.sign i.cycleRange = (-1) ^ ↑i

@[simp]

theorem Fin.succAbove_cycleRange {n : ℕ} (i j : Fin n) : i.succ.succAbove (i.cycleRange j) = (Equiv.swap 0 i.succ) j.succ

@[simp]

theorem Fin.cycleRange_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.cycleRange (i.succAbove j) = j.succ

@[simp]

theorem Fin.cycleRange_symm_zero {n : ℕ} [NeZero n] (i : Fin n) : (Equiv.symm i.cycleRange) 0 = i

@[simp]

theorem Fin.cycleRange_symm_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) : (Equiv.symm i.cycleRange) j.succ = i.succAbove j

@[simp]

theorem Fin.insertNth_apply_cycleRange_symm {n : ℕ} {α : Type u_1} (p : Fin (n + 1)) (a : α) (x : Fin n → α) (j : Fin (n + 1)) : p.insertNth a x ((Equiv.symm p.cycleRange) j) = cons a x j

@[simp]

theorem Fin.insertNth_comp_cycleRange_symm {n : ℕ} {α : Type u_1} (p : Fin (n + 1)) (a : α) (x : Fin n → α) : p.insertNth a x ∘ ⇑(Equiv.symm p.cycleRange) = cons a x

theorem Fin.cons_removeNth_eq_comp_cycleRange_symm {n : ℕ} {α : Type u_1} (x : Fin (n + 1) → α) (p : Fin (n + 1)) : cons (x p) (p.removeNth x) = x ∘ ⇑(Equiv.symm p.cycleRange)

@[simp]

theorem Fin.cons_apply_cycleRange {n : ℕ} {α : Type u_1} (a : α) (x : Fin n → α) (p j : Fin (n + 1)) : cons a x (p.cycleRange j) = p.insertNth a x j

@[simp]

theorem Fin.cons_comp_cycleRange {n : ℕ} {α : Type u_1} (a : α) (x : Fin n → α) (p : Fin (n + 1)) : cons a x ∘ ⇑p.cycleRange = p.insertNth a x

theorem Fin.isCycle_cycleRange {n : ℕ} {i : Fin n} [NeZero n] (h0 : i ≠ 0) : i.cycleRange.IsCycle

@[simp]

theorem Fin.cycleType_cycleRange {n : ℕ} {i : Fin n} [NeZero n] (h0 : i ≠ 0) : i.cycleRange.cycleType = {↑i + 1}

theorem Fin.isThreeCycle_cycleRange_two {n : ℕ} : (cycleRange 2).IsThreeCycle

The permutation cycleIcc

In this section, we define the permutation cycleIcc i j, which 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.

theorem Fin.instNeZeroNatHSubVal_mathlib {n : ℕ} {i : Fin n} : NeZero (n - ↑i)

def Fin.cycleIcc {n : ℕ} (i j : Fin n) : Equiv.Perm (Fin n)

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.

Equations

• i.cycleIcc j = if hij : i ≤ j then ((j - i).castLT ⋯).cycleRange.extendDomain (Fin.natAdd_castLEEmb ⋯).toEquivRange else 1

@[simp]

theorem Fin.cycleIcc_def_le {n : ℕ} {i j : Fin n} (hij : i ≤ j) : i.cycleIcc j = ((j - i).castLT ⋯).cycleRange.extendDomain (natAdd_castLEEmb ⋯).toEquivRange

@[simp]

theorem Fin.cycleIcc_def_gt {n : ℕ} {i j : Fin n} (hij : i < j) : j.cycleIcc i = 1

@[simp]

theorem Fin.cycleIcc_def_gt' {n : ℕ} {i j : Fin n} (hij : ¬j ≤ i) : j.cycleIcc i = 1

theorem Fin.cycleIcc_of_lt {n : ℕ} {i j k : Fin n} (h : k < i) : (i.cycleIcc j) k = k

theorem Fin.cycleIcc_to_cycleRange {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (kin : k ∈ Set.range ⇑(natAdd_castLEEmb ⋯)) : (i.cycleIcc j) k = (natAdd_castLEEmb ⋯) (((j - i).castLT ⋯).cycleRange ((natAdd_castLEEmb ⋯).toEquivRange.symm ⟨k, kin⟩))

theorem Fin.cycleIcc_of_gt {n : ℕ} {i j k : Fin n} (h : j < k) : (i.cycleIcc j) k = k

@[simp]

theorem Fin.cycleIcc_of_le_of_le {n : ℕ} {i j k : Fin n} (hik : i ≤ k) (hkj : k ≤ j) [NeZero n] : (i.cycleIcc j) k = if k = j then i else k + 1

theorem Fin.cycleIcc_of_ge_of_lt {n : ℕ} {i j k : Fin n} (hik : i ≤ k) (hkj : k < j) [NeZero n] : (i.cycleIcc j) k = k + 1

theorem Fin.cycleIcc_of_last {n : ℕ} {i j : Fin n} (hij : i ≤ j) [NeZero n] : (i.cycleIcc j) j = i

theorem Fin.cycleIcc_eq {n : ℕ} {i : Fin n} [NeZero n] : i.cycleIcc i = 1

@[simp]

theorem Fin.cycleIcc_ge {n : ℕ} {i j : Fin n} (hij : i ≤ j) [NeZero n] : j.cycleIcc i = 1

theorem Fin.sign_cycleIcc_of_le {n : ℕ} {i j : Fin n} (hij : i ≤ j) : Equiv.Perm.sign (i.cycleIcc j) = (-1) ^ (↑j - ↑i)

theorem Fin.sign_cycleIcc_of_eq {n : ℕ} {i : Fin n} : Equiv.Perm.sign (i.cycleIcc i) = 1

theorem Fin.sign_cycleIcc_of_ge {n : ℕ} {i j : Fin n} (hij : i ≤ j) : Equiv.Perm.sign (j.cycleIcc i) = 1

theorem Fin.isCycle_cycleIcc {n : ℕ} {i j : Fin n} (hij : i < j) : (i.cycleIcc j).IsCycle

theorem Fin.cycleType_cycleIcc_of_lt {n : ℕ} {i j : Fin n} (hij : i < j) : (i.cycleIcc j).cycleType = {↑j - ↑i + 1}

theorem Fin.cycleType_cycleIcc_of_ge {n : ℕ} {i j : Fin n} (hij : i ≤ j) [NeZero n] : (j.cycleIcc i).cycleType = ∅

theorem Fin.cycleIcc_zero_eq_cycleRange {n : ℕ} (i : Fin n) [NeZero n] : cycleIcc 0 i = i.cycleRange

theorem Fin.cycleIcc_comp_succAbove {n : ℕ} (i j : Fin (n + 1)) (hij : i ≤ j) : ⇑(i.cycleIcc j) ∘ j.succAbove = i.succAbove

theorem Fin.cycleIcc.trans {n : ℕ} {i j k : Fin n} [NeZero n] (hij : i ≤ j) (hjk : j ≤ k) : ⇑(i.cycleIcc j) ∘ ⇑(j.cycleIcc k) = ⇑(i.cycleIcc k)

theorem Fin.cycleIcc.trans_left_one {n : ℕ} {i j k : Fin n} [NeZero n] (hij : i ≤ j) : ⇑(j.cycleIcc i) ∘ ⇑(i.cycleIcc k) = ⇑(i.cycleIcc k)

theorem Fin.cycleIcc.trans_right_one {n : ℕ} {i j k : Fin n} [NeZero n] (hjk : j ≤ k) : ⇑(i.cycleIcc k) ∘ ⇑(k.cycleIcc j) = ⇑(i.cycleIcc k)

theorem Equiv.Perm.sign_eq_prod_prod_Iio {n : ℕ} (σ : Perm (Fin n)) : sign σ = ∏ j : Fin n, ∏ i < j, if σ i < σ j then 1 else -1

theorem Equiv.Perm.sign_eq_prod_prod_Ioi {n : ℕ} (σ : Perm (Fin n)) : sign σ = ∏ i : Fin n, ∏ j > i, if σ i < σ j then 1 else -1

theorem Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod {n : ℕ} {R : Type u_1} [CommRing R] (σ : Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ (i j : Fin n), f i j = -f j i) : ∏ j : Fin n, ∏ i < j, f (σ i) (σ j) = ↑↑(sign σ) * ∏ j : Fin n, ∏ i < j, f i j

theorem Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod {n : ℕ} {R : Type u_1} [CommRing R] (σ : Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ (i j : Fin n), f i j = -f j i) : ∏ i : Fin n, ∏ j > i, f (σ i) (σ j) = ↑↑(sign σ) * ∏ i : Fin n, ∏ j > i, f i j

noncomputable def Equiv.Perm.decomposeFin'Symm {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : Perm (Fin (n + 2))

Given i : Fin (n + 2) and σ : Perm (Fin (n + 1), this is the permutation of Fin (n + 2) which sends 0 to i and j.succ to i.succAbove (σ j).

Equations

• Equiv.Perm.decomposeFin'Symm i σ = Equiv.ofBijective (fun (i_1 : Fin (n + 1 + 1)) => Fin.cases i (i.succAbove ∘ ⇑σ) i_1) ⋯

@[simp]

theorem Equiv.Perm.decomposeFin'Symm_zero {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : (decomposeFin'Symm i σ) 0 = i

@[simp]

theorem Equiv.Perm.decomposeFin'Symm_succ {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) (j : Fin (n + 1)) : (decomposeFin'Symm i σ) j.succ = i.succAbove (σ j)

@[simp]

theorem Equiv.Perm.decomposeFin'Symm_symm_eq_zero {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : (Equiv.symm (decomposeFin'Symm i σ)) i = 0

@[simp]

theorem Equiv.Perm.decomposeFin'Symm_symm_succAbove {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) (j : Fin (n + 1)) : (Equiv.symm (decomposeFin'Symm i σ)) (i.succAbove (σ j)) = j.succ

theorem Equiv.Perm.decomposeFin'Symm_uncurry_bijective (n : ℕ) : Function.Bijective (Function.uncurry decomposeFin'Symm)

noncomputable def Equiv.Perm.decomposeFin' {n : ℕ} : Perm (Fin (n + 2)) ≃ Fin (n + 2) × Perm (Fin (n + 1))

A bijection between Perm (Fin (n + 2)) and Fin (n + 2) × Perm (Fin (n + 1)). The inverse map sends ⟨i, σ⟩ (with i : Fin (n + 2) and σ : Perm (Fin (n + 1)) to decomposeFin'Symm i σ which sends 0 to i and j.succ to i.succAbove (σ j). (This bijection is slightly different from Equiv.Perm.decomposeFin.)

Equations

• Equiv.Perm.decomposeFin' = (Equiv.ofBijective (Function.uncurry Equiv.Perm.decomposeFin'Symm) ⋯).symm

@[simp]

theorem Equiv.Perm.decomposeFin'_symm {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : decomposeFin'.symm (i, σ) = decomposeFin'Symm i σ

@[simp]

theorem Equiv.Perm.sign_decomposeFin'Symm {n : ℕ} (i : Fin (n + 2)) (σ : Perm (Fin (n + 1))) : sign (decomposeFin'Symm i σ) = (-1) ^ ↑i * sign σ