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.

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)) = (-1) ^ n

@[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 (Equiv.ofLeftInverse' (⇑(Fin.castLEEmb ⋯)) (fun (x : Fin n) => ↑↑x) ⋯)

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

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

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

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

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

theorem Fin.cycleRange_of_eq {n : ℕ} [NeZero n] {i j : Fin n} (h : j = i) : i.cycleRange j = 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

@[deprecated Fin.cycleRange_mk_zero (since := "2025-01-28")]

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

Alias of Fin.cycleRange_mk_zero.

@[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

@[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 : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) : i.cycleRange.IsCycle

@[simp]

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

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

theorem Equiv.Perm.sign_eq_prod_prod_Iio {n : ℕ} (σ : Perm (Fin n)) : sign σ = ∏ j : Fin n, ∏ i ∈ Finset.Iio 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 ∈ Finset.Ioi 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 ∈ Finset.Iio j, f (σ i) (σ j) = ↑↑(sign σ) * ∏ j : Fin n, ∏ i ∈ Finset.Iio 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 ∈ Finset.Ioi i, f (σ i) (σ j) = ↑↑(sign σ) * ∏ i : Fin n, ∏ j ∈ Finset.Ioi i, f i j