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/Finite.lean

@[implicit_reducible]

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

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.

@[implicit_reducible]

noncomputable instance Equiv.Perm.instDecidableRelROfFintype {α : Type u_1} [Fintype α] [DecidableEq α] (i j : α) : DecidableRel ⇑(modSwap i j)

def Equiv.Perm.swapFactorsAux {α : Type u} [DecidableEq α] (l : List α) (f : Perm α) : (∀ {x : α}, f x ≠ x → x ∈ l) → { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, 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.

def Equiv.Perm.swapFactors {α : Type u} [DecidableEq α] [Fintype α] [LinearOrder α] (f : Perm α) : { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }

swapFactors represents a permutation as a product of a list of transpositions. The representation is nonunique and depends on the linear order structure. For types without linear order truncSwapFactors can be used.

def Equiv.Perm.truncSwapFactors {α : Type u} [DecidableEq α] [Fintype α] (f : Perm α) : Trunc { l : List (Perm α) // l.prod = f ∧ ∀ g ∈ l, g.IsSwap }

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

theorem Equiv.Perm.swap_induction_on {α : Type u} [DecidableEq α] [Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1) (swap_mul : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (swap x y * f)) : motive 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} [DecidableEq α] [Finite α] : Submonoid.closure {σ : Perm α | σ.IsSwap} = ⊤

theorem Equiv.Perm.closure_isSwap {α : Type u} [DecidableEq α] [Finite α] : Subgroup.closure {σ : Perm α | σ.IsSwap} = ⊤

theorem Equiv.Perm.mclosure_swap_castSucc_succ (n : ℕ) : Submonoid.closure (Set.range fun (i : Fin n) => swap i.castSucc i.succ) = ⊤

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

theorem Equiv.Perm.swap_induction_on' {α : Type u} [DecidableEq α] [Finite α] {motive : Perm α → Prop} (f : Perm α) (one : motive 1) (mul_swap : ∀ (f : Perm α) (x y : α), x ≠ y → motive f → motive (f * swap x y)) : motive f

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.

theorem Equiv.Perm.isConj_swap {α : Type u} [DecidableEq α] {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) : IsConj (swap w x) (swap y z)

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

theorem Equiv.Perm.mem_finPairsLT {n : ℕ} {a : (_ : Fin n) × Fin n} : a ∈ finPairsLT n ↔ a.snd < a.fst

def Equiv.Perm.signAux {n : ℕ} (a : 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₂

@[simp]

theorem Equiv.Perm.signAux_one (n : ℕ) : signAux 1 = 1

def Equiv.Perm.signBijAux {n : ℕ} (f : 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.

theorem Equiv.Perm.signBijAux_injOn {n : ℕ} {f : Perm (Fin n)} : Set.InjOn f.signBijAux ↑(finPairsLT n)

theorem Equiv.Perm.signBijAux_surj {n : ℕ} {f : Perm (Fin n)} (a : (_ : Fin n) × Fin n) : a ∈ finPairsLT n → ∃ b ∈ finPairsLT n, f.signBijAux b = a

theorem Equiv.Perm.signBijAux_mem {n : ℕ} {f : Perm (Fin n)} (a : (_ : Fin n) × Fin n) : a ∈ finPairsLT n → f.signBijAux a ∈ finPairsLT n

@[simp]

theorem Equiv.Perm.signAux_inv {n : ℕ} (f : Perm (Fin n)) : f⁻¹.signAux = f.signAux

theorem Equiv.Perm.signAux_mul {n : ℕ} (f g : Perm (Fin n)) : (f * g).signAux = f.signAux * g.signAux

theorem Equiv.Perm.signAux_swap {n : ℕ} {x y : Fin n} (_hxy : x ≠ y) : (swap x y).signAux = -1

def Equiv.Perm.signAux2 {α : Type u} [DecidableEq α] : List α → Perm α → ℤˣ

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

theorem Equiv.Perm.signAux_eq_signAux2 {α : Type u} [DecidableEq α] {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

def Equiv.Perm.signAux3 {α : Type u} [DecidableEq α] [Finite α] (f : Perm α) {s : Multiset α} : (∀ (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.

theorem Equiv.Perm.signAux3_mul_and_swap {α : Type u} [DecidableEq α] [Finite α] (f g : Perm α) (s : Multiset α) (hs : ∀ (x : α), x ∈ s) : (f * g).signAux3 hs = f.signAux3 hs * g.signAux3 hs ∧ Pairwise fun (x y : α) => (swap x y).signAux3 hs = -1

theorem Equiv.Perm.signAux3_symm_trans_trans {α : Type u} [DecidableEq α] {β : Type v} [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 = f.signAux3 hs

def Equiv.Perm.sign {α : Type u} [DecidableEq α] [Fintype α] : Perm α →* ℤˣ

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.

@[simp]

theorem Equiv.Perm.sign_mul {α : Type u} [DecidableEq α] [Fintype α] (f g : Perm α) : sign (f * g) = sign f * sign g

@[simp]

theorem Equiv.Perm.sign_trans {α : Type u} [DecidableEq α] [Fintype α] (f g : Perm α) : sign (Equiv.trans f g) = sign g * sign f

@[simp]

theorem Equiv.Perm.sign_one {α : Type u} [DecidableEq α] [Fintype α] : sign 1 = 1

@[simp]

theorem Equiv.Perm.sign_refl {α : Type u} [DecidableEq α] [Fintype α] : sign (Equiv.refl α) = 1

@[simp]

theorem Equiv.Perm.sign_inv {α : Type u} [DecidableEq α] [Fintype α] (f : Perm α) : sign f⁻¹ = sign f

@[simp]

theorem Equiv.Perm.sign_symm {α : Type u} [DecidableEq α] [Fintype α] (e : Perm α) : sign (Equiv.symm e) = sign e

theorem Equiv.Perm.sign_swap {α : Type u} [DecidableEq α] [Fintype α] {x y : α} (h : x ≠ y) : sign (swap x y) = -1

@[simp]

theorem Equiv.Perm.sign_swap' {α : Type u} [DecidableEq α] [Fintype α] {x y : α} : sign (swap x y) = if x = y then 1 else -1

theorem Equiv.Perm.IsSwap.sign_eq {α : Type u} [DecidableEq α] [Fintype α] {f : Perm α} (h : f.IsSwap) : sign f = -1

@[simp]

theorem Equiv.Perm.sign_symm_trans_trans {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (f : Perm α) (e : α ≃ β) : sign ((e.symm.trans f).trans e) = sign f

@[simp]

theorem Equiv.Perm.sign_trans_trans_symm {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (f : Perm β) (e : α ≃ β) : sign ((e.trans f).trans e.symm) = sign f

theorem Equiv.Perm.sign_prod_list_swap {α : Type u} [DecidableEq α] [Fintype α] {l : List (Perm α)} (hl : ∀ g ∈ l, g.IsSwap) : sign l.prod = (-1) ^ l.length

@[simp]

theorem Equiv.Perm.sign_abs {α : Type u} [DecidableEq α] [Fintype α] (f : Perm α) : |↑(sign f)| = 1

theorem Equiv.Perm.sign_surjective (α : Type u) [DecidableEq α] [Fintype α] [Nontrivial α] : Function.Surjective ⇑sign

theorem Equiv.Perm.eq_sign_of_surjective_hom {α : Type u} [DecidableEq α] [Fintype α] {s : Perm α →* ℤˣ} (hs : Function.Surjective ⇑s) : s = sign

theorem Equiv.Perm.sign_subtypePerm {α : Type u} [DecidableEq α] [Fintype α] (f : Perm α) {p : α → Prop} [DecidablePred p] (h₁ : ∀ (x : α), p (f x) ↔ p x) (h₂ : ∀ (x : α), f x ≠ x → p x) : sign (f.subtypePerm h₁) = sign f

theorem Equiv.Perm.sign_eq_sign_of_equiv {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (f : Perm α) (g : Perm β) (e : α ≃ β) (h : ∀ (x : α), e (f x) = g (e x)) : sign f = sign g

theorem Equiv.Perm.sign_bij {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] {f : Perm α} {g : Perm β} (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) : sign f = sign g

theorem Equiv.Perm.prod_prodExtendRight {β : Type v} {α : Type u_1} [DecidableEq α] (σ : α → Perm β) {l : List α} (hl : l.Nodup) (mem_l : ∀ (a : α), a ∈ l) : (List.map (fun (a : α) => prodExtendRight a (σ a)) l).prod = prodCongrRight σ

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

@[simp]

theorem Equiv.Perm.sign_prodExtendRight {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (a : α) (σ : Perm β) : sign (prodExtendRight a σ) = sign σ

theorem Equiv.Perm.sign_prodCongrRight {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (σ : α → Perm β) : sign (prodCongrRight σ) = ∏ k : α, sign (σ k)

theorem Equiv.Perm.sign_prodCongrLeft {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (σ : α → Perm β) : sign (prodCongrLeft σ) = ∏ k : α, sign (σ k)

@[simp]

theorem Equiv.Perm.sign_permCongr {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (e : α ≃ β) (p : Perm α) : sign (e.permCongr p) = sign p

@[simp]

theorem Equiv.Perm.sign_sumCongr {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (σa : Perm α) (σb : Perm β) : sign (σa.sumCongr σb) = sign σa * sign σb

@[simp]

theorem Equiv.Perm.sign_subtypeCongr {α : Type u} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] (ep : Perm { a : α // p a }) (en : Perm { a : α // ¬p a }) : sign (ep.subtypeCongr en) = sign ep * sign en

@[simp]

theorem Equiv.Perm.sign_extendDomain {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [DecidableEq β] [Fintype β] (e : Perm α) {p : β → Prop} [DecidablePred p] (f : α ≃ Subtype p) : sign (e.extendDomain f) = sign e

@[simp]

theorem Equiv.Perm.sign_ofSubtype {α : Type u} [DecidableEq α] [Fintype α] {p : α → Prop} [DecidablePred p] [Fintype (Subtype p)] (f : Perm (Subtype p)) : sign (ofSubtype f) = sign f

@[simp]

theorem Equiv.Perm.viaFintypeEmbedding_sign {α : Type u} [DecidableEq α] {β : Type v} [Fintype α] [Fintype β] [DecidableEq β] (e : Perm α) (f : α ↪ β) : sign (e.viaFintypeEmbedding f) = sign e

def Equiv.Perm.ofSign {α : Type u} [DecidableEq α] [Fintype α] (s : ℤˣ) : Finset (Perm α)

Permutations of a given sign.

@[simp]

theorem Equiv.Perm.mem_ofSign {α : Type u} [DecidableEq α] [Fintype α] {s : ℤˣ} {σ : Perm α} : σ ∈ ofSign s ↔ sign σ = s

theorem Equiv.Perm.ofSign_disjoint {α : Type u} [DecidableEq α] [Fintype α] : _root_.Disjoint (ofSign 1) (ofSign (-1))

theorem Equiv.Perm.ofSign_disjUnion {α : Type u} [DecidableEq α] [Fintype α] : (ofSign 1).disjUnion (ofSign (-1)) ⋯ = Finset.univ