Documentation

Mathlib.GroupTheory.Perm.Fin

Permutations of Fin n #

source
def Equiv.Perm.decomposeFin {n : ℕ} :
Equiv.Perm (Fin (Nat.succ n)) ≃ Fin (Nat.succ n) × 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
Instances For
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) :
    ↑Equiv.Perm.decomposeFin.symm (p, Equiv.refl (Fin n)) = Equiv.swap 0 p
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_of_one {n : ℕ} (p : Fin (n + 1)) :
    ↑Equiv.Perm.decomposeFin.symm (p, 1) = Equiv.swap 0 p
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)) :
    ↑(↑Equiv.Perm.decomposeFin.symm (p, e)) 0 = p
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : ℕ} (e : Equiv.Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n) :
    ↑(↑Equiv.Perm.decomposeFin.symm (p, e)) (Fin.succ x) = ↑(Equiv.swap 0 p) (Fin.succ (↑e x))
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_apply_one {n : ℕ} (e : Equiv.Perm (Fin (n + 1))) (p : Fin (n + 2)) :
    ↑(↑Equiv.Perm.decomposeFin.symm (p, e)) 1 = ↑(Equiv.swap 0 p) (Fin.succ (↑e 0))
    source
    @[simp]
    theorem Equiv.Perm.decomposeFin.symm_sign {n : ℕ} (p : Fin (n + 1)) (e : Equiv.Perm (Fin n)) :
    ↑Equiv.Perm.sign (↑Equiv.Perm.decomposeFin.symm (p, e)) = (if p = 0 then 1 else -1) * ↑Equiv.Perm.sign e
    source
    theorem Finset.univ_perm_fin_succ {n : ℕ} :
    Finset.univ = Finset.map (Equiv.toEmbedding Equiv.Perm.decomposeFin.symm) 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.

    cycleRange section #

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

    source
    theorem finRotate_succ_eq_decomposeFin {n : ℕ} :
    finRotate (Nat.succ n) = ↑Equiv.Perm.decomposeFin.symm (1, finRotate n)
    source
    @[simp]
    theorem sign_finRotate (n : ℕ) :
    ↑Equiv.Perm.sign (finRotate (n + 1)) = (-1) ^ n
    source
    @[simp]
    theorem support_finRotate {n : ℕ} :
    Equiv.Perm.support (finRotate (n + 2)) = Finset.univ
    source
    theorem support_finRotate_of_le {n : ℕ} (h : 2 ≤ n) :
    Equiv.Perm.support (finRotate n) = Finset.univ
    source
    theorem isCycle_finRotate {n : ℕ} :
    Equiv.Perm.IsCycle (finRotate (n + 2))
    source
    theorem isCycle_finRotate_of_le {n : ℕ} (h : 2 ≤ n) :
    Equiv.Perm.IsCycle (finRotate n)
    source
    @[simp]
    theorem cycleType_finRotate {n : ℕ} :
    Equiv.Perm.cycleType (finRotate (n + 2)) = {n + 2}
    source
    theorem cycleType_finRotate_of_le {n : ℕ} (h : 2 ≤ n) :
    Equiv.Perm.cycleType (finRotate n) = {n}
    source
    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
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      theorem Fin.cycleRange_of_gt {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : i < j) :
      ↑(Fin.cycleRange i) j = j
      source
      theorem Fin.cycleRange_of_le {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j ≤ i) :
      ↑(Fin.cycleRange i) j = if j = i then 0 else j + 1
      source
      theorem Fin.coe_cycleRange_of_le {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j ≤ i) :
      ↑(↑(Fin.cycleRange i) j) = if j = i then 0 else ↑j + 1
      source
      theorem Fin.cycleRange_of_lt {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j < i) :
      ↑(Fin.cycleRange i) j = j + 1
      source
      theorem Fin.coe_cycleRange_of_lt {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j < i) :
      ↑(↑(Fin.cycleRange i) j) = ↑j + 1
      source
      theorem Fin.cycleRange_of_eq {n : ℕ} {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j = i) :
      ↑(Fin.cycleRange i) j = 0
      source
      @[simp]
      theorem Fin.cycleRange_self {n : ℕ} (i : Fin (Nat.succ n)) :
      ↑(Fin.cycleRange i) i = 0
      source
      theorem Fin.cycleRange_apply {n : ℕ} (i : Fin (Nat.succ n)) (j : Fin (Nat.succ n)) :
      ↑(Fin.cycleRange i) j = if j < i then j + 1 else if j = i then 0 else j
      source
      @[simp]
      theorem Fin.cycleRange_zero (n : ℕ) :
      Fin.cycleRange 0 = 1
      source
      @[simp]
      theorem Fin.cycleRange_last (n : ℕ) :
      Fin.cycleRange (Fin.last n) = finRotate (n + 1)
      source
      @[simp]
      theorem Fin.cycleRange_zero' {n : ℕ} (h : 0 < n) :
      Fin.cycleRange { val := 0, isLt := h } = 1
      source
      @[simp]
      theorem Fin.sign_cycleRange {n : ℕ} (i : Fin n) :
      ↑Equiv.Perm.sign (Fin.cycleRange i) = (-1) ^ ↑i
      source
      @[simp]
      theorem Fin.succAbove_cycleRange {n : ℕ} (i : Fin n) (j : Fin n) :
      Fin.succAbove (Fin.succ i) (↑(Fin.cycleRange i) j) = ↑(Equiv.swap 0 (Fin.succ i)) (Fin.succ j)
      source
      @[simp]
      theorem Fin.cycleRange_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
      ↑(Fin.cycleRange i) (Fin.succAbove i j) = Fin.succ j
      source
      @[simp]
      theorem Fin.cycleRange_symm_zero {n : ℕ} (i : Fin (n + 1)) :
      ↑(Fin.cycleRange i).symm 0 = i
      source
      @[simp]
      theorem Fin.cycleRange_symm_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
      ↑(Fin.cycleRange i).symm (Fin.succ j) = Fin.succAbove i j
      source
      theorem Fin.isCycle_cycleRange {n : ℕ} {i : Fin (n + 1)} (h0 : i ≠ 0) :
      Equiv.Perm.IsCycle (Fin.cycleRange i)
      source
      @[simp]
      theorem Fin.cycleType_cycleRange {n : ℕ} {i : Fin (n + 1)} (h0 : i ≠ 0) :
      Equiv.Perm.cycleType (Fin.cycleRange i) = {↑i + 1}
      source
      theorem Fin.isThreeCycle_cycleRange_two {n : ℕ} :
      Equiv.Perm.IsThreeCycle (Fin.cycleRange 2)