Documentation

Mathlib.GroupTheory.Perm.Fin

Permutations of 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
    @[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
    @[simp]
    theorem Equiv.Perm.decomposeFin_symm_of_one {n : } (p : Fin (n + 1)) :
    Equiv.Perm.decomposeFin.symm (p, 1) = Equiv.swap 0 p
    @[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
    @[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))
    @[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))
    @[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
    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).

    theorem finRotate_succ_eq_decomposeFin {n : } :
    finRotate (Nat.succ n) = 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 : } :
    Equiv.Perm.support (finRotate (n + 2)) = Finset.univ
    theorem support_finRotate_of_le {n : } (h : 2 n) :
    @[simp]
    def Fin.cycleRange {n : } (i : 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
      theorem Fin.cycleRange_of_gt {n : } {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : i < j) :
      ↑(Fin.cycleRange i) j = j
      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
      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
      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
      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
      theorem Fin.cycleRange_of_eq {n : } {i : Fin (Nat.succ n)} {j : Fin (Nat.succ n)} (h : j = i) :
      ↑(Fin.cycleRange i) j = 0
      @[simp]
      theorem Fin.cycleRange_self {n : } (i : Fin (Nat.succ n)) :
      ↑(Fin.cycleRange i) i = 0
      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
      @[simp]
      @[simp]
      theorem Fin.cycleRange_zero' {n : } (h : 0 < n) :
      Fin.cycleRange { val := 0, isLt := h } = 1
      @[simp]
      theorem Fin.sign_cycleRange {n : } (i : Fin n) :
      Equiv.Perm.sign (Fin.cycleRange i) = (-1) ^ i
      @[simp]
      theorem Fin.succAbove_cycleRange {n : } (i : Fin n) (j : Fin n) :
      @[simp]
      theorem Fin.cycleRange_succAbove {n : } (i : Fin (n + 1)) (j : Fin n) :
      @[simp]
      theorem Fin.cycleRange_symm_zero {n : } (i : Fin (n + 1)) :
      (Fin.cycleRange i).symm 0 = i
      @[simp]
      theorem Fin.cycleRange_symm_succ {n : } (i : Fin (n + 1)) (j : Fin n) :
      theorem Fin.isCycle_cycleRange {n : } {i : Fin (n + 1)} (h0 : i 0) :
      @[simp]
      theorem Fin.cycleType_cycleRange {n : } {i : Fin (n + 1)} (h0 : i 0) :