mathlib3 documentation

group_theory.perm.fin

Permutations of fin n #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
def equiv.perm.decompose_fin {n : ℕ} :
equiv.perm (fin n.succ) ≃ fin n.succ × equiv.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
source
@[simp]
theorem equiv.perm.decompose_fin_symm_of_refl {n : ℕ} (p : fin (n + 1)) :
⇑(equiv.perm.decompose_fin.symm) (p, equiv.refl (fin n)) = equiv.swap 0 p
source
@[simp]
theorem equiv.perm.decompose_fin_symm_of_one {n : ℕ} (p : fin (n + 1)) :
⇑(equiv.perm.decompose_fin.symm) (p, 1) = equiv.swap 0 p
source
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_zero {n : ℕ} (p : fin (n + 1)) (e : equiv.perm (fin n)) :
⇑(⇑(equiv.perm.decompose_fin.symm) (p, e)) 0 = p
source
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_succ {n : ℕ} (e : equiv.perm (fin n)) (p : fin (n + 1)) (x : fin n) :
⇑(⇑(equiv.perm.decompose_fin.symm) (p, e)) x.succ = ⇑(equiv.swap 0 p) (⇑e x).succ
source
@[simp]
theorem equiv.perm.decompose_fin_symm_apply_one {n : ℕ} (e : equiv.perm (fin (n + 1))) (p : fin (n + 2)) :
⇑(⇑(equiv.perm.decompose_fin.symm) (p, e)) 1 = ⇑(equiv.swap 0 p) (⇑e 0).succ
source
@[simp]
theorem equiv.perm.decompose_fin.symm_sign {n : ℕ} (p : fin (n + 1)) (e : equiv.perm (fin n)) :
⇑equiv.perm.sign (⇑(equiv.perm.decompose_fin.symm) (p, e)) = ite (p = 0) 1 (-1) * ⇑equiv.perm.sign e
source
theorem finset.univ_perm_fin_succ {n : ℕ} :
finset.univ = finset.map equiv.perm.decompose_fin.symm.to_embedding finset.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.

cycle_range section #

Define the permutations fin.cycle_range i, the cycle (0 1 2 ... i).

source
theorem fin_rotate_succ {n : ℕ} :
fin_rotate n.succ = ⇑(equiv.perm.decompose_fin.symm) (1, fin_rotate n)
source
@[simp]
theorem sign_fin_rotate (n : ℕ) :
⇑equiv.perm.sign (fin_rotate (n + 1)) = (-1) ^ n
source
@[simp]
theorem support_fin_rotate {n : ℕ} :
(fin_rotate (n + 2)).support = finset.univ
source
theorem support_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) :
(fin_rotate n).support = finset.univ
source
theorem is_cycle_fin_rotate {n : ℕ} :
(fin_rotate (n + 2)).is_cycle
source
theorem is_cycle_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) :
(fin_rotate n).is_cycle
source
@[simp]
theorem cycle_type_fin_rotate {n : ℕ} :
(fin_rotate (n + 2)).cycle_type = {n + 2}
source
theorem cycle_type_fin_rotate_of_le {n : ℕ} (h : 2 ≤ n) :
(fin_rotate n).cycle_type = {n}
source
def fin.cycle_range {n : ℕ} (i : fin n) :
equiv.perm (fin n)

fin.cycle_range i is the cycle (0 1 2 ... i) leaving (i+1 ... (n-1)) unchanged.

Equations
source
theorem fin.cycle_range_of_gt {n : ℕ} {i j : fin n.succ} (h : i < j) :
⇑(i.cycle_range) j = j
source
theorem fin.cycle_range_of_le {n : ℕ} {i j : fin n.succ} (h : j ≤ i) :
⇑(i.cycle_range) j = ite (j = i) 0 (j + 1)
source
theorem fin.coe_cycle_range_of_le {n : ℕ} {i j : fin n.succ} (h : j ≤ i) :
↑(⇑(i.cycle_range) j) = ite (j = i) 0 (↑j + 1)
source
theorem fin.cycle_range_of_lt {n : ℕ} {i j : fin n.succ} (h : j < i) :
⇑(i.cycle_range) j = j + 1
source
theorem fin.coe_cycle_range_of_lt {n : ℕ} {i j : fin n.succ} (h : j < i) :
↑(⇑(i.cycle_range) j) = ↑j + 1
source
theorem fin.cycle_range_of_eq {n : ℕ} {i j : fin n.succ} (h : j = i) :
⇑(i.cycle_range) j = 0
source
@[simp]
theorem fin.cycle_range_self {n : ℕ} (i : fin n.succ) :
⇑(i.cycle_range) i = 0
source
theorem fin.cycle_range_apply {n : ℕ} (i j : fin n.succ) :
⇑(i.cycle_range) j = ite (j < i) (j + 1) (ite (j = i) 0 j)
source
@[simp]
theorem fin.cycle_range_zero (n : ℕ) :
0.cycle_range = 1
source
@[simp]
theorem fin.cycle_range_last (n : ℕ) :
(fin.last n).cycle_range = fin_rotate (n + 1)
source
@[simp]
theorem fin.cycle_range_zero' {n : ℕ} (h : 0 < n) :
⟨0, h⟩.cycle_range = 1
source
@[simp]
theorem fin.sign_cycle_range {n : ℕ} (i : fin n) :
⇑equiv.perm.sign i.cycle_range = (-1) ^ ↑i
source
@[simp]
theorem fin.succ_above_cycle_range {n : ℕ} (i j : fin n) :
⇑(i.succ.succ_above) (⇑(i.cycle_range) j) = ⇑(equiv.swap 0 i.succ) j.succ
source
@[simp]
theorem fin.cycle_range_succ_above {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑(i.cycle_range) (⇑(i.succ_above) j) = j.succ
source
@[simp]
theorem fin.cycle_range_symm_zero {n : ℕ} (i : fin (n + 1)) :
⇑(equiv.symm i.cycle_range) 0 = i
source
@[simp]
theorem fin.cycle_range_symm_succ {n : ℕ} (i : fin (n + 1)) (j : fin n) :
⇑(equiv.symm i.cycle_range) j.succ = ⇑(i.succ_above) j
source
theorem fin.is_cycle_cycle_range {n : ℕ} {i : fin (n + 1)} (h0 : i ≠ 0) :
i.cycle_range.is_cycle
source
@[simp]
theorem fin.cycle_type_cycle_range {n : ℕ} {i : fin (n + 1)} (h0 : i ≠ 0) :
i.cycle_range.cycle_type = {↑i + 1}
source
theorem fin.is_three_cycle_cycle_range_two {n : ℕ} :
2.cycle_range.is_three_cycle