# 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

def Equiv.Perm.modSwap {α : Type u} [] (i : α) (j : α) :

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.

Equations
• = { r := fun (σ τ : ) => σ = τ σ = * τ, iseqv := }
Instances For
noncomputable instance Equiv.Perm.instDecidableRelROfFintype {α : Type u_1} [] [] (i : α) (j : α) :
DecidableRel Setoid.r
Equations
• = Or.decidable
def Equiv.Perm.swapFactorsAux {α : Type u} [] (l : List α) (f : ) :
(∀ {x : α}, f x xx l){ l : List () // l.prod = f gl, g.IsSwap }

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.

Equations
• One or more equations did not get rendered due to their size.
• = fun (f : ) (h : ∀ {x : α}, f x xx []) => [],
Instances For
def Equiv.Perm.swapFactors {α : Type u} [] [] [] (f : ) :
{ l : List () // l.prod = f gl, g.IsSwap }

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.

Equations
Instances For
def Equiv.Perm.truncSwapFactors {α : Type u} [] [] (f : ) :
Trunc { l : List () // l.prod = f gl, g.IsSwap }

This computably represents the fact that any permutation can be represented as the product of a list of transpositions.

Equations
• One or more equations did not get rendered due to their size.
Instances For
theorem Equiv.Perm.swap_induction_on {α : Type u} [] [] {P : } (f : ) :
P 1(∀ (f : ) (x y : α), x yP fP ( * f))P f

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.

theorem Equiv.Perm.mclosure_isSwap {α : Type u} [] [] :
Submonoid.closure {σ : | σ.IsSwap} =
theorem Equiv.Perm.closure_isSwap {α : Type u} [] [] :
Subgroup.closure {σ : | σ.IsSwap} =
theorem Equiv.Perm.mclosure_swap_castSucc_succ (n : ) :
Submonoid.closure (Set.range fun (i : Fin n) => Equiv.swap i.castSucc i.succ) =

Every finite symmetric group is generated by transpositions of adjacent elements.

theorem Equiv.Perm.swap_induction_on' {α : Type u} [] [] {P : } (f : ) :
P 1(∀ (f : ) (x y : α), x yP fP (f * ))P f

Like swap_induction_on, but with the composition on the right of f.

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.

theorem Equiv.Perm.isConj_swap {α : Type u} [] {w : α} {x : α} {y : α} {z : α} (hwx : w x) (hyz : y z) :
IsConj () ()
def Equiv.Perm.finPairsLT (n : ) :
Finset ((_ : Fin n) × Fin n)

set of all pairs (⟨a, b⟩ : Σ a : fin n, fin n) such that b < a

Equations
• = Finset.univ.sigma fun (a : Fin n) => ().attachFin
Instances For
theorem Equiv.Perm.mem_finPairsLT {n : } {a : (_ : Fin n) × Fin n} :
a.snd < a.fst
def Equiv.Perm.signAux {n : } (a : Equiv.Perm (Fin n)) :

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₂

Equations
• a.signAux = x ∈ , if a x.fst a x.snd then -1 else 1
Instances For
@[simp]
theorem Equiv.Perm.signAux_one (n : ) :
def Equiv.Perm.signBijAux {n : } (f : Equiv.Perm (Fin n)) (a : (_ : Fin n) × Fin n) :
(_ : Fin n) × Fin n

signBijAux f ⟨a, b⟩ returns the pair consisting of f a and f b in decreasing order.

Equations
• f.signBijAux a = if x : f a.snd < f a.fst then f a.fst, f a.snd else f a.snd, f a.fst
Instances For
theorem Equiv.Perm.signBijAux_injOn {n : } {f : Equiv.Perm (Fin n)} :
Set.InjOn f.signBijAux
theorem Equiv.Perm.signBijAux_surj {n : } {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) :
b, f.signBijAux b = a
theorem Equiv.Perm.signBijAux_mem {n : } {f : Equiv.Perm (Fin n)} (a : (_ : Fin n) × Fin n) :
f.signBijAux a
@[simp]
theorem Equiv.Perm.signAux_inv {n : } (f : Equiv.Perm (Fin n)) :
f⁻¹.signAux = f.signAux
theorem Equiv.Perm.signAux_mul {n : } (f : Equiv.Perm (Fin n)) (g : Equiv.Perm (Fin n)) :
(f * g).signAux = f.signAux * g.signAux
theorem Equiv.Perm.signAux_swap {n : } {x : Fin n} {y : Fin n} (_hxy : x y) :
().signAux = -1
def Equiv.Perm.signAux2 {α : Type u} [] :
List α

When the list l : List α contains all nonfixed points of the permutation f : Perm α, signAux2 l f recursively calculates the sign of f.

Equations
Instances For
theorem Equiv.Perm.signAux_eq_signAux2 {α : Type u} [] {n : } (l : List α) (f : ) (e : α Fin n) (_h : ∀ (x : α), f x xx l) :
Equiv.Perm.signAux ((e.symm.trans f).trans e) =
def Equiv.Perm.signAux3 {α : Type u} [] [] (f : ) {s : } :
(∀ (x : α), x s)

When the multiset s : Multiset α contains all nonfixed points of the permutation f : Perm α, signAux2 f _ recursively calculates the sign of f.

Equations
• f.signAux3 = Quotient.hrecOn (motive := fun (x : ) => (∀ (x_1 : α), x_1 x)) s (fun (l : List α) (x : ∀ (x : α), x l) => )
Instances For
theorem Equiv.Perm.signAux3_mul_and_swap {α : Type u} [] [] (f : ) (g : ) (s : ) (hs : ∀ (x : α), x s) :
(f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs Pairwise fun (x y : α) => ().signAux3 hs = -1
theorem Equiv.Perm.signAux3_symm_trans_trans {α : Type u} [] {β : Type v} [] [] [] (f : ) (e : α β) {s : } {t : } (hs : ∀ (x : α), x s) (ht : ∀ (x : β), x t) :
Equiv.Perm.signAux3 ((e.symm.trans f).trans e) ht = f.signAux3 hs
def Equiv.Perm.sign {α : Type u} [] [] :

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.

Equations
Instances For
theorem Equiv.Perm.sign_mul {α : Type u} [] [] (f : ) (g : ) :
Equiv.Perm.sign (f * g) = Equiv.Perm.sign f * Equiv.Perm.sign g
@[simp]
theorem Equiv.Perm.sign_trans {α : Type u} [] [] (f : ) (g : ) :
Equiv.Perm.sign () = Equiv.Perm.sign g * Equiv.Perm.sign f
theorem Equiv.Perm.sign_one {α : Type u} [] [] :
Equiv.Perm.sign 1 = 1
@[simp]
theorem Equiv.Perm.sign_refl {α : Type u} [] [] :
Equiv.Perm.sign () = 1
theorem Equiv.Perm.sign_inv {α : Type u} [] [] (f : ) :
Equiv.Perm.sign f⁻¹ = Equiv.Perm.sign f
@[simp]
theorem Equiv.Perm.sign_symm {α : Type u} [] [] (e : ) :
Equiv.Perm.sign () = Equiv.Perm.sign e
theorem Equiv.Perm.sign_swap {α : Type u} [] [] {x : α} {y : α} (h : x y) :
Equiv.Perm.sign () = -1
@[simp]
theorem Equiv.Perm.sign_swap' {α : Type u} [] [] {x : α} {y : α} :
Equiv.Perm.sign () = if x = y then 1 else -1
theorem Equiv.Perm.IsSwap.sign_eq {α : Type u} [] [] {f : } (h : f.IsSwap) :
Equiv.Perm.sign f = -1
@[simp]
theorem Equiv.Perm.sign_symm_trans_trans {α : Type u} [] {β : Type v} [] [] [] (f : ) (e : α β) :
Equiv.Perm.sign ((e.symm.trans f).trans e) = Equiv.Perm.sign f
@[simp]
theorem Equiv.Perm.sign_trans_trans_symm {α : Type u} [] {β : Type v} [] [] [] (f : ) (e : α β) :
Equiv.Perm.sign ((e.trans f).trans e.symm) = Equiv.Perm.sign f
theorem Equiv.Perm.sign_prod_list_swap {α : Type u} [] [] {l : List ()} (hl : gl, g.IsSwap) :
Equiv.Perm.sign l.prod = (-1) ^ l.length
theorem Equiv.Perm.sign_surjective (α : Type u) [] [] [] :
Function.Surjective Equiv.Perm.sign
theorem Equiv.Perm.eq_sign_of_surjective_hom {α : Type u} [] [] {s : } (hs : ) :
s = Equiv.Perm.sign
theorem Equiv.Perm.sign_subtypePerm {α : Type u} [] [] (f : ) {p : αProp} [] (h₁ : ∀ (x : α), p x p (f x)) (h₂ : ∀ (x : α), f x xp x) :
Equiv.Perm.sign (f.subtypePerm h₁) = Equiv.Perm.sign f
theorem Equiv.Perm.sign_eq_sign_of_equiv {α : Type u} [] {β : Type v} [] [] [] (f : ) (g : ) (e : α β) (h : ∀ (x : α), e (f x) = g (e x)) :
Equiv.Perm.sign f = Equiv.Perm.sign g
theorem Equiv.Perm.sign_bij {α : Type u} [] {β : Type v} [] [] [] {f : } {g : } (i : (x : α) → f x xβ) (h : ∀ (x : α) (hx : f x x) (hx' : f (f x) f x), i (f x) hx' = g (i x hx)) (hi : ∀ (x₁ x₂ : α) (hx₁ : f x₁ x₁) (hx₂ : f x₂ x₂), i x₁ hx₁ = i x₂ hx₂x₁ = x₂) (hg : ∀ (y : β), g y y∃ (x : α) (hx : f x x), i x hx = y) :
Equiv.Perm.sign f = Equiv.Perm.sign g
theorem Equiv.Perm.prod_prodExtendRight {β : Type v} {α : Type u_1} [] (σ : α) {l : List α} (hl : l.Nodup) (mem_l : ∀ (a : α), a l) :
(List.map (fun (a : α) => ) l).prod =

If we apply prod_extendRight a (σ a) for all a : α in turn, we get prod_congrRight σ.

@[simp]
theorem Equiv.Perm.sign_prodExtendRight {α : Type u} [] {β : Type v} [] [] [] (a : α) (σ : ) :
Equiv.Perm.sign = Equiv.Perm.sign σ
theorem Equiv.Perm.sign_prodCongrRight {α : Type u} [] {β : Type v} [] [] [] (σ : α) :
Equiv.Perm.sign = k : α, Equiv.Perm.sign (σ k)
theorem Equiv.Perm.sign_prodCongrLeft {α : Type u} [] {β : Type v} [] [] [] (σ : α) :
Equiv.Perm.sign = k : α, Equiv.Perm.sign (σ k)
@[simp]
theorem Equiv.Perm.sign_permCongr {α : Type u} [] {β : Type v} [] [] [] (e : α β) (p : ) :
Equiv.Perm.sign (e.permCongr p) = Equiv.Perm.sign p
@[simp]
theorem Equiv.Perm.sign_sumCongr {α : Type u} [] {β : Type v} [] [] [] (σa : ) (σb : ) :
Equiv.Perm.sign (σa.sumCongr σb) = Equiv.Perm.sign σa * Equiv.Perm.sign σb
@[simp]
theorem Equiv.Perm.sign_subtypeCongr {α : Type u} [] [] {p : αProp} [] (ep : Equiv.Perm { a : α // p a }) (en : Equiv.Perm { a : α // ¬p a }) :
Equiv.Perm.sign (ep.subtypeCongr en) = Equiv.Perm.sign ep * Equiv.Perm.sign en
@[simp]
theorem Equiv.Perm.sign_extendDomain {α : Type u} [] {β : Type v} [] [] [] (e : ) {p : βProp} [] (f : α ) :
Equiv.Perm.sign (e.extendDomain f) = Equiv.Perm.sign e
@[simp]
theorem Equiv.Perm.sign_ofSubtype {α : Type u} [] [] {p : αProp} [] (f : ) :
Equiv.Perm.sign (Equiv.Perm.ofSubtype f) = Equiv.Perm.sign f