doc-next-gen

Mathlib.GroupTheory.Perm.Sign

Module docstring

{"# Sign of a permutation

The main definition of this file is Equiv.Perm.sign, associating a ℤˣ sign with a permutation.

Other lemmas have been moved to Mathlib.GroupTheory.Perm.Fintype

"}

Equiv.Perm.modSwap definition
(i j : α) : Setoid (Perm α)
Full source 
/-- `modSwap i j` contains permutations up to swapping `i` and `j`.

We use this to partition permutations in `Matrix.det_zero_of_row_eq`, such that each partition
sums up to `0`.
-/
def modSwap (i j : α) : Setoid (Perm α) :=
  ⟨fun σ τ => σ = τ ∨ σ = swap i j * τ, fun σ => Or.inl (refl σ), fun {σ τ} h =>
    Or.casesOn h (fun h => Or.inl h.symm) fun h => Or.inr (by rw [h, swap_mul_self_mul]),
    fun {σ τ υ} hστ hτυ => by
    rcases hστ with hστ | hστ <;> rcases hτυ with hτυ | hτυ <;>
      (try rw [hστ, hτυ, swap_mul_self_mul]) <;>
      simp [hστ, hτυ]⟩
Equivalence relation modulo transposition of \(i\) and \(j\)
Informal description
For elements \(i\) and \(j\) of type \(\alpha\), the equivalence relation `modSwap i j` on permutations of \(\alpha\) identifies two permutations \(\sigma\) and \(\tau\) if they are either equal or related by composition with the transposition \((i\ j)\), i.e., \(\sigma = \tau\) or \(\sigma = (i\ j) \circ \tau\). This equivalence relation is reflexive, symmetric, and transitive, forming a setoid on the group of permutations of \(\alpha\).
Equiv.Perm.instDecidableRelROfFintype instance
{α : Type*} [Fintype α] [DecidableEq α] (i j : α) : DecidableRel (modSwap i j).r
Full source 
noncomputable instance {α : Type*} [Fintype α] [DecidableEq α] (i j : α) :
    DecidableRel (modSwap i j).r :=
  fun _ _ => inferInstanceAs (Decidable (_ ∨ _))
Decidability of Permutation Equivalence Modulo Transposition
Informal description
For any finite type $\alpha$ with decidable equality and any elements $i, j \in \alpha$, the equivalence relation `modSwap i j` on permutations of $\alpha$ is decidable. This means that given two permutations $\sigma$ and $\tau$, we can algorithmically determine whether they are equivalent under the relation that identifies them if they are equal or differ by composition with the transposition $(i\ j)$.
Equiv.Perm.swapFactorsAux definition
: ∀ (l : List α) (f : Perm α), (∀ {x}, f x ≠ x → x ∈ l) → { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g }
Full source 
/-- Given a list `l : List α` and a permutation `f : Perm α` such that the nonfixed points of `f`
  are in `l`, recursively factors `f` as a product of transpositions. -/
def swapFactorsAux :
    ∀ (l : List α) (f : Perm α),
      (∀ {x}, f x ≠ x → x ∈ l) → { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g }
  | [] => fun f h =>
    ⟨[],
      Equiv.ext fun x => by
        rw [List.prod_nil]
        exact (Classical.not_not.1 (mt h List.not_mem_nil)).symm,
      by simp⟩
  | x::l => fun f h =>
    if hfx : x = f x then
      swapFactorsAux l f fun {y} hy =>
        List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h hy)
    else
      let m :=
        swapFactorsAux l (swap x (f x) * f) fun {y} hy =>
          have : f y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
          List.mem_of_ne_of_mem this.2 (h this.1)
      ⟨swap x (f x)::m.1, by
        rw [List.prod_cons, m.2.1, ← mul_assoc, mul_def (swap x (f x)), swap_swap, ← one_def,
          one_mul],
        fun {_} hg => ((List.mem_cons).1 hg).elim (fun h => ⟨x, f x, hfx, h⟩) (m.2.2 _)⟩
Factorization of a permutation into transpositions
Informal description
Given a list `l` of elements of type `α` and a permutation `f` of `α` such that all non-fixed points of `f` are in `l`, the function recursively factors `f` as a product of transpositions. Specifically, it returns a list of transpositions whose product is `f`, and each element in the list is a transposition. More formally, for any list `l : List α` and permutation `f : Perm α` satisfying the condition that for every `x`, if `f x ≠ x` then `x ∈ l`, the function returns a pair consisting of: 1. A list `l' : List (Perm α)` such that the product of the elements in `l'` equals `f`. 2. A proof that every element in `l'` is a transposition (i.e., of the form `swap x y` for some `x ≠ y`).
Equiv.Perm.swapFactors definition
[Fintype α] [LinearOrder α] (f : Perm α) : { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g }
Full source 
/-- `swapFactors` represents a permutation as a product of a list of transpositions.
The representation is non unique and depends on the linear order structure.
For types without linear order `truncSwapFactors` can be used. -/
def swapFactors [Fintype α] [LinearOrder α] (f : Perm α) :
    { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g } :=
  swapFactorsAux ((@univ α _).sort (· ≤ ·)) f fun {_ _} => (mem_sort _).2 (mem_univ _)
Factorization of a permutation into transpositions (with linear order)
Informal description
Given a finite type $\alpha$ with a linear order and a permutation $f$ of $\alpha$, the function `swapFactors` returns a list of transpositions (swaps of two elements) whose product is equal to $f$. More precisely, it returns a pair consisting of: 1. A list $l$ of transpositions such that the product of the elements in $l$ equals $f$. 2. A proof that every element in $l$ is a transposition (i.e., of the form $\text{swap } x y$ for some $x \neq y$). The representation depends on the linear order structure of $\alpha$.
Equiv.Perm.truncSwapFactors definition
[Fintype α] (f : Perm α) : Trunc { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g }
Full source 
/-- This computably represents the fact that any permutation can be represented as the product of
  a list of transpositions. -/
def truncSwapFactors [Fintype α] (f : Perm α) :
    Trunc { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, IsSwap g } :=
  Quotient.recOnSubsingleton (@univ α _).1 (fun l h => Trunc.mk (swapFactorsAux l f (h _)))
    (show ∀ x, f x ≠ x → x ∈ (@univ α _).1 from fun _ _ => mem_univ _)
Truncated transposition factorization of a permutation
Informal description
Given a finite type $\alpha$ and a permutation $f$ of $\alpha$, the function returns a truncated (i.e., quotient) version of a factorization of $f$ into a product of transpositions. Specifically, it returns a truncated pair consisting of: 1. A list of transpositions whose product equals $f$. 2. A proof that every element in the list is a transposition (i.e., of the form $\text{swap } x y$ for some $x \neq y$). The factorization is constructed using the auxiliary function `swapFactorsAux` applied to the universal list of elements of $\alpha$.
Equiv.Perm.swap_induction_on theorem
[Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1) (swap_mul : ∀ f x y, x ≠ y → motive f → motive (swap x y * f)) : motive f
Full source 
/-- An induction principle for permutations. If `P` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `P` holds for all permutations. -/
@[elab_as_elim]
theorem swap_induction_on [Finite α] {motive : Perm α → Prop} (f : Perm α)
    (one : motive 1) (swap_mul : ∀ f x y, x ≠ y → motive f → motive (swap x y * f)) : motive f := by
  cases nonempty_fintype α
  obtain ⟨l, hl⟩ := (truncSwapFactors f).out
  induction l generalizing f with
  | nil =>
    simp only [one, hl.left.symm, List.prod_nil, forall_true_iff]
  | cons g l ih =>
    rcases hl.2 g (by simp) with ⟨x, y, hxy⟩
    rw [← hl.1, List.prod_cons, hxy.2]
    exact swap_mul _ _ _ hxy.1 (ih _ ⟨rfl, fun v hv => hl.2 _ (List.mem_cons_of_mem _ hv)⟩)
Induction Principle for Permutations via Transpositions
Informal description
Let $\alpha$ be a finite type and $P$ be a property of permutations of $\alpha$. If $P$ holds for the identity permutation, and for any permutation $f$ and distinct elements $x, y \in \alpha$, $P(f)$ implies $P(\text{swap}(x, y) \circ f)$, then $P$ holds for all permutations of $\alpha$.
Equiv.Perm.mclosure_isSwap theorem
[Finite α] : Submonoid.closure {σ : Perm α | IsSwap σ} = ⊤
Full source 
theorem mclosure_isSwap [Finite α] : Submonoid.closure { σ : Perm α | IsSwap σ } = ⊤ := by
  cases nonempty_fintype α
  refine top_unique fun x _ ↦ ?_
  obtain ⟨h1, h2⟩ := Subtype.mem (truncSwapFactors x).out
  rw [← h1]
  exact Submonoid.list_prod_mem _ fun y hy ↦ Submonoid.subset_closure (h2 y hy)
Transpositions Generate the Permutation Monoid for Finite Types
Informal description
For any finite type $\alpha$, the submonoid generated by the set of transpositions (permutations that swap two distinct elements) is equal to the entire monoid of permutations of $\alpha$.
Equiv.Perm.closure_isSwap theorem
[Finite α] : Subgroup.closure {σ : Perm α | IsSwap σ} = ⊤
Full source 
theorem closure_isSwap [Finite α] : Subgroup.closure { σ : Perm α | IsSwap σ } = ⊤ :=
  Subgroup.closure_eq_top_of_mclosure_eq_top mclosure_isSwap
Transpositions Generate the Permutation Group for Finite Types
Informal description
For any finite type $\alpha$, the subgroup generated by the set of all transpositions (permutations that swap two distinct elements) is equal to the entire group of permutations of $\alpha$.
Equiv.Perm.mclosure_swap_castSucc_succ theorem
(n : ℕ) : Submonoid.closure (Set.range fun i : Fin n ↦ swap i.castSucc i.succ) = ⊤
Full source 
/-- Every finite symmetric group is generated by transpositions of adjacent elements. -/
theorem mclosure_swap_castSucc_succ (n : ℕ) :
    Submonoid.closure (Set.range fun i : Fin n ↦ swap i.castSucc i.succ) = ⊤ := by
  apply top_unique
  rw [← mclosure_isSwap, Submonoid.closure_le]
  rintro _ ⟨i, j, ne, rfl⟩
  wlog lt : i < j generalizing i j
  · rw [swap_comm]; exact this _ _ ne.symm (ne.lt_or_lt.resolve_left lt)
  induction' j using Fin.induction with j ih
  · cases lt
  have mem : swapswap j.castSucc j.succ ∈ Submonoid.closure
      (Set.range fun (i : Fin n) ↦ swap i.castSucc i.succ) := Submonoid.subset_closure ⟨_, rfl⟩
  obtain rfl | lts := (Fin.le_castSucc_iff.mpr lt).eq_or_lt
  · exact mem
  rw [swap_comm, ← swap_mul_swap_mul_swap (y := Fin.castSucc j) lts.ne lt.ne]
  exact mul_mem (mul_mem mem <| ih lts.ne lts) mem
Adjacent Transpositions Generate the Permutation Monoid on $\text{Fin } n$
Informal description
For any natural number $n$, the submonoid generated by the set of transpositions of adjacent elements in $\text{Fin } n$ (i.e., permutations that swap $i$ and $i+1$ for $i \in \text{Fin } n$) is equal to the entire monoid of permutations of $\text{Fin } n$.
Equiv.Perm.swap_induction_on' theorem
[Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1) (mul_swap : ∀ f x y, x ≠ y → motive f → motive (f * swap x y)) : motive f
Full source 
/-- Like `swap_induction_on`, but with the composition on the right of `f`.

An induction principle for permutations. If `motive` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `motive` holds for all permutations. -/
@[elab_as_elim]
theorem swap_induction_on' [Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1)
    (mul_swap : ∀ f x y, x ≠ y → motive f → motive (f * swap x y)) : motive f :=
  inv_inv f ▸ swap_induction_on f⁻¹ one fun f => mul_swap f⁻¹
Right Composition Induction Principle for Permutations via Transpositions
Informal description
Let $\alpha$ be a finite type and $P$ be a property of permutations of $\alpha$. If $P$ holds for the identity permutation, and for any permutation $f$ and distinct elements $x, y \in \alpha$, $P(f)$ implies $P(f \circ \text{swap}(x, y))$, then $P$ holds for all permutations of $\alpha$.
Equiv.Perm.isConj_swap theorem
{w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (swap w x) (swap y z)
Full source 
theorem isConj_swap {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (swap w x) (swap y z) :=
  isConj_iff.2
    (have h :
      ∀ {y z : α},
        y ≠ z → w ≠ z → swap w y * swap x z * swap w x * (swap w y * swap x z)⁻¹ = swap y z :=
      fun {y z} hyz hwz => by
      rw [mul_inv_rev, swap_inv, swap_inv, mul_assoc (swap w y), mul_assoc (swap w y), ←
        mul_assoc _ (swap x z), swap_mul_swap_mul_swap hwx hwz, ← mul_assoc,
        swap_mul_swap_mul_swap hwz.symm hyz.symm]
    if hwz : w = z then
      have hwy : w ≠ y := by rw [hwz]; exact hyz.symm
      ⟨swap w z * swap x y, by rw [swap_comm y z, h hyz.symm hwy]⟩
    else ⟨swap w y * swap x z, h hyz hwz⟩)
Conjugacy of Transpositions for Distinct Pairs
Informal description
For any distinct elements $w, x$ and distinct elements $y, z$ in a type $\alpha$, the transpositions $\text{swap}(w, x)$ and $\text{swap}(y, z)$ are conjugate in the permutation group of $\alpha$.
Equiv.Perm.finPairsLT definition
(n : ℕ) : Finset (Σ _ : Fin n, Fin n)
Full source 
/-- set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a -/
def finPairsLT (n : ℕ) : Finset (Σ_ : Fin n, Fin n) :=
  (univ : Finset (Fin n)).sigma fun a => (range a).attachFin fun _ hm => (mem_range.1 hm).trans a.2
Finite set of ordered pairs with second element less than first
Informal description
For a natural number \( n \), the set `finPairsLT n` consists of all pairs \((a, b)\) where \( a \) is an element of the finite type with \( n \) elements and \( b \) is an element of the same type such that \( b < a \). This is represented as a finite set of dependent pairs \((a, b)\) with the ordering constraint \( b < a \).
Equiv.Perm.mem_finPairsLT theorem
{n : ℕ} {a : Σ _ : Fin n, Fin n} : a ∈ finPairsLT n ↔ a.2 < a.1
Full source 
theorem mem_finPairsLT {n : ℕ} {a : Σ _ : Fin n, Fin n} : a ∈ finPairsLT na ∈ finPairsLT n ↔ a.2 < a.1 := by
  simp only [finPairsLT, Fin.lt_iff_val_lt_val, true_and, mem_attachFin, mem_range, mem_univ,
    mem_sigma]
Membership Criterion for Ordered Pairs in $\text{finPairsLT}\ n$
Informal description
For any natural number $n$ and any pair $a = (a_1, a_2)$ where $a_1, a_2$ are elements of $\text{Fin}\ n$, the pair $a$ belongs to the finite set $\text{finPairsLT}\ n$ if and only if $a_2 < a_1$.
Equiv.Perm.signAux definition
{n : ℕ} (a : Perm (Fin n)) : ℤˣ
Full source 
/-- `signAux σ` is the sign of a permutation on `Fin n`, defined as the parity of the number of
  pairs `(x₁, x₂)` such that `x₂ < x₁` but `σ x₁ ≤ σ x₂` -/
def signAux {n : ℕ} (a : Perm (Fin n)) : ℤℤˣ :=
  ∏ x ∈ finPairsLT n, if a x.1 ≤ a x.2 then -1 else 1
Sign of a permutation on a finite type via inversion count
Informal description
For a permutation \( \sigma \) on the finite type with \( n \) elements, the sign \( \text{signAux}(\sigma) \) is defined as the product over all pairs \( (x_1, x_2) \) with \( x_2 < x_1 \) of \( -1 \) if \( \sigma(x_1) \leq \sigma(x_2) \) and \( 1 \) otherwise. This gives the parity of the number of inversions of \( \sigma \).
Equiv.Perm.signBijAux definition
{n : ℕ} (f : Perm (Fin n)) (a : Σ _ : Fin n, Fin n) : Σ _ : Fin n, Fin n
Full source 
/-- `signBijAux f ⟨a, b⟩` returns the pair consisting of `f a` and `f b` in decreasing order. -/
def signBijAux {n : ℕ} (f : Perm (Fin n)) (a : Σ _ : Fin n, Fin n) : Σ_ : Fin n, Fin n :=
  if _ : f a.2 < f a.1 then ⟨f a.1, f a.2⟩ else ⟨f a.2, f a.1⟩
Auxiliary function for permutation sign via inversion count
Informal description
For a permutation \( f \) on the finite type with \( n \) elements and a pair \( (a, b) \) where \( a, b \) are elements of this type, the function `signBijAux` returns the pair \( (f(a), f(b)) \) if \( f(b) < f(a) \), and \( (f(b), f(a)) \) otherwise. This auxiliary function is used to define the sign of a permutation via inversion count.
Equiv.Perm.signBijAux_injOn theorem
{n : ℕ} {f : Perm (Fin n)} : (finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f)
Full source 
theorem signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} :
    (finPairsLT n : Set (Σ _, Fin n)).InjOn (signBijAux f) := by
  rintro ⟨a₁, a₂⟩ ha ⟨b₁, b₂⟩ hb h
  dsimp [signBijAux] at h
  rw [Finset.mem_coe, mem_finPairsLT] at *
  have : ¬b₁ < b₂ := hb.le.not_lt
  split_ifs at h <;>
  simp_all only [not_lt, Sigma.mk.inj_iff, (Equiv.injective f).eq_iff, heq_eq_eq]
  · exact absurd this (not_le.mpr ha)
  · exact absurd this (not_le.mpr ha)
Injectivity of $\text{signBijAux}\ f$ on $\text{finPairsLT}\ n$
Informal description
For any natural number $n$ and any permutation $f$ of the finite set $\text{Fin}\ n$, the function $\text{signBijAux}\ f$ is injective on the set $\text{finPairsLT}\ n$ of ordered pairs $(a, b)$ with $b < a$.
Equiv.Perm.signBijAux_surj theorem
{n : ℕ} {f : Perm (Fin n)} : ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, signBijAux f b = a
Full source 
theorem signBijAux_surj {n : ℕ} {f : Perm (Fin n)} :
    ∀ a ∈ finPairsLT n, ∃ b ∈ finPairsLT n, signBijAux f b = a :=
  fun ⟨a₁, a₂⟩ ha =>
    if hxa : f⁻¹ a₂ < f⁻¹ a₁ then
      ⟨⟨f⁻¹ a₁, f⁻¹ a₂⟩, mem_finPairsLT.2 hxa, by
        dsimp [signBijAux]
        rw [apply_inv_self, apply_inv_self, if_pos (mem_finPairsLT.1 ha)]⟩
    else
      ⟨⟨f⁻¹ a₂, f⁻¹ a₁⟩,
        mem_finPairsLT.2 <|
          (le_of_not_gt hxa).lt_of_ne fun h => by
            simp [mem_finPairsLT, f⁻¹.injective h, lt_irrefl] at ha, by
              dsimp [signBijAux]
              rw [apply_inv_self, apply_inv_self, if_neg (mem_finPairsLT.1 ha).le.not_lt]⟩
Surjectivity of the Sign Auxiliary Function on Ordered Pairs
Informal description
For any natural number $n$ and any permutation $f$ of the finite set $\text{Fin}\ n$, the function $\text{signBijAux}\ f$ is surjective on the set $\text{finPairsLT}\ n$ of ordered pairs $(a, b)$ with $b < a$. That is, for every pair $a \in \text{finPairsLT}\ n$, there exists a pair $b \in \text{finPairsLT}\ n$ such that $\text{signBijAux}\ f\ b = a$.
Equiv.Perm.signBijAux_mem theorem
{n : ℕ} {f : Perm (Fin n)} : ∀ a : Σ _ : Fin n, Fin n, a ∈ finPairsLT n → signBijAux f a ∈ finPairsLT n
Full source 
theorem signBijAux_mem {n : ℕ} {f : Perm (Fin n)} :
    ∀ a : Σ_ : Fin n, Fin n, a ∈ finPairsLT n → signBijAuxsignBijAux f a ∈ finPairsLT n :=
  fun ⟨a₁, a₂⟩ ha => by
    unfold signBijAux
    split_ifs with h
    · exact mem_finPairsLT.2 h
    · exact mem_finPairsLT.2
        ((le_of_not_gt h).lt_of_ne fun h => (mem_finPairsLT.1 ha).ne (f.injective h.symm))
Preservation of Ordering by $\text{signBijAux}\ f$ on $\text{finPairsLT}\ n$
Informal description
For any natural number $n$, any permutation $f$ of the finite set $\text{Fin}\ n$, and any pair $(a, b)$ in the set $\text{finPairsLT}\ n$ (i.e., pairs with $b < a$), the image of $(a, b)$ under the auxiliary function $\text{signBijAux}\ f$ is also in $\text{finPairsLT}\ n$.
Equiv.Perm.signAux_inv theorem
{n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f
Full source 
@[simp]
theorem signAux_inv {n : ℕ} (f : Perm (Fin n)) : signAux f⁻¹ = signAux f :=
  prod_nbij (signBijAux f⁻¹) signBijAux_mem signBijAux_injOn signBijAux_surj fun ⟨a, b⟩ hab ↦
    if h : f⁻¹ b < f⁻¹ a then by
      simp_all [signBijAux, dif_pos h, if_neg h.not_le, apply_inv_self, apply_inv_self,
        if_neg (mem_finPairsLT.1 hab).not_le]
    else by
      simp_all [signBijAux, if_pos (le_of_not_gt h), dif_neg h, apply_inv_self, apply_inv_self,
        if_pos (mem_finPairsLT.1 hab).le]
Sign of Inverse Permutation Equals Sign of Original Permutation
Informal description
For any natural number $n$ and any permutation $f$ of the finite set $\text{Fin}\ n$, the sign of the inverse permutation $f^{-1}$ is equal to the sign of $f$, i.e., $\text{signAux}(f^{-1}) = \text{signAux}(f)$.
Equiv.Perm.signAux_mul theorem
{n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g
Full source 
theorem signAux_mul {n : ℕ} (f g : Perm (Fin n)) : signAux (f * g) = signAux f * signAux g := by
  rw [← signAux_inv g]
  unfold signAux
  rw [← prod_mul_distrib]
  refine prod_nbij (signBijAux g) signBijAux_mem signBijAux_injOn signBijAux_surj ?_
  rintro ⟨a, b⟩ hab
  dsimp only [signBijAux]
  rw [mul_apply, mul_apply]
  rw [mem_finPairsLT] at hab
  by_cases h : g b < g a
  · rw [dif_pos h]
    simp only [not_le_of_gt hab, mul_one, mul_ite, mul_neg, Perm.inv_apply_self, if_false]
  · rw [dif_neg h, inv_apply_self, inv_apply_self, if_pos hab.le]
    by_cases h₁ : f (g b) ≤ f (g a)
    · have : f (g b) ≠ f (g a) := by
        rw [Ne, f.injective.eq_iff, g.injective.eq_iff]
        exact ne_of_lt hab
      rw [if_pos h₁, if_neg (h₁.lt_of_ne this).not_le]
      rfl
    · rw [if_neg h₁, if_pos (lt_of_not_ge h₁).le]
      rfl
Multiplicativity of Permutation Sign under Composition
Informal description
For any natural number $n$ and any two permutations $f$ and $g$ of the finite set $\{1, \dots, n\}$, the sign of the composition $f \circ g$ is equal to the product of the signs of $f$ and $g$, i.e., $\text{signAux}(f \circ g) = \text{signAux}(f) \cdot \text{signAux}(g)$.
Equiv.Perm.signAux_swap theorem
: ∀ {n : ℕ} {x y : Fin n} (_hxy : x ≠ y), signAux (swap x y) = -1
Full source 
theorem signAux_swap : ∀ {n : ℕ} {x y : Fin n} (_hxy : x ≠ y), signAux (swap x y) = -1
  | 0, x, y => by intro; exact Fin.elim0 x
  | 1, x, y => by
    dsimp [signAux, swap, swapCore]
    simp only [eq_iff_true_of_subsingleton, not_true, ite_true, le_refl, prod_const,
               IsEmpty.forall_iff]
  | n + 2, x, y => fun hxy => by
    have h2n : 2 ≤ n + 2 := by exact le_add_self
    rw [← isConj_iff_eq, ← signAux_swap_zero_one h2n]
    exact (MonoidHom.mk' signAux signAux_mul).map_isConj
      (isConj_swap hxy (by exact of_decide_eq_true rfl))
Sign of a Transposition is $-1$
Informal description
For any natural number $n$ and any two distinct elements $x, y$ in the finite set $\{1, \dots, n\}$, the sign of the transposition swapping $x$ and $y$ is $-1$, i.e., $\text{signAux}(\text{swap } x y) = -1$.
Equiv.Perm.signAux2 definition
: List α → Perm α → ℤˣ
Full source 
/-- When the list `l : List α` contains all nonfixed points of the permutation `f : Perm α`,
  `signAux2 l f` recursively calculates the sign of `f`. -/
def signAux2 : List α → Perm α → ℤℤˣ
  | [], _ => 1
  | x::l, f => if x = f x then signAux2 l f else -signAux2 l (swap x (f x) * f)
Recursive sign computation for permutations
Informal description
Given a list `l : List α` containing all non-fixed points of a permutation `f : Perm α`, the function `signAux2 l f` recursively computes the sign of `f` as an element of `ℤˣ`. The sign is defined as follows: - If the list is empty, the sign is `1`. - For a non-empty list `x::l`, if `x` is a fixed point of `f` (i.e., `f x = x`), then the sign is the same as `signAux2 l f`. - Otherwise, the sign is `-signAux2 l (swap x (f x) * f)`, where `swap x (f x)` is the transposition swapping `x` and `f x`.
Equiv.Perm.signAux_eq_signAux2 theorem
{n : ℕ} : ∀ (l : List α) (f : Perm α) (e : α ≃ Fin n) (_h : ∀ x, f x ≠ x → x ∈ l), signAux ((e.symm.trans f).trans e) = signAux2 l f
Full source 
theorem signAux_eq_signAux2 {n : ℕ} :
    ∀ (l : List α) (f : Perm α) (e : α ≃ Fin n) (_h : ∀ x, f x ≠ x → x ∈ l),
      signAux ((e.symm.trans f).trans e) = signAux2 l f
  | [], f, e, h => by
    have : f = 1 := Equiv.ext fun y => Classical.not_not.1 (mt (h y) List.not_mem_nil)
    rw [this, one_def, Equiv.trans_refl, Equiv.symm_trans_self, ← one_def, signAux_one, signAux2]
  | x::l, f, e, h => by
    rw [signAux2]
    by_cases hfx : x = f x
    · rw [if_pos hfx]
      exact
        signAux_eq_signAux2 l f _ fun y (hy : f y ≠ y) =>
          List.mem_of_ne_of_mem (fun h : y = x => by simp [h, hfx.symm] at hy) (h y hy)
    · have hy : ∀ y : α, (swap x (f x) * f) y ≠ y → y ∈ l := fun y hy =>
        have : f y ≠ yf y ≠ y ∧ y ≠ x := ne_and_ne_of_swap_mul_apply_ne_self hy
        List.mem_of_ne_of_mem this.2 (h _ this.1)
      have : (e.symm.trans (swap x (f x) * f)).trans e =
          swap (e x) (e (f x)) * (e.symm.trans f).trans e := by
        ext
        rw [← Equiv.symm_trans_swap_trans, mul_def, Equiv.symm_trans_swap_trans, mul_def]
        repeat (rw [trans_apply])
        simp [swap, swapCore]
        split_ifs <;> rfl
      have hefx : e x ≠ e (f x) := mt e.injective.eq_iff.1 hfx
      rw [if_neg hfx, ← signAux_eq_signAux2 _ _ e hy, this, signAux_mul, signAux_swap hefx]
      simp only [neg_neg, one_mul, neg_mul]
Equivalence of Sign Computations for Permutations via List and Inversion Count
Informal description
For any natural number $n$, list $l$ of elements of type $\alpha$, permutation $f$ of $\alpha$, and equivalence $e : \alpha \simeq \text{Fin}\ n$ such that every non-fixed point of $f$ is in $l$, the sign of the permutation $e^{-1} \circ f \circ e$ on $\text{Fin}\ n$ (computed via inversion count) is equal to the recursively computed sign of $f$ with respect to $l$.
Equiv.Perm.signAux3 definition
[Finite α] (f : Perm α) {s : Multiset α} : (∀ x, x ∈ s) → ℤˣ
Full source 
/-- When the multiset `s : Multiset α` contains all nonfixed points of the permutation `f : Perm α`,
  `signAux2 f _` recursively calculates the sign of `f`. -/
def signAux3 [Finite α] (f : Perm α) {s : Multiset α} : (∀ x, x ∈ s) → ℤℤˣ :=
  Quotient.hrecOn s (fun l _ => signAux2 l f) fun l₁ l₂ h ↦ by
    rcases Finite.exists_equiv_fin α with ⟨n, ⟨e⟩⟩
    refine Function.hfunext (forall_congr fun _ ↦ propext h.mem_iff) fun h₁ h₂ _ ↦ ?_
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => h₁ _, ← signAux_eq_signAux2 _ _ e fun _ _ => h₂ _]
Sign of a permutation via auxiliary computation
Informal description
Given a finite type `α`, a permutation `f : Perm α`, and a multiset `s : Multiset α` containing all elements of `α`, the function `signAux3 f hs` computes the sign of `f` as an element of `ℤˣ`. The computation is performed by lifting the permutation to a list and using the recursive definition `signAux2`. The result is independent of the choice of the multiset `s` as long as it contains all elements of `α`.
Equiv.Perm.signAux3_mul_and_swap theorem
[Finite α] (f g : Perm α) (s : Multiset α) (hs : ∀ x, x ∈ s) : signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧ Pairwise fun x y => signAux3 (swap x y) hs = -1
Full source 
theorem signAux3_mul_and_swap [Finite α] (f g : Perm α) (s : Multiset α) (hs : ∀ x, x ∈ s) :
    signAux3signAux3 (f * g) hs = signAux3 f hs * signAux3 g hs ∧
      Pairwise fun x y => signAux3 (swap x y) hs = -1 := by
  obtain ⟨n, ⟨e⟩⟩ := Finite.exists_equiv_fin α
  induction s using Quotient.inductionOn with | _ l => ?_
  show
    signAux2signAux2 l (f * g) = signAux2 l f * signAux2 l g ∧
    Pairwise fun x y => signAux2 l (swap x y) = -1
  have hfg : (e.symm.trans (f * g)).trans e = (e.symm.trans f).trans e * (e.symm.trans g).trans e :=
    Equiv.ext fun h => by simp [mul_apply]
  constructor
  · rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, ←
      signAux_eq_signAux2 _ _ e fun _ _ => hs _, ← signAux_eq_signAux2 _ _ e fun _ _ => hs _,
      hfg, signAux_mul]
  · intro x y hxy
    rw [← e.injective.ne_iff] at hxy
    rw [← signAux_eq_signAux2 _ _ e fun _ _ => hs _, symm_trans_swap_trans, signAux_swap hxy]
Multiplicativity of Permutation Sign and Sign of Transpositions
Informal description
For a finite type $\alpha$, any two permutations $f$ and $g$ of $\alpha$, and a multiset $s$ containing all elements of $\alpha$, the following holds: 1. The sign of the composition $f \circ g$ is the product of the signs of $f$ and $g$, i.e., $\text{signAux3}(f \circ g) = \text{signAux3}(f) \cdot \text{signAux3}(g)$. 2. For any two distinct elements $x, y \in \alpha$, the sign of the transposition swapping $x$ and $y$ is $-1$, i.e., $\text{signAux3}(\text{swap } x y) = -1$.
Equiv.Perm.signAux3_symm_trans_trans theorem
[Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β) {s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) : signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs
Full source 
theorem signAux3_symm_trans_trans [Finite α] [DecidableEq β] [Finite β] (f : Perm α) (e : α ≃ β)
    {s : Multiset α} {t : Multiset β} (hs : ∀ x, x ∈ s) (ht : ∀ x, x ∈ t) :
    signAux3 ((e.symm.trans f).trans e) ht = signAux3 f hs := by
  induction' t, s using Quotient.inductionOn₂ with t s ht hs
  show signAux2 _ _ = signAux2 _ _
  rcases Finite.exists_equiv_fin β with ⟨n, ⟨e'⟩⟩
  rw [← signAux_eq_signAux2 _ _ e' fun _ _ => ht _,
    ← signAux_eq_signAux2 _ _ (e.trans e') fun _ _ => hs _]
  exact congr_arg signAux
    (Equiv.ext fun x => by simp [Equiv.coe_trans, apply_eq_iff_eq, symm_trans_apply])
Invariance of Permutation Sign under Conjugation by Equivalence
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $f$ be a permutation of $\alpha$. Given an equivalence $e : \alpha \simeq \beta$, multisets $s$ and $t$ containing all elements of $\alpha$ and $\beta$ respectively, the sign of the conjugated permutation $e^{-1} \circ f \circ e$ computed with respect to $t$ is equal to the sign of $f$ computed with respect to $s$. In other words, $\text{signAux3}(e^{-1} \circ f \circ e, \text{ht}) = \text{signAux3}(f, \text{hs})$, where $\text{hs}$ and $\text{ht}$ are proofs that $s$ and $t$ contain all elements of $\alpha$ and $\beta$ respectively.
Equiv.Perm.sign definition
[Fintype α] : Perm α →* ℤˣ
Full source 
/-- `SignType.sign` of a permutation returns the signature or parity of a permutation, `1` for even
permutations, `-1` for odd permutations. It is the unique surjective group homomorphism from
`Perm α` to the group with two elements. -/
def sign [Fintype α] : PermPerm α →* ℤˣ :=
  MonoidHom.mk' (fun f => signAux3 f mem_univ) fun f g => (signAux3_mul_and_swap f g _ mem_univ).1
Sign of a permutation
Informal description
The sign of a permutation $f$ of a finite type $\alpha$ is defined as the unique group homomorphism from the group of permutations $\text{Perm}(\alpha)$ to the multiplicative group of units $\mathbb{Z}^\times$, taking the value $1$ for even permutations and $-1$ for odd permutations. More precisely, for any permutation $f \in \text{Perm}(\alpha)$, $\text{sign}(f)$ is computed using an auxiliary function that lifts $f$ to a list and recursively calculates the sign based on transpositions. The result is independent of the choice of lifting.
Equiv.Perm.sign_mul theorem
(f g : Perm α) : sign (f * g) = sign f * sign g
Full source 
@[simp]
theorem sign_mul (f g : Perm α) : sign (f * g) = sign f * sign g :=
  MonoidHom.map_mul sign f g
Sign of Permutation Composition: $\text{sign}(f \circ g) = \text{sign}(f) \cdot \text{sign}(g)$
Informal description
For any two permutations $f$ and $g$ of a finite type $\alpha$, the sign of their composition $f \circ g$ is equal to the product of their signs, i.e., $\text{sign}(f \circ g) = \text{sign}(f) \cdot \text{sign}(g)$.
Equiv.Perm.sign_trans theorem
(f g : Perm α) : sign (f.trans g) = sign g * sign f
Full source 
@[simp]
theorem sign_trans (f g : Perm α) : sign (f.trans g) = sign g * sign f := by
  rw [← mul_def, sign_mul]
Sign of Permutation Composition in Reverse Order: $\text{sign}(f \circ g) = \text{sign}(g) \cdot \text{sign}(f)$
Informal description
For any two permutations $f$ and $g$ of a finite type $\alpha$, the sign of their composition $f \circ g$ is equal to the product of their signs in reverse order, i.e., $\text{sign}(f \circ g) = \text{sign}(g) \cdot \text{sign}(f)$.
Equiv.Perm.sign_one theorem
: sign (1 : Perm α) = 1
Full source 
@[simp]
theorem sign_one : sign (1 : Perm α) = 1 :=
  MonoidHom.map_one sign
Sign of the Identity Permutation is One
Informal description
The sign of the identity permutation on a finite type $\alpha$ is $1$.
Equiv.Perm.sign_refl theorem
: sign (Equiv.refl α) = 1
Full source 
@[simp]
theorem sign_refl : sign (Equiv.refl α) = 1 :=
  MonoidHom.map_one sign
Sign of Identity Permutation is One
Informal description
The sign of the identity permutation on a finite type $\alpha$ is equal to $1$, i.e., $\text{sign}(\text{id}_\alpha) = 1$.
Equiv.Perm.sign_inv theorem
(f : Perm α) : sign f⁻¹ = sign f
Full source 
@[simp]
theorem sign_inv (f : Perm α) : sign f⁻¹ = sign f := by
  rw [MonoidHom.map_inv sign f, Int.units_inv_eq_self]
Sign of Inverse Permutation Equals Sign of Original Permutation
Informal description
For any permutation $f$ of a finite type $\alpha$, the sign of the inverse permutation $f^{-1}$ is equal to the sign of $f$, i.e., $\text{sign}(f^{-1}) = \text{sign}(f)$.
Equiv.Perm.sign_symm theorem
(e : Perm α) : sign e.symm = sign e
Full source 
@[simp]
theorem sign_symm (e : Perm α) : sign e.symm = sign e :=
  sign_inv e
Sign of Inverse Permutation Equals Sign of Original Permutation
Informal description
For any permutation $e$ of a finite type $\alpha$, the sign of the inverse permutation $e^{-1}$ is equal to the sign of $e$, i.e., $\text{sign}(e^{-1}) = \text{sign}(e)$.
Equiv.Perm.sign_swap theorem
{x y : α} (h : x ≠ y) : sign (swap x y) = -1
Full source 
theorem sign_swap {x y : α} (h : x ≠ y) : sign (swap x y) = -1 :=
  (signAux3_mul_and_swap 1 1 _ mem_univ).2 h
Sign of a Transposition is $-1$
Informal description
For any two distinct elements $x$ and $y$ of a finite type $\alpha$, the sign of the transposition swapping $x$ and $y$ is $-1$, i.e., $\text{sign}(\text{swap } x y) = -1$.
Equiv.Perm.sign_swap' theorem
{x y : α} : sign (swap x y) = if x = y then 1 else -1
Full source 
@[simp]
theorem sign_swap' {x y : α} : sign (swap x y) = if x = y then 1 else -1 :=
  if H : x = y then by simp [H, swap_self] else by simp [sign_swap H, H]
Sign of Swap Permutation: $\text{sign}(\text{swap } x y) = \text{if } x = y \text{ then } 1 \text{ else } -1$
Informal description
For any two elements $x$ and $y$ of a finite type $\alpha$, the sign of the permutation swapping $x$ and $y$ is given by: \[ \text{sign}(\text{swap } x y) = \begin{cases} 1 & \text{if } x = y, \\ -1 & \text{if } x \neq y. \end{cases} \]
Equiv.Perm.IsSwap.sign_eq theorem
{f : Perm α} (h : f.IsSwap) : sign f = -1
Full source 
theorem IsSwap.sign_eq {f : Perm α} (h : f.IsSwap) : sign f = -1 :=
  let ⟨_, _, hxy⟩ := h
  hxy.2.symm ▸ sign_swap hxy.1
Sign of a Transposition is $-1$
Informal description
For any permutation $f$ of a finite type $\alpha$, if $f$ is a transposition (i.e., $f$ swaps two distinct elements of $\alpha$), then the sign of $f$ is $-1$.
Equiv.Perm.sign_symm_trans_trans theorem
[DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β) : sign ((e.symm.trans f).trans e) = sign f
Full source 
@[simp]
theorem sign_symm_trans_trans [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β) :
    sign ((e.symm.trans f).trans e) = sign f :=
  signAux3_symm_trans_trans f e mem_univ mem_univ
Invariance of Permutation Sign under Conjugation by Equivalence
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $f$ be a permutation of $\alpha$. For any equivalence $e : \alpha \simeq \beta$, the sign of the conjugated permutation $e^{-1} \circ f \circ e$ is equal to the sign of $f$, i.e., $\text{sign}(e^{-1} \circ f \circ e) = \text{sign}(f)$.
Equiv.Perm.sign_trans_trans_symm theorem
[DecidableEq β] [Fintype β] (f : Perm β) (e : α ≃ β) : sign ((e.trans f).trans e.symm) = sign f
Full source 
@[simp]
theorem sign_trans_trans_symm [DecidableEq β] [Fintype β] (f : Perm β) (e : α ≃ β) :
    sign ((e.trans f).trans e.symm) = sign f :=
  sign_symm_trans_trans f e.symm
Invariance of Permutation Sign under Conjugation by Equivalence (Symmetric Form)
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $f$ be a permutation of $\beta$. For any equivalence $e : \alpha \simeq \beta$, the sign of the conjugated permutation $e \circ f \circ e^{-1}$ is equal to the sign of $f$, i.e., $\text{sign}(e \circ f \circ e^{-1}) = \text{sign}(f)$.
Equiv.Perm.sign_prod_list_swap theorem
{l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) : sign l.prod = (-1) ^ l.length
Full source 
theorem sign_prod_list_swap {l : List (Perm α)} (hl : ∀ g ∈ l, IsSwap g) :
    sign l.prod = (-1) ^ l.length := by
  have h₁ : l.map sign = List.replicate l.length (-1) :=
    List.eq_replicate_iff.2
      ⟨by simp, fun u hu =>
        let ⟨g, hg⟩ := List.mem_map.1 hu
        hg.2 ▸ (hl _ hg.1).sign_eq⟩
  rw [← List.prod_replicate, ← h₁, List.prod_hom _ (@sign α _ _)]
Sign of a Product of Transpositions is $(-1)^{\text{length}}$
Informal description
For any list $l$ of permutations of a finite type $\alpha$, if every permutation in $l$ is a transposition, then the sign of the product of the permutations in $l$ is equal to $(-1)$ raised to the power of the length of $l$, i.e., $\text{sign}(\prod l) = (-1)^{|l|}$.
Equiv.Perm.sign_abs theorem
(f : Perm α) : |(Equiv.Perm.sign f : ℤ)| = 1
Full source 
@[simp]
theorem sign_abs (f : Perm α) :
    |(Equiv.Perm.sign f : ℤ)| = 1 := by
  rw [Int.abs_eq_natAbs, Int.units_natAbs, Nat.cast_one]
Absolute value of permutation sign is one
Informal description
For any permutation $f$ of a finite type $\alpha$, the absolute value of the sign of $f$ (as an integer) is equal to $1$, i.e., $|\text{sign}(f)| = 1$.
Equiv.Perm.sign_surjective theorem
[Nontrivial α] : Function.Surjective (sign : Perm α → ℤˣ)
Full source 
theorem sign_surjective [Nontrivial α] : Function.Surjective (sign : Perm α → ℤℤˣ) := fun a =>
  (Int.units_eq_one_or a).elim (fun h => ⟨1, by simp [h]⟩) fun h =>
    let ⟨x, y, hxy⟩ := exists_pair_ne α
    ⟨swap x y, by rw [sign_swap hxy, h]⟩
Surjectivity of the Permutation Sign Homomorphism
Informal description
For any nontrivial finite type $\alpha$, the sign homomorphism $\text{sign} : \text{Perm}(\alpha) \to \mathbb{Z}^\times$ is surjective. That is, for every unit $u \in \mathbb{Z}^\times$, there exists a permutation $f \in \text{Perm}(\alpha)$ such that $\text{sign}(f) = u$.
Equiv.Perm.sign_subtypePerm theorem
(f : Perm α) {p : α → Prop} [DecidablePred p] (h₁ : ∀ x, p x ↔ p (f x)) (h₂ : ∀ x, f x ≠ x → p x) : sign (subtypePerm f h₁) = sign f
Full source 
theorem sign_subtypePerm (f : Perm α) {p : α → Prop} [DecidablePred p] (h₁ : ∀ x, p x ↔ p (f x))
    (h₂ : ∀ x, f x ≠ x → p x) : sign (subtypePerm f h₁) = sign f := by
  let l := (truncSwapFactors (subtypePerm f h₁)).out
  have hl' : ∀ g' ∈ l.1.map ofSubtype, IsSwap g' := fun g' hg' =>
    let ⟨g, hg⟩ := List.mem_map.1 hg'
    hg.2 ▸ (l.2.2 _ hg.1).of_subtype_isSwap
  have hl'₂ : (l.1.map ofSubtype).prod = f := by
    rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
  conv =>
    congr
    rw [← l.2.1]
  simp_rw [← hl'₂]
  rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]
Sign Preservation under Subtype Restriction of a Permutation
Informal description
Let $f$ be a permutation of a finite type $\alpha$, and let $p : \alpha \to \mathrm{Prop}$ be a decidable predicate on $\alpha$. Suppose that: 1. For every $x \in \alpha$, $p(x)$ holds if and only if $p(f(x))$ holds. 2. For every $x \in \alpha$, if $f(x) \neq x$, then $p(x)$ holds. Then the sign of the permutation $f$ restricted to the subtype $\{x \in \alpha \mid p(x)\}$ is equal to the sign of $f$, i.e., $\mathrm{sign}(\mathrm{subtypePerm}\, f\, h_1) = \mathrm{sign}(f)$.
Equiv.Perm.sign_eq_sign_of_equiv theorem
[DecidableEq β] [Fintype β] (f : Perm α) (g : Perm β) (e : α ≃ β) (h : ∀ x, e (f x) = g (e x)) : sign f = sign g
Full source 
theorem sign_eq_sign_of_equiv [DecidableEq β] [Fintype β] (f : Perm α) (g : Perm β) (e : α ≃ β)
    (h : ∀ x, e (f x) = g (e x)) : sign f = sign g := by
  have hg : g = (e.symm.trans f).trans e := Equiv.ext <| by simp [h]
  rw [hg, sign_symm_trans_trans]
Equivariance of Permutation Sign under Equivalence
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $f$ be a permutation of $\alpha$ and $g$ a permutation of $\beta$. If there exists an equivalence $e : \alpha \simeq \beta$ such that for all $x \in \alpha$, $e(f(x)) = g(e(x))$, then the sign of $f$ equals the sign of $g$, i.e., $\text{sign}(f) = \text{sign}(g)$.
Equiv.Perm.sign_bij theorem
[DecidableEq β] [Fintype β] {f : Perm α} {g : Perm β} (i : ∀ x : α, f x ≠ x → β) (h : ∀ x hx hx', i (f x) hx' = g (i x hx)) (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂) (hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) : sign f = sign g
Full source 
theorem sign_bij [DecidableEq β] [Fintype β] {f : Perm α} {g : Perm β} (i : ∀ x : α, f x ≠ x → β)
    (h : ∀ x hx hx', i (f x) hx' = g (i x hx)) (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂)
    (hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) : sign f = sign g :=
  calc
    sign f = sign (subtypePerm f <| by simp : Perm { x // f x ≠ x }) :=
      (sign_subtypePerm _ _ fun _ => id).symm
    _ = sign (subtypePerm g <| by simp : Perm { x // g x ≠ x }) :=
      sign_eq_sign_of_equiv _ _
        (Equiv.ofBijective
          (fun x : { x // f x ≠ x } =>
            (⟨i x.1 x.2, by
                have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
                rw [← h _ x.2 this]
                exact mt (hi _ _ this x.2) x.2⟩ :
              { y // g y ≠ y }))
          ⟨fun ⟨_, _⟩ ⟨_, _⟩ h => Subtype.eq (hi _ _ _ _ (Subtype.mk.inj h)), fun ⟨y, hy⟩ =>
            let ⟨x, hfx, hx⟩ := hg y hy
            ⟨⟨x, hfx⟩, Subtype.eq hx⟩⟩)
        fun ⟨x, _⟩ => Subtype.eq (h x _ _)
    _ = sign g := sign_subtypePerm _ _ fun _ => id
Sign Equality of Permutations via Bijection on Supports
Informal description
Let $\alpha$ and $\beta$ be finite types with decidable equality, and let $f$ be a permutation of $\alpha$ and $g$ a permutation of $\beta$. Suppose there exists a function $i : \alpha \to \beta$ defined on the support of $f$ (i.e., for all $x \in \alpha$ with $f(x) \neq x$) such that: 1. For all $x \in \alpha$ and $hx : f(x) \neq x$, $hx' : f(f(x)) \neq f(x)$, we have $i(f(x), hx') = g(i(x, hx))$. 2. The function $i$ is injective on its domain, i.e., for all $x_1, x_2 \in \alpha$ and $hx_1 : f(x_1) \neq x_1$, $hx_2 : f(x_2) \neq x_2$, if $i(x_1, hx_1) = i(x_2, hx_2)$ then $x_1 = x_2$. 3. The function $i$ is surjective onto the support of $g$, i.e., for all $y \in \beta$ with $g(y) \neq y$, there exists $x \in \alpha$ and $hx : f(x) \neq x$ such that $i(x, hx) = y$. Then the sign of $f$ equals the sign of $g$, i.e., $\text{sign}(f) = \text{sign}(g)$.
Equiv.Perm.prod_prodExtendRight theorem
{α : Type*} [DecidableEq α] (σ : α → Perm β) {l : List α} (hl : l.Nodup) (mem_l : ∀ a, a ∈ l) : (l.map fun a => prodExtendRight a (σ a)).prod = prodCongrRight σ
Full source 
/-- If we apply `prod_extendRight a (σ a)` for all `a : α` in turn,
we get `prod_congrRight σ`. -/
theorem prod_prodExtendRight {α : Type*} [DecidableEq α] (σ : α → Perm β) {l : List α}
    (hl : l.Nodup) (mem_l : ∀ a, a ∈ l) :
    (l.map fun a => prodExtendRight a (σ a)).prod = prodCongrRight σ := by
  ext ⟨a, b⟩ : 1
  -- We'll use induction on the list of elements,
  -- but we have to keep track of whether we already passed `a` in the list.
  suffices a ∈ la ∈ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, σ a b)a ∈ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, σ a b) ∨
      a ∉ l ∧ (l.map fun a => prodExtendRight a (σ a)).prod (a, b) = (a, b) by
    obtain ⟨_, prod_eq⟩ := Or.resolve_right this (not_and.mpr fun h _ => h (mem_l a))
    rw [prod_eq, prodCongrRight_apply]
  clear mem_l
  induction' l with a' l ih
  · refine Or.inr ⟨List.not_mem_nil, ?_⟩
    rw [List.map_nil, List.prod_nil, one_apply]
  rw [List.map_cons, List.prod_cons, mul_apply]
  rcases ih (List.nodup_cons.mp hl).2 with (⟨mem_l, prod_eq⟩ | ⟨not_mem_l, prod_eq⟩) <;>
    rw [prod_eq]
  · refine Or.inl ⟨List.mem_cons_of_mem _ mem_l, ?_⟩
    rw [prodExtendRight_apply_ne _ fun h : a = a' => (List.nodup_cons.mp hl).1 (h ▸ mem_l)]
  by_cases ha' : a = a'
  · rw [← ha'] at *
    refine Or.inl ⟨l.mem_cons_self, ?_⟩
    rw [prodExtendRight_apply_eq]
  · refine Or.inr ⟨fun h => not_or_intro ha' not_mem_l ((List.mem_cons).mp h), ?_⟩
    rw [prodExtendRight_apply_ne _ ha']
Product of Extended Permutations Equals Product of Right Congruent Permutations
Informal description
Let $\alpha$ be a type with decidable equality and $\beta$ be any type. Given a function $\sigma : \alpha \to \text{Perm}(\beta)$ and a list $l$ of distinct elements of $\alpha$ containing all elements of $\alpha$, the product of the permutations obtained by applying $\text{prodExtendRight}$ to each element $a \in l$ with $\sigma(a)$ equals $\text{prodCongrRight}(\sigma)$. In other words, if we apply $\text{prodExtendRight}$ to each element $a \in l$ with the corresponding permutation $\sigma(a)$, the product of these extended permutations is equal to the permutation obtained by taking the product of $\sigma$ over all elements of $\alpha$.
Equiv.Perm.sign_prodExtendRight theorem
(a : α) (σ : Perm β) : sign (prodExtendRight a σ) = sign σ
Full source 
@[simp]
theorem sign_prodExtendRight (a : α) (σ : Perm β) : sign (prodExtendRight a σ) = sign σ :=
  sign_bij (fun (ab : α × β) _ => ab.snd)
    (fun ⟨a', b⟩ hab _ => by simp [eq_of_prodExtendRight_ne hab])
    (fun ⟨a₁, b₁⟩ ⟨a₂, b₂⟩ hab₁ hab₂ h => by
      simpa [eq_of_prodExtendRight_ne hab₁, eq_of_prodExtendRight_ne hab₂] using h)
    fun y hy => ⟨(a, y), by simpa, by simp⟩
Sign Preservation under Permutation Extension
Informal description
For any element $a$ of a type $\alpha$ and any permutation $\sigma$ of a type $\beta$, the sign of the permutation obtained by extending $\sigma$ to $\alpha \times \beta$ via $a$ is equal to the sign of $\sigma$, i.e., $\text{sign}(\text{prodExtendRight}(a, \sigma)) = \text{sign}(\sigma)$.
Equiv.Perm.sign_prodCongrRight theorem
(σ : α → Perm β) : sign (prodCongrRight σ) = ∏ k, sign (σ k)
Full source 
theorem sign_prodCongrRight (σ : α → Perm β) : sign (prodCongrRight σ) = ∏ k, sign (σ k) := by
  obtain ⟨l, hl, mem_l⟩ := Finite.exists_univ_list α
  have l_to_finset : l.toFinset = Finset.univ := by
    apply eq_top_iff.mpr
    intro b _
    exact List.mem_toFinset.mpr (mem_l b)
  rw [← prod_prodExtendRight σ hl mem_l, map_list_prod sign, List.map_map, ← l_to_finset,
    List.prod_toFinset _ hl]
  simp_rw [← fun a => sign_prodExtendRight a (σ a), Function.comp_def]
Sign of Product of Right Congruent Permutations Equals Product of Signs
Informal description
For any function $\sigma : \alpha \to \text{Perm}(\beta)$ mapping elements of a finite type $\alpha$ to permutations of $\beta$, the sign of the permutation $\text{prodCongrRight}(\sigma)$ is equal to the product of the signs of the permutations $\sigma(k)$ for all $k \in \alpha$, i.e., \[ \text{sign}(\text{prodCongrRight}(\sigma)) = \prod_{k \in \alpha} \text{sign}(\sigma(k)). \]
Equiv.Perm.sign_prodCongrLeft theorem
(σ : α → Perm β) : sign (prodCongrLeft σ) = ∏ k, sign (σ k)
Full source 
theorem sign_prodCongrLeft (σ : α → Perm β) : sign (prodCongrLeft σ) = ∏ k, sign (σ k) := by
  refine (sign_eq_sign_of_equiv _ _ (prodComm β α) ?_).trans (sign_prodCongrRight σ)
  rintro ⟨b, α⟩
  rfl
Sign of Product of Left Congruent Permutations Equals Product of Signs
Informal description
For any function $\sigma : \alpha \to \text{Perm}(\beta)$ mapping elements of a finite type $\alpha$ to permutations of $\beta$, the sign of the permutation $\text{prodCongrLeft}(\sigma)$ is equal to the product of the signs of the permutations $\sigma(k)$ for all $k \in \alpha$, i.e., \[ \text{sign}(\text{prodCongrLeft}(\sigma)) = \prod_{k \in \alpha} \text{sign}(\sigma(k)). \]
Equiv.Perm.sign_permCongr theorem
(e : α ≃ β) (p : Perm α) : sign (e.permCongr p) = sign p
Full source 
@[simp]
theorem sign_permCongr (e : α ≃ β) (p : Perm α) : sign (e.permCongr p) = sign p :=
  sign_eq_sign_of_equiv _ _ e.symm (by simp)
Invariance of Permutation Sign under Conjugation by Equivalence
Informal description
For any equivalence $e : \alpha \simeq \beta$ between finite types $\alpha$ and $\beta$, and any permutation $p$ of $\alpha$, the sign of the conjugate permutation $e.permCongr\, p$ is equal to the sign of $p$, i.e., $\text{sign}(e.permCongr\, p) = \text{sign}(p)$.
Equiv.Perm.sign_sumCongr theorem
(σa : Perm α) (σb : Perm β) : sign (sumCongr σa σb) = sign σa * sign σb
Full source 
@[simp]
theorem sign_sumCongr (σa : Perm α) (σb : Perm β) : sign (sumCongr σa σb) = sign σa * sign σb := by
  suffices signsign (sumCongr σa (1 : Perm β)) = sign σa ∧ sign (sumCongr (1 : Perm α) σb) = sign σb
    by rw [← this.1, ← this.2, ← sign_mul, sumCongr_mul, one_mul, mul_one]
  constructor
  · induction σa using swap_induction_on with
    | one => simp
    | swap_mul σa' a₁ a₂ ha ih =>
      rw [← one_mul (1 : Perm β), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_swap_one,
        sign_swap ha, sign_swap (Sum.inl_injective.ne_iff.mpr ha)]
  · induction σb using swap_induction_on with
    | one => simp
    | swap_mul σb' b₁ b₂ hb ih =>
      rw [← one_mul (1 : Perm α), ← sumCongr_mul, sign_mul, sign_mul, ih, sumCongr_one_swap,
        sign_swap hb, sign_swap (Sum.inr_injective.ne_iff.mpr hb)]
Sign of Direct Sum of Permutations: $\text{sign}(\sigma_a \oplus \sigma_b) = \text{sign}(\sigma_a) \cdot \text{sign}(\sigma_b)$
Informal description
For any permutations $\sigma_a$ of a finite type $\alpha$ and $\sigma_b$ of a finite type $\beta$, the sign of their direct sum permutation $\sigma_a \oplus \sigma_b$ is equal to the product of their signs, i.e., $\text{sign}(\sigma_a \oplus \sigma_b) = \text{sign}(\sigma_a) \cdot \text{sign}(\sigma_b)$.
Equiv.Perm.sign_subtypeCongr theorem
{p : α → Prop} [DecidablePred p] (ep : Perm { a // p a }) (en : Perm { a // ¬p a }) : sign (ep.subtypeCongr en) = sign ep * sign en
Full source 
@[simp]
theorem sign_subtypeCongr {p : α → Prop} [DecidablePred p] (ep : Perm { a // p a })
    (en : Perm { a // ¬p a }) : sign (ep.subtypeCongr en) = sign ep * sign en := by
  simp [subtypeCongr]
Sign of Combined Permutations on Complementary Subtypes: $\text{sign}(\sigma_p \oplus \sigma_{\neg p}) = \text{sign}(\sigma_p) \cdot \text{sign}(\sigma_{\neg p})$
Informal description
For any predicate $p$ on a finite type $\alpha$ (with a decidable predicate), and for any permutations $\sigma_p$ of the subtype $\{a \mid p(a)\}$ and $\sigma_{\neg p}$ of the subtype $\{a \mid \neg p(a)\}$, the sign of the permutation obtained by combining $\sigma_p$ and $\sigma_{\neg p}$ via `subtypeCongr` is equal to the product of their signs, i.e., $\text{sign}(\sigma_p.\text{subtypeCongr}\, \sigma_{\neg p}) = \text{sign}(\sigma_p) \cdot \text{sign}(\sigma_{\neg p})$.
Equiv.Perm.sign_extendDomain theorem
(e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e
Full source 
@[simp]
theorem sign_extendDomain (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) :
    Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e := by
  simp only [Equiv.Perm.extendDomain, sign_subtypeCongr, sign_permCongr, sign_refl, mul_one]
Invariance of Permutation Sign under Domain Extension
Informal description
For any permutation $e$ of a finite type $\alpha$, any predicate $p$ on a type $\beta$ (with a decidable predicate), and any equivalence $f$ between $\alpha$ and the subtype $\{b \mid p(b)\}$, the sign of the permutation $e.\text{extendDomain}\, f$ is equal to the sign of $e$, i.e., $\text{sign}(e.\text{extendDomain}\, f) = \text{sign}(e)$.
Equiv.Perm.sign_ofSubtype theorem
{p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) : sign (ofSubtype f) = sign f
Full source 
@[simp]
theorem sign_ofSubtype {p : α → Prop} [DecidablePred p] (f : Equiv.Perm (Subtype p)) :
    sign (ofSubtype f) = sign f :=
  sign_extendDomain f (Equiv.refl (Subtype p))
Sign Preservation under Subtype Permutation Lifting
Informal description
For any predicate $p$ on a finite type $\alpha$ (with a decidable predicate) and any permutation $f$ of the subtype $\{a \mid p(a)\}$, the sign of the permutation $\text{ofSubtype}\, f$ is equal to the sign of $f$, i.e., $\text{sign}(\text{ofSubtype}\, f) = \text{sign}(f)$.
Equiv.Perm.viaFintypeEmbedding_sign theorem
[Fintype α] [Fintype β] [DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) : sign (e.viaFintypeEmbedding f) = sign e
Full source 
@[simp]
theorem viaFintypeEmbedding_sign
    [Fintype α] [Fintype β] [DecidableEq β] (e : Equiv.Perm α) (f : α ↪ β) :
    sign (e.viaFintypeEmbedding f) = sign e := by
  simp [viaFintypeEmbedding]
Invariance of Permutation Sign under Finite Type Embedding
Informal description
For any permutation $e$ of a finite type $\alpha$ and any embedding $f$ from $\alpha$ to another finite type $\beta$ with decidable equality, the sign of the permutation $e.\text{viaFintypeEmbedding}\, f$ is equal to the sign of $e$, i.e., $\text{sign}(e.\text{viaFintypeEmbedding}\, f) = \text{sign}(e)$.
Equiv.Perm.ofSign definition
(s : ℤˣ) : Finset (Perm α)
Full source 
/-- Permutations of a given sign. -/
def ofSign (s : ℤℤˣ) : Finset (Perm α) := univ.filter (sign · = s)
Permutations of a given sign
Informal description
For a given unit \( s \) in the integers \( \mathbb{Z}^\times \), the set of all permutations \( \sigma \) of a finite type \( \alpha \) such that the sign of \( \sigma \) equals \( s \). More precisely, this is the subset of the symmetric group \( \text{Perm}(\alpha) \) consisting of all permutations \( \sigma \) for which \( \text{sign}(\sigma) = s \).
Equiv.Perm.mem_ofSign theorem
{s : ℤˣ} {σ : Perm α} : σ ∈ ofSign s ↔ σ.sign = s
Full source 
@[simp]
lemma mem_ofSign {s : ℤℤˣ} {σ : Perm α} : σ ∈ ofSign sσ ∈ ofSign s ↔ σ.sign = s := by
  rw [ofSign, mem_filter, and_iff_right (mem_univ σ)]
Membership in Permutation Sign Set Characterized by Sign Equality
Informal description
For any unit $s \in \mathbb{Z}^\times$ and any permutation $\sigma$ of a finite type $\alpha$, the permutation $\sigma$ belongs to the set $\text{ofSign}(s)$ if and only if the sign of $\sigma$ equals $s$, i.e., $\text{sign}(\sigma) = s$.
Equiv.Perm.ofSign_disjoint theorem
: _root_.Disjoint (ofSign 1 : Finset (Perm α)) (ofSign (-1))
Full source 
lemma ofSign_disjoint : _root_.Disjoint (ofSign 1 : Finset (Perm α)) (ofSign (-1)) := by
  rw [Finset.disjoint_iff_ne]
  rintro σ hσ τ hτ rfl
  rw [mem_ofSign] at hσ hτ
  have := hσ.symm.trans hτ
  contradiction
Disjointness of Permutation Sets by Sign
Informal description
The sets of permutations with sign $1$ and sign $-1$ are disjoint, i.e., $\text{ofSign}(1) \cap \text{ofSign}(-1) = \emptyset$.
Equiv.Perm.ofSign_disjUnion theorem
: (ofSign 1).disjUnion (ofSign (-1)) ofSign_disjoint = (univ : Finset (Perm α))
Full source 
lemma ofSign_disjUnion :
    (ofSign 1).disjUnion (ofSign (-1)) ofSign_disjoint = (univ : Finset (Perm α)) := by
  ext σ
  simp_rw [mem_disjUnion, mem_ofSign, Int.units_eq_one_or, mem_univ]
Disjoint Union of Permutation Sign Sets Covers All Permutations
Informal description
The disjoint union of the set of permutations with sign $1$ and the set of permutations with sign $-1$ is equal to the entire set of permutations of a finite type $\alpha$. In other words, $( \text{ofSign}(1) \sqcup \text{ofSign}(-1) ) = \text{univ}$, where $\text{univ}$ denotes the universal set of all permutations of $\alpha$.