Documentation

KoszulComplex.cycleIcc

Main Definitions and Results #

source
def natAdd_castLEEmb {n : ℕ} (m : ℕ) (hmn : n ≤ m) :
Fin n ↪ Fin m

Fin.natAdd_castLEEmb as an Embedding from Fin n to Fin m, natAdd_castLEEmb m hmn i adds m - n to i, generalizes addNatEmb.

Equations
Instances For
    source
    @[simp]
    theorem natAdd_castLEEmb_apply_val {n : ℕ} (m : ℕ) (hmn : n ≤ m) (a✝ : Fin n) :
    ↑((natAdd_castLEEmb m hmn) a✝) = ↑a✝ + (m - n)
    source
    @[simp]
    theorem natAdd_castLEEmb_apply {n m : ℕ} (hmn : n ≤ m) (k : Fin n) :
    ↑((natAdd_castLEEmb m hmn) k) = ↑k + (m - n)
    source
    @[simp]
    theorem range_natAdd_castLEEmb {n m : ℕ} (hmn : n ≤ m) :
    Set.range ⇑(natAdd_castLEEmb m hmn) = {i : Fin m | m - n ≤ ↑i}
    source
    def cycleIcc {n : ℕ} {i j : Fin n} (hij : i ≤ j) :
    Equiv.Perm (Fin n)

    cycleIcc i j hij is the cycle (i i+1 .... j) leaving (0 ... i-1) and (j+1 ... n-1) unchanged.

    Equations
    Instances For
      source
      theorem cycleIcc_of_gt {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (h : k < i) :
      (cycleIcc hij) k = k
      source
      @[simp]
      theorem cycleIcc_of_le {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (h : j < k) :
      (cycleIcc hij) k = k
      source
      instance instNeZeroNatHSubVal_koszulComplex {n : ℕ} {i : Fin n} :
      NeZero (n - ↑i)
      source
      @[simp]
      theorem Fin.val_add_one_of_lt' {n : ℕ} [NeZero n] {i j : Fin n} (hij : i < j) :
      ↑(i + 1) = ↑i + 1
      source
      @[simp]
      theorem cycleIcc_of {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (h1 : i ≤ k) (h2 : k ≤ j) [NeZero n] :
      (cycleIcc hij) k = if k = j then i else k + 1
      source
      @[simp]
      theorem cycleIcc_of_lt {n : ℕ} {i j k : Fin n} (hij : i ≤ j) (h1 : i ≤ k) (h2 : k < j) [NeZero n] :
      (cycleIcc hij) k = k + 1
      source
      @[simp]
      theorem cycleIcc_of_eq {n : ℕ} {i j : Fin n} (hij : i ≤ j) [NeZero n] :
      (cycleIcc hij) j = i
      source
      @[simp]
      theorem sign_cycleIcc {n : ℕ} {i j : Fin n} (hij : i ≤ j) :
      Equiv.Perm.sign (cycleIcc hij) = (-1) ^ (↑j - ↑i)
      source
      theorem isCycle_cycleIcc {n : ℕ} {i j : Fin n} (hij : i < j) :
      (cycleIcc ⋯).IsCycle
      source
      theorem cycleType_cycleIcc {n : ℕ} {i j : Fin n} (hij : i < j) :
      (cycleIcc ⋯).cycleType = {↑j - ↑i + 1}