Mathlib.GroupTheory.Perm.Fin

Equiv.Perm.decomposeFin definition

{n : ℕ} : Perm (Fin n.succ) ≃ Fin n.succ × Perm (Fin n)

Full source

/-- 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`. -/
def Equiv.Perm.decomposeFin {n : ℕ} : PermPerm (Fin n.succ) ≃ Fin n.succ × Perm (Fin n) :=
  ((Equiv.permCongr <| finSuccEquiv n).trans Equiv.Perm.decomposeOption).trans
    (Equiv.prodCongr (finSuccEquiv n).symm (Equiv.refl _))

Decomposition of permutations of `Fin (n + 1)`

Informal description

The equivalence between permutations of `Fin (n + 1)` and pairs consisting of an element of `Fin (n + 1)` and a permutation of `Fin n`. Specifically, a permutation `σ` of `Fin (n + 1)` is mapped to the pair `(σ 0, removeZero σ)`, where `removeZero σ` is the permutation of `Fin n` obtained by restricting `σ` to the remaining elements (after swapping `0` with `σ 0`). The inverse operation constructs a permutation of `Fin (n + 1)` by swapping `0` with the given element of `Fin (n + 1)` and applying the given permutation of `Fin n` to the remaining elements.

Equiv.Perm.decomposeFin_symm_of_refl theorem

{n : ℕ} (p : Fin (n + 1)) : Equiv.Perm.decomposeFin.symm (p, Equiv.refl _) = swap 0 p

Full source

@[simp]
theorem Equiv.Perm.decomposeFin_symm_of_refl {n : ℕ} (p : Fin (n + 1)) :
    Equiv.Perm.decomposeFin.symm (p, Equiv.refl _) = swap 0 p := by
  simp [Equiv.Perm.decomposeFin, Equiv.permCongr_def]

Inverse Decomposition Yields Swap for Identity Permutation

Informal description

For any natural number $n$ and any element $p \in \text{Fin}(n+1)$, the inverse of the decomposition equivalence applied to the pair $(p, \text{id})$ equals the transposition swapping $0$ and $p$, i.e., $\text{decomposeFin.symm}(p, \text{id}) = \text{swap}(0, p)$.

Equiv.Perm.decomposeFin_symm_of_one theorem

{n : ℕ} (p : Fin (n + 1)) : Equiv.Perm.decomposeFin.symm (p, 1) = swap 0 p

Full source

@[simp]
theorem Equiv.Perm.decomposeFin_symm_of_one {n : ℕ} (p : Fin (n + 1)) :
    Equiv.Perm.decomposeFin.symm (p, 1) = swap 0 p :=
  Equiv.Perm.decomposeFin_symm_of_refl p

Inverse Decomposition Yields Swap for Identity Permutation (Multiplicative Notation)

Informal description

For any natural number $n$ and any element $p \in \text{Fin}(n+1)$, the inverse of the decomposition equivalence applied to the pair $(p, 1)$ equals the transposition swapping $0$ and $p$, i.e., $\text{decomposeFin.symm}(p, 1) = \text{swap}(0, p)$.

Equiv.Perm.decomposeFin_symm_apply_zero theorem

{n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) : Equiv.Perm.decomposeFin.symm (p, e) 0 = p

Full source

@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_zero {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Equiv.Perm.decomposeFin.symm (p, e) 0 = p := by simp [Equiv.Perm.decomposeFin]

Image of Zero under Decomposed Permutation Inverse

Informal description

For any natural number $n$, element $p \in \text{Fin}(n+1)$, and permutation $e$ of $\text{Fin}(n)$, the permutation $\text{decomposeFin.symm}(p, e)$ maps $0$ to $p$.

Equiv.Perm.decomposeFin_symm_apply_succ theorem

 {n : ℕ} (e : Perm (Fin n)) (p : Fin (n + 1)) (x : Fin n) :
  Equiv.Perm.decomposeFin.symm (p, e) x.succ = swap 0 p (e x).succ

Full source

@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_succ {n : ℕ} (e : Perm (Fin n)) (p : Fin (n + 1))
    (x : Fin n) : Equiv.Perm.decomposeFin.symm (p, e) x.succ = swap 0 p (e x).succ := by
  refine Fin.cases ?_ ?_ p
  · simp [Equiv.Perm.decomposeFin, EquivFunctor.map]
  · intro i
    by_cases h : i = e x
    · simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map]
    · simp [h, Equiv.Perm.decomposeFin, EquivFunctor.map, swap_apply_def, Ne.symm h]

Image of Successor under Decomposed Permutation Inverse

Informal description

For any natural number $n$, permutation $e$ of $\text{Fin}(n)$, element $p \in \text{Fin}(n+1)$, and element $x \in \text{Fin}(n)$, the permutation $\text{decomposeFin.symm}(p, e)$ maps the successor of $x$ to the successor of $(e x)$ after swapping $0$ and $p$. That is, $\text{decomposeFin.symm}(p, e) (x + 1) = \text{swap}(0, p) (e x + 1)$.

Equiv.Perm.decomposeFin_symm_apply_one theorem

{n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) : Equiv.Perm.decomposeFin.symm (p, e) 1 = swap 0 p (e 0).succ

Full source

@[simp]
theorem Equiv.Perm.decomposeFin_symm_apply_one {n : ℕ} (e : Perm (Fin (n + 1))) (p : Fin (n + 2)) :
    Equiv.Perm.decomposeFin.symm (p, e) 1 = swap 0 p (e 0).succ := by
  rw [← Fin.succ_zero_eq_one, Equiv.Perm.decomposeFin_symm_apply_succ e p 0]

Image of One under Decomposed Permutation Inverse

Informal description

For any natural number $n$, permutation $e$ of $\text{Fin}(n+1)$, and element $p \in \text{Fin}(n+2)$, the permutation $\text{decomposeFin.symm}(p, e)$ maps $1$ to the successor of $(e 0)$ after swapping $0$ and $p$. That is, $\text{decomposeFin.symm}(p, e)(1) = \text{swap}(0, p)(e 0 + 1)$.

Equiv.Perm.decomposeFin.symm_sign theorem

 {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
  Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = ite (p = 0) 1 (-1) * Perm.sign e

Full source

@[simp]
theorem Equiv.Perm.decomposeFin.symm_sign {n : ℕ} (p : Fin (n + 1)) (e : Perm (Fin n)) :
    Perm.sign (Equiv.Perm.decomposeFin.symm (p, e)) = ite (p = 0) 1 (-1) * Perm.sign e := by
  refine Fin.cases ?_ ?_ p <;> simp [Equiv.Perm.decomposeFin]

Sign of Decomposed Permutation: $\text{sign}(\text{decomposeFin.symm}(p, e)) = (-1)^{\delta_{p0}} \cdot \text{sign}(e)$

Informal description

For any natural number $n$, element $p \in \text{Fin}(n+1)$, and permutation $e$ of $\text{Fin}(n)$, the sign of the permutation $\text{decomposeFin.symm}(p, e)$ is given by: \[ \text{sign}(\text{decomposeFin.symm}(p, e)) = \begin{cases} \text{sign}(e) & \text{if } p = 0, \\ -\text{sign}(e) & \text{otherwise}. \end{cases} \]

Finset.univ_perm_fin_succ theorem

 {n : ℕ} :
  @Finset.univ (Perm <| Fin n.succ) _ =
    (Finset.univ : Finset <| Fin n.succ × Perm (Fin n)).map Equiv.Perm.decomposeFin.symm.toEmbedding

Full source

/-- 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. -/
theorem Finset.univ_perm_fin_succ {n : ℕ} :
    @Finset.univ (Perm <| Fin n.succ) _ =
      (Finset.univ : Finset <| FinFin n.succ × Perm (Fin n)).map
        Equiv.Perm.decomposeFin.symm.toEmbedding :=
  (Finset.univ_map_equiv_to_embedding _).symm

Permutations of $\text{Fin}(n+1)$ as Augmented Permutations of $\text{Fin}(n)$

Informal description

For any natural number $n$, the set of all permutations of $\text{Fin}(n+1)$ is equal to the image of the set of all pairs $(p, \sigma)$ where $p \in \text{Fin}(n+1)$ and $\sigma$ is a permutation of $\text{Fin}(n)$, under the inverse of the decomposition equivalence $\text{decomposeFin}$.

finRotate_succ_eq_decomposeFin theorem

{n : ℕ} : finRotate n.succ = decomposeFin.symm (1, finRotate n)

Full source

theorem finRotate_succ_eq_decomposeFin {n : ℕ} :
    finRotate n.succ = decomposeFin.symm (1, finRotate n) := by
  ext i
  cases n; · simp
  refine Fin.cases ?_ (fun i => ?_) i
  · simp
  rw [coe_finRotate, decomposeFin_symm_apply_succ, if_congr i.succ_eq_last_succ rfl rfl]
  split_ifs with h
  · simp [h]
  · rw [Fin.val_succ, Function.Injective.map_swap Fin.val_injective, Fin.val_succ, coe_finRotate,
      if_neg h, Fin.val_zero, Fin.val_one,
      swap_apply_of_ne_of_ne (Nat.succ_ne_zero _) (Nat.succ_succ_ne_one _)]

Recursive Construction of `finRotate` via Permutation Decomposition

Informal description

For any natural number $n$, the permutation $\text{finRotate}(n+1)$ is equal to the inverse of the decomposition equivalence applied to the pair $(1, \text{finRotate}(n))$, i.e., $\text{finRotate}(n+1) = \text{decomposeFin.symm}(1, \text{finRotate}(n))$.

sign_finRotate theorem

(n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n

Full source

@[simp]
theorem sign_finRotate (n : ℕ) : Perm.sign (finRotate (n + 1)) = (-1) ^ n := by
  induction n with
  | zero => simp
  | succ n ih =>
    rw [finRotate_succ_eq_decomposeFin]
    simp [ih, pow_succ]

Sign of $\text{finRotate}(n+1)$ is $(-1)^n$

Informal description

For any natural number $n$, the sign of the permutation $\text{finRotate}(n+1)$ is equal to $(-1)^n$.

support_finRotate theorem

{n : ℕ} : support (finRotate (n + 2)) = Finset.univ

Full source

@[simp]
theorem support_finRotate {n : ℕ} : support (finRotate (n + 2)) = Finset.univ := by
  ext
  simp

Support of `finRotate (n + 2)` is the Entire Finite Set

Informal description

For any natural number $n$, the support of the permutation `finRotate (n + 2)` is the entire finite set of elements of its domain, i.e., $\text{support}(\text{finRotate}(n + 2)) = \text{Finset.univ}$.

support_finRotate_of_le theorem

{n : ℕ} (h : 2 ≤ n) : support (finRotate n) = Finset.univ

Full source

theorem support_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : support (finRotate n) = Finset.univ := by
  obtain ⟨m, rfl⟩ := exists_add_of_le h
  rw [add_comm, support_finRotate]

Support of $\text{finRotate}(n)$ is Entire Set for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the support of the permutation $\text{finRotate}(n)$ is the entire finite set of its domain, i.e., $\text{support}(\text{finRotate}(n)) = \text{Finset.univ}$.

isCycle_finRotate theorem

{n : ℕ} : IsCycle (finRotate (n + 2))

Full source

theorem isCycle_finRotate {n : ℕ} : IsCycle (finRotate (n + 2)) := by
  refine ⟨0, by simp, fun x hx' => ⟨x, ?_⟩⟩
  clear hx'
  obtain ⟨x, hx⟩ := x
  rw [zpow_natCast, Fin.ext_iff, Fin.val_mk]
  induction' x with x ih; · rfl
  rw [pow_succ', Perm.mul_apply, coe_finRotate_of_ne_last, ih (lt_trans x.lt_succ_self hx)]
  rw [Ne, Fin.ext_iff, ih (lt_trans x.lt_succ_self hx), Fin.val_last]
  exact ne_of_lt (Nat.lt_of_succ_lt_succ hx)

$\text{finRotate}(n + 2)$ is a cycle permutation

Informal description

For any natural number $n$, the permutation $\text{finRotate}(n + 2)$ is a cycle.

isCycle_finRotate_of_le theorem

{n : ℕ} (h : 2 ≤ n) : IsCycle (finRotate n)

Full source

theorem isCycle_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : IsCycle (finRotate n) := by
  obtain ⟨m, rfl⟩ := exists_add_of_le h
  rw [add_comm]
  exact isCycle_finRotate

$\text{finRotate}(n)$ is a cycle for $n \geq 2$

Informal description

For any natural number $n \geq 2$, the permutation $\text{finRotate}(n)$ is a cycle.

cycleType_finRotate theorem

{n : ℕ} : cycleType (finRotate (n + 2)) = {n + 2}

Full source

@[simp]
theorem cycleType_finRotate {n : ℕ} : cycleType (finRotate (n + 2)) = {n + 2} := by
  rw [isCycle_finRotate.cycleType, support_finRotate, ← Fintype.card, Fintype.card_fin]

Cycle Type of $\text{finRotate}(n + 2)$ is $\{n + 2\}$

Informal description

For any natural number $n$, the cycle type of the permutation $\text{finRotate}(n + 2)$ is the singleton multiset $\{n + 2\}$.

cycleType_finRotate_of_le theorem

{n : ℕ} (h : 2 ≤ n) : cycleType (finRotate n) = { n }

Full source

theorem cycleType_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : cycleType (finRotate n) = {n} := by
  obtain ⟨m, rfl⟩ := exists_add_of_le h
  rw [add_comm, cycleType_finRotate]

Cycle Type of $\text{finRotate}(n)$ for $n \geq 2$ is $\{n\}$

Informal description

For any natural number $n \geq 2$, the cycle type of the permutation $\text{finRotate}(n)$ is the singleton multiset $\{n\}$.

Fin.cycleRange definition

{n : ℕ} (i : Fin n) : Perm (Fin n)

Full source

/-- `Fin.cycleRange i` is the cycle `(0 1 2 ... i)` leaving `(i+1 ... (n-1))` unchanged. -/
def cycleRange {n : ℕ} (i : Fin n) : Perm (Fin n) :=
  (finRotate (i + 1)).extendDomain
    (Equiv.ofLeftInverse' (Fin.castLEEmb (Nat.succ_le_of_lt i.is_lt)) (↑)
      (by
        intro x
        ext
        simp))

Cycle permutation $ (0\ 1\ 2\ \dots\ i) $ on $ \text{Fin } n $

Informal description

For a natural number $ n $ and $ i $ in $ \text{Fin } n $, the permutation $ \text{Fin.cycleRange } i $ is the cycle $ (0\ 1\ 2\ \dots\ i) $ that leaves all elements $ j $ with $ i < j < n $ unchanged. More precisely, it is defined by extending the domain of the rotation permutation $ \text{finRotate } (i + 1) $ to $ \text{Fin } n $ via an equivalence that embeds $ \text{Fin } (i + 1) $ into $ \text{Fin } n $.

Fin.cycleRange_of_gt theorem

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

Full source

theorem cycleRange_of_gt {n : ℕ} {i j : Fin n} (h : i < j) : cycleRange i j = j := by
  rw [cycleRange, ofLeftInverse'_eq_ofInjective,
    ← Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding,
    viaFintypeEmbedding_apply_not_mem_range]
  simpa

Cycle Permutation Fixes Elements Above Index

Informal description

For any natural number $n$ and elements $i, j \in \text{Fin } n$ such that $i < j$, the permutation $\text{cycleRange } i$ leaves $j$ unchanged, i.e., $\text{cycleRange } i\ j = j$.

Fin.cycleRange_of_le theorem

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

Full source

theorem cycleRange_of_le {n : ℕ} [NeZero n] {i j : Fin n} (h : j ≤ i) :
    cycleRange i j = if j = i then 0 else j + 1 := by
  cases n
  · subsingleton
  have : j = (Fin.castLE (Nat.succ_le_of_lt i.is_lt))
    ⟨j, lt_of_le_of_lt h (Nat.lt_succ_self i)⟩ := by simp
  ext
  rw [this, cycleRange, ofLeftInverse'_eq_ofInjective, ←
    Function.Embedding.toEquivRange_eq_ofInjective, ← viaFintypeEmbedding, ← coe_castLEEmb,
    viaFintypeEmbedding_apply_image, coe_castLEEmb, coe_castLE, coe_finRotate]
  simp only [Fin.ext_iff, val_last, val_mk, val_zero, Fin.eta, castLE_mk]
  split_ifs with heq
  · rfl
  · rw [Fin.val_add_one_of_lt]
    exact lt_of_lt_of_le (lt_of_le_of_ne h (mt (congr_arg _) heq)) (le_last i)

Action of Cycle Permutation on Elements Below or Equal to Index

Informal description

For a natural number $n \neq 0$ and elements $i, j \in \text{Fin } n$ such that $j \leq i$, the permutation $\text{cycleRange } i$ maps $j$ to $0$ if $j = i$, and to $j + 1$ otherwise.

Fin.coe_cycleRange_of_le theorem

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

Full source

theorem coe_cycleRange_of_le {n : ℕ} {i j : Fin n} (h : j ≤ i) :
    (cycleRange i j : ℕ) = if j = i then 0 else (j : ℕ) + 1 := by
  rcases n with - | n
  · exact absurd le_rfl i.pos.not_le
  rw [cycleRange_of_le h]
  split_ifs with h'
  · rfl
  exact
    val_add_one_of_lt
      (calc
        (j : ℕ) < i := Fin.lt_iff_val_lt_val.mp (lt_of_le_of_ne h h')
        _ ≤ n := Nat.lt_succ_iff.mp i.2)

Natural Number Representation of Cycle Permutation on Elements Below or Equal to Index

Informal description

For any natural number $n$ and elements $i, j \in \text{Fin } n$ such that $j \leq i$, the natural number value of the permutation $\text{cycleRange } i$ applied to $j$ is $0$ if $j = i$, and $(j : \mathbb{N}) + 1$ otherwise.

Fin.cycleRange_of_lt theorem

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

Full source

theorem cycleRange_of_lt {n : ℕ} [NeZero n] {i j : Fin n} (h : j < i) : cycleRange i j = j + 1 := by
  rw [cycleRange_of_le h.le, if_neg h.ne]

Action of Cycle Permutation on Elements Below Index

Informal description

For a natural number $n \neq 0$ and elements $i, j \in \text{Fin } n$ such that $j < i$, the permutation $\text{cycleRange } i$ maps $j$ to $j + 1$.

Fin.coe_cycleRange_of_lt theorem

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

Full source

theorem coe_cycleRange_of_lt {n : ℕ} {i j : Fin n} (h : j < i) :
    (cycleRange i j : ℕ) = j + 1 := by rw [coe_cycleRange_of_le h.le, if_neg h.ne]

Natural Number Representation of Cycle Permutation on Elements Below Index

Informal description

For any natural number $n$ and elements $i, j \in \text{Fin } n$ such that $j < i$, the natural number value of the permutation $\text{cycleRange } i$ applied to $j$ is $j + 1$.

Fin.cycleRange_of_eq theorem

{n : ℕ} [NeZero n] {i j : Fin n} (h : j = i) : cycleRange i j = 0

Full source

theorem cycleRange_of_eq {n : ℕ} [NeZero n] {i j : Fin n} (h : j = i) : cycleRange i j = 0 := by
  rw [cycleRange_of_le h.le, if_pos h]

Cycle permutation maps equal indices to zero

Informal description

For a natural number $n \neq 0$ and elements $i, j \in \text{Fin } n$ such that $j = i$, the permutation $\text{cycleRange } i$ maps $j$ to $0$.

Fin.cycleRange_self theorem

{n : ℕ} [NeZero n] (i : Fin n) : cycleRange i i = 0

Full source

@[simp]
theorem cycleRange_self {n : ℕ} [NeZero n] (i : Fin n) : cycleRange i i = 0 :=
  cycleRange_of_eq rfl

Fixed Point of Cycle Permutation: $\text{cycleRange } i\ i = 0$

Informal description

For any natural number $n \neq 0$ and any element $i \in \text{Fin } n$, the permutation $\text{cycleRange } i$ maps $i$ to $0$, i.e., $\text{cycleRange } i\ i = 0$.

Fin.cycleRange_apply theorem

{n : ℕ} [NeZero n] (i j : Fin n) : cycleRange i j = if j < i then j + 1 else if j = i then 0 else j

Full source

theorem cycleRange_apply {n : ℕ} [NeZero n] (i j : Fin n) :
    cycleRange i j = if j < i then j + 1 else if j = i then 0 else j := by
  split_ifs with h₁ h₂
  · exact cycleRange_of_lt h₁
  · exact cycleRange_of_eq h₂
  · exact cycleRange_of_gt (lt_of_le_of_ne (le_of_not_gt h₁) (Ne.symm h₂))

Action of Cycle Permutation $(0\ 1\ 2\ \dots\ i)$ on $\text{Fin } n$ Elements

Informal description

For a natural number $n \neq 0$ and elements $i, j \in \text{Fin } n$, the permutation $\text{cycleRange } i$ acts on $j$ as follows: \[ \text{cycleRange } i\ j = \begin{cases} j + 1 & \text{if } j < i, \\ 0 & \text{if } j = i, \\ j & \text{otherwise.} \end{cases} \]

Fin.cycleRange_zero theorem

(n : ℕ) [NeZero n] : cycleRange (0 : Fin n) = 1

Full source

@[simp]
theorem cycleRange_zero (n : ℕ) [NeZero n] : cycleRange (0 : Fin n) = 1 := by
  ext j
  rcases (Fin.zero_le' j).eq_or_lt with rfl | hj
  · simp
  · rw [cycleRange_of_gt hj, one_apply]

Cycle Range at Zero is Identity Permutation

Informal description

For any natural number $n \neq 0$, the cycle permutation $\text{cycleRange}$ applied to the zero element of $\text{Fin } n$ is the identity permutation, i.e., $\text{cycleRange } 0 = 1$.

Fin.cycleRange_last theorem

(n : ℕ) : cycleRange (last n) = finRotate (n + 1)

Full source

@[simp]
theorem cycleRange_last (n : ℕ) : cycleRange (last n) = finRotate (n + 1) := by
  ext i
  rw [coe_cycleRange_of_le (le_last _), coe_finRotate]

Cycle Range of Last Element Equals Rotation Permutation on $\text{Fin } (n+1)$

Informal description

For any natural number $n$, the cycle permutation $\text{cycleRange}$ applied to the last element of $\text{Fin } n$ (i.e., $i = n-1$) is equal to the rotation permutation $\text{finRotate}$ on $\text{Fin } (n+1)$. In other words, the cycle $(0\ 1\ \dots\ n-1)$ on $\text{Fin } n$ coincides with the rotation permutation on $\text{Fin } (n+1)$ when $i$ is the last element of $\text{Fin } n$.

Fin.cycleRange_mk_zero theorem

{n : ℕ} (h : 0 < n) : cycleRange ⟨0, h⟩ = 1

Full source

@[simp]
theorem cycleRange_mk_zero {n : ℕ} (h : 0 < n) : cycleRange ⟨0, h⟩ = 1 :=
  have : NeZero n := .of_pos h
  cycleRange_zero n

Cycle Range at Zero is Identity Permutation (with explicit zero element)

Informal description

For any natural number $n > 0$, the cycle permutation $\text{cycleRange}$ applied to the zero element of $\text{Fin } n$ (represented as $\langle 0, h \rangle$ where $h$ is a proof that $0 < n$) is the identity permutation, i.e., $\text{cycleRange } \langle 0, h \rangle = 1$.

Fin.sign_cycleRange theorem

{n : ℕ} (i : Fin n) : Perm.sign (cycleRange i) = (-1) ^ (i : ℕ)

Full source

@[simp]
theorem sign_cycleRange {n : ℕ} (i : Fin n) : Perm.sign (cycleRange i) = (-1) ^ (i : ℕ) := by
  simp [cycleRange]

Sign of the Cycle Permutation $(0\ 1\ \dots\ i)$ is $(-1)^i$

Informal description

For any natural number $n$ and any element $i \in \text{Fin } n$, the sign of the cycle permutation $\text{cycleRange } i = (0\ 1\ 2\ \dots\ i)$ is equal to $(-1)^i$. In other words, $\text{sign}(\text{cycleRange } i) = (-1)^i$.

Fin.succAbove_cycleRange theorem

{n : ℕ} (i j : Fin n) : i.succ.succAbove (i.cycleRange j) = swap 0 i.succ j.succ

Full source

@[simp]
theorem succAbove_cycleRange {n : ℕ} (i j : Fin n) :
    i.succ.succAbove (i.cycleRange j) = swap 0 i.succ j.succ := by
  cases n
  · rcases j with ⟨_, ⟨⟩⟩
  rcases lt_trichotomy j i with (hlt | heq | hgt)
  · have : castSucc (j + 1) = j.succ := by
      ext
      rw [coe_castSucc, val_succ, Fin.val_add_one_of_lt (lt_of_lt_of_le hlt i.le_last)]
    rw [Fin.cycleRange_of_lt hlt, Fin.succAbove_of_castSucc_lt, this, swap_apply_of_ne_of_ne]
    · apply Fin.succ_ne_zero
    · exact (Fin.succ_injective _).ne hlt.ne
    · rw [Fin.lt_iff_val_lt_val]
      simpa [this] using hlt
  · rw [heq, Fin.cycleRange_self, Fin.succAbove_of_castSucc_lt, swap_apply_right, Fin.castSucc_zero]
    · rw [Fin.castSucc_zero]
      apply Fin.succ_pos
  · rw [Fin.cycleRange_of_gt hgt, Fin.succAbove_of_le_castSucc, swap_apply_of_ne_of_ne]
    · apply Fin.succ_ne_zero
    · apply (Fin.succ_injective _).ne hgt.ne.symm
    · simpa [Fin.le_iff_val_le_val] using hgt

Interaction between Cycle Permutation and Successor-Above Operation

Informal description

For any natural number $n$ and elements $i, j \in \text{Fin } n$, applying the successor-above operation at $i+1$ to the result of the cycle permutation $\text{cycleRange } i$ applied to $j$ is equal to swapping $0$ and $i+1$ applied to $j+1$, i.e., \[ (i+1).\text{succAbove}(\text{cycleRange } i\ j) = \text{swap } 0\ (i+1)\ (j+1). \]

Fin.cycleRange_succAbove theorem

{n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.cycleRange (i.succAbove j) = j.succ

Full source

@[simp]
theorem cycleRange_succAbove {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    i.cycleRange (i.succAbove j) = j.succ := by
  rcases lt_or_ge (castSucc j) i with h | h
  · rw [Fin.succAbove_of_castSucc_lt _ _ h, Fin.cycleRange_of_lt h, Fin.coeSucc_eq_succ]
  · rw [Fin.succAbove_of_le_castSucc _ _ h, Fin.cycleRange_of_gt (Fin.le_castSucc_iff.mp h)]

Action of Cycle Permutation on Successor Above Element: $\text{cycleRange } i (\text{succAbove } i\ j) = \text{succ } j$

Informal description

For any natural number $n$ and elements $i \in \text{Fin } (n + 1)$, $j \in \text{Fin } n$, the permutation $\text{cycleRange } i$ maps the element $\text{succAbove } i\ j$ to $\text{succ } j$.

Fin.cycleRange_symm_zero theorem

{n : ℕ} [NeZero n] (i : Fin n) : i.cycleRange.symm 0 = i

Full source

@[simp]
theorem cycleRange_symm_zero {n : ℕ} [NeZero n] (i : Fin n) : i.cycleRange.symm 0 = i :=
  i.cycleRange.injective (by simp)

Inverse Cycle Permutation Maps Zero Back: $(\text{cycleRange } i)^{-1}(0) = i$

Informal description

For any natural number $n \neq 0$ and any element $i \in \text{Fin } n$, the inverse of the cycle permutation $\text{cycleRange } i$ maps $0$ back to $i$, i.e., $(\text{cycleRange } i)^{-1}(0) = i$.

Fin.cycleRange_symm_succ theorem

{n : ℕ} (i : Fin (n + 1)) (j : Fin n) : i.cycleRange.symm j.succ = i.succAbove j

Full source

@[simp]
theorem cycleRange_symm_succ {n : ℕ} (i : Fin (n + 1)) (j : Fin n) :
    i.cycleRange.symm j.succ = i.succAbove j :=
  i.cycleRange.injective (by simp)

Inverse Cycle Permutation Maps Successor to Successor Above: $(0\ 1\ 2\ \dots\ i)^{-1}(j + 1) = \text{succAbove } i\ j$

Informal description

For any natural number $n$, element $i \in \text{Fin } (n + 1)$, and element $j \in \text{Fin } n$, the inverse of the cycle permutation $\text{cycleRange } i$ maps the successor of $j$ to $\text{succAbove } i\ j$. In other words, $(0\ 1\ 2\ \dots\ i)^{-1}(j + 1) = \text{succAbove } i\ j$.

Fin.isCycle_cycleRange theorem

{n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) : IsCycle (cycleRange i)

Full source

theorem isCycle_cycleRange {n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) :
    IsCycle (cycleRange i) := by
  obtain ⟨i, hi⟩ := i
  cases i
  · exact (h0 rfl).elim
  exact isCycle_finRotate.extendDomain _

Cycle Property of $\text{cycleRange } i$ for Nonzero $i$ in $\text{Fin } n$

Informal description

For any natural number $n$ with $n \neq 0$ and any nonzero element $i$ of $\text{Fin } n$ (i.e., $i \neq 0$), the permutation $\text{cycleRange } i$ is a cycle.

Fin.cycleType_cycleRange theorem

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

Full source

@[simp]
theorem cycleType_cycleRange {n : ℕ} [NeZero n] {i : Fin n} (h0 : i ≠ 0) :
    cycleType (cycleRange i) = {(i + 1 : ℕ)} := by
  obtain ⟨i, hi⟩ := i
  cases i
  · exact (h0 rfl).elim
  rw [cycleRange, cycleType_extendDomain]
  exact cycleType_finRotate

Cycle Type of $(0\ 1\ 2\ \dots\ i)$ is $\{i + 1\}$

Informal description

For any natural number $n$ with $n \neq 0$ and any nonzero element $i$ of $\text{Fin } n$ (i.e., $i \neq 0$), the cycle type of the permutation $\text{cycleRange } i$ is the singleton multiset $\{i + 1\}$.

Fin.isThreeCycle_cycleRange_two theorem

{n : ℕ} : IsThreeCycle (cycleRange 2 : Perm (Fin (n + 3)))

Full source

theorem isThreeCycle_cycleRange_two {n : ℕ} : IsThreeCycle (cycleRange 2 : Perm (Fin (n + 3))) := by
  rw [IsThreeCycle, cycleType_cycleRange] <;> simp [Fin.ext_iff]

$\text{cycleRange } 2$ is a three-cycle on $\text{Fin } (n + 3)$

Informal description

For any natural number $n$, the permutation $\text{cycleRange } 2$ on $\text{Fin } (n + 3)$ is a three-cycle, i.e., its cycle type is $\{3\}$.

Equiv.Perm.sign_eq_prod_prod_Iio theorem

(σ : Equiv.Perm (Fin n)) : σ.sign = ∏ j, ∏ i ∈ Finset.Iio j, (if σ i < σ j then 1 else -1)

Full source

theorem Equiv.Perm.sign_eq_prod_prod_Iio (σ : Equiv.Perm (Fin n)) :
    σ.sign = ∏ j, ∏ i ∈ Finset.Iio j, (if σ i < σ j then 1 else -1) := by
  suffices h : σ.sign = σ.signAux by
    rw [h, Finset.prod_sigma', Equiv.Perm.signAux]
    convert rfl using 2 with x hx
    · simp [Finset.ext_iff, Equiv.Perm.mem_finPairsLT]
    simp [not_lt, ← ite_not (p := _ ≤ _)]
  refine σ.swap_induction_on (by simp) fun π i j hne h_eq ↦ ?_
  rw [Equiv.Perm.signAux_mul, Equiv.Perm.sign_mul, h_eq, Equiv.Perm.sign_swap hne,
    Equiv.Perm.signAux_swap hne]

Sign of Permutation as Product over Inversion Pairs: $\text{sign}(\sigma) = \prod_{i

Informal description

For any permutation $\sigma$ of the finite set $\{0, 1, \dots, n-1\}$, the sign of $\sigma$ is equal to the product over all pairs $(i, j)$ with $i < j$ of $1$ if $\sigma(i) < \sigma(j)$ and $-1$ otherwise. More precisely, the sign is given by: \[ \text{sign}(\sigma) = \prod_{j=0}^{n-1} \prod_{\substack{i=0 \\ i < j}}^{n-1} \begin{cases} 1 & \text{if } \sigma(i) < \sigma(j) \\ -1 & \text{otherwise} \end{cases} \]

Equiv.Perm.sign_eq_prod_prod_Ioi theorem

(σ : Equiv.Perm (Fin n)) : σ.sign = ∏ i, ∏ j ∈ Finset.Ioi i, (if σ i < σ j then 1 else -1)

Full source

theorem Equiv.Perm.sign_eq_prod_prod_Ioi (σ : Equiv.Perm (Fin n)) :
    σ.sign = ∏ i, ∏ j ∈ Finset.Ioi i, (if σ i < σ j then 1 else -1) := by
  rw [σ.sign_eq_prod_prod_Iio]
  apply Finset.prod_comm' (by simp)

Sign of Permutation as Product over Ordered Pairs: $\text{sign}(\sigma) = \prod_{i

Informal description

For any permutation $\sigma$ of the finite set $\{0, 1, \dots, n-1\}$, the sign of $\sigma$ is equal to the product over all pairs $(i, j)$ with $i < j$ of $1$ if $\sigma(i) < \sigma(j)$ and $-1$ otherwise. More precisely, the sign is given by: \[ \text{sign}(\sigma) = \prod_{i=0}^{n-1} \prod_{\substack{j=i+1 \\ j < n}}^{n-1} \begin{cases} 1 & \text{if } \sigma(i) < \sigma(j) \\ -1 & \text{otherwise} \end{cases} \]

Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod theorem

 {R : Type*} [CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ i j, f i j = -f j i) :
  ∏ j, ∏ i ∈ Finset.Iio j, f (σ i) (σ j) = σ.sign * ∏ j, ∏ i ∈ Finset.Iio j, f i j

Full source

theorem Equiv.Perm.prod_Iio_comp_eq_sign_mul_prod {R : Type*} [CommRing R]
    (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ i j, f i j = -f j i) :
    ∏ j, ∏ i ∈ Finset.Iio j, f (σ i) (σ j) = σ.sign * ∏ j, ∏ i ∈ Finset.Iio j, f i j := by
  simp_rw [← σ.sign_inv, σ⁻¹.sign_eq_prod_prod_Iio, Finset.prod_sigma', Units.coe_prod,
    Int.cast_prod, ← Finset.prod_mul_distrib]
  set D := (Finset.univ : Finset (Fin n)).sigma Finset.Iio with hD
  have hφD : D.image (fun x ↦ ⟨σ x.1 ⊔ σ x.2, σ x.1 ⊓ σ x.2⟩) = D := by
    ext ⟨x1, x2⟩
    suffices (∃ a, ∃ b < a, σ a ⊔ σ b = x1 ∧ σ a ⊓ σ b = x2) ↔ x2 < x1 by simpa [hD]
    refine ⟨?_, fun hlt ↦ ?_⟩
    · rintro ⟨i, j, hij, rfl, rfl⟩
      exact inf_le_sup.lt_of_ne <| by simp [hij.ne.symm]
    obtain hlt' | hle := lt_or_le (σ.symm x1) (σ.symm x2)
    · exact ⟨_, _, hlt', by simp [hlt.le]⟩
    exact ⟨_, _, hle.lt_of_ne (by simp [hlt.ne]), by simp [hlt.le]⟩
  nth_rw 2 [← hφD]
  rw [Finset.prod_image fun x hx y hy ↦ Finset.injOn_of_card_image_eq (by rw [hφD]) hx hy]
  refine Finset.prod_congr rfl fun ⟨x₁, x₂⟩ hx ↦ ?_
  replace hx : x₂ < x₁ := by simpa [hD] using hx
  obtain hlt | hle := lt_or_le (σ x₁) (σ x₂)
  · simp [inf_eq_left.2 hlt.le, sup_eq_right.2 hlt.le, hx.not_lt, ← hf]
  simp [inf_eq_right.2 hle, sup_eq_left.2 hle, hx]

Permutation Sign and Antisymmetric Product Relation: $\prod_{i

Informal description

Let $R$ be a commutative ring and $\sigma$ be a permutation of $\text{Fin } n$. For any antisymmetric function $f : \text{Fin } n \to \text{Fin } n \to R$ (i.e., $f(i,j) = -f(j,i)$ for all $i,j$), we have: \[ \prod_{j=0}^{n-1} \prod_{\substack{i=0 \\ i < j}}^{n-1} f(\sigma(i), \sigma(j)) = \text{sign}(\sigma) \cdot \prod_{j=0}^{n-1} \prod_{\substack{i=0 \\ i < j}}^{n-1} f(i,j) \]

Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod theorem

 {R : Type*} [CommRing R] (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ i j, f i j = -f j i) :
  ∏ i, ∏ j ∈ Finset.Ioi i, f (σ i) (σ j) = σ.sign * ∏ i, ∏ j ∈ Finset.Ioi i, f i j

Full source

theorem Equiv.Perm.prod_Ioi_comp_eq_sign_mul_prod {R : Type*} [CommRing R]
    (σ : Equiv.Perm (Fin n)) {f : Fin n → Fin n → R} (hf : ∀ i j, f i j = -f j i) :
    ∏ i, ∏ j ∈ Finset.Ioi i, f (σ i) (σ j) = σ.sign * ∏ i, ∏ j ∈ Finset.Ioi i, f i j := by
  convert σ.prod_Iio_comp_eq_sign_mul_prod hf using 1
  · apply Finset.prod_comm' (by simp)
  convert rfl using 2
  apply Finset.prod_comm' (by simp)

Permutation Sign and Antisymmetric Product Relation: $\prod_{i

Informal description

Let $R$ be a commutative ring and $\sigma$ be a permutation of the finite set $\{0, 1, \dots, n-1\}$. For any antisymmetric function $f : \{0, 1, \dots, n-1\} \times \{0, 1, \dots, n-1\} \to R$ (i.e., $f(i,j) = -f(j,i)$ for all $i,j$), we have: \[ \prod_{i=0}^{n-1} \prod_{\substack{j=i+1 \\ j < n}}^{n-1} f(\sigma(i), \sigma(j)) = \text{sign}(\sigma) \cdot \prod_{i=0}^{n-1} \prod_{\substack{j=i+1 \\ j < n}}^{n-1} f(i,j) \]