mathlib documentation

group_theory.perm.sign

Sign of a permutation #

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

This file also contains miscellaneous lemmas about equiv.perm and equiv.swap, building on top of those in data/equiv/basic and other files in group_theory/perm/*.

def equiv.perm.mod_swap {α : Type u} [decidable_eq α] (i j : α) :

mod_swap 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
@[protected, instance]
def equiv.perm.r.decidable_rel {α : Type u_1} [fintype α] [decidable_eq α] (i j : α) :
Equations
theorem equiv.perm.perm_inv_on_of_perm_on_finset {α : Type u} {s : finset α} {f : equiv.perm α} (h : ∀ (x : α), x sf x s) {y : α} (hy : y s) :
theorem equiv.perm.perm_inv_maps_to_of_maps_to {α : Type u} (f : equiv.perm α) {s : set α} [fintype s] (h : set.maps_to f s s) :
@[simp]
theorem equiv.perm.perm_inv_maps_to_iff_maps_to {α : Type u} {f : equiv.perm α} {s : set α} [fintype s] :
theorem equiv.perm.perm_inv_on_of_perm_on_fintype {α : Type u} {f : equiv.perm α} {p : α → Prop} [fintype {x // p x}] (h : ∀ (x : α), p xp (f x)) {x : α} (hx : p x) :
p (f⁻¹ x)
def equiv.perm.subtype_perm_of_fintype {α : Type u} (f : equiv.perm α) {p : α → Prop} [fintype {x // p x}] (h : ∀ (x : α), p xp (f x)) :
equiv.perm {x // p x}

If the permutation f maps {x // p x} into itself, then this returns the permutation on {x // p x} induced by f. Note that the h hypothesis is weaker than for equiv.perm.subtype_perm.

@[simp]
theorem equiv.perm.subtype_perm_of_fintype_apply {α : Type u} (f : equiv.perm α) {p : α → Prop} [fintype {x // p x}] (h : ∀ (x : α), p xp (f x)) (x : {x // p x}) :
@[simp]
theorem equiv.perm.subtype_perm_of_fintype_one {α : Type u} (p : α → Prop) [fintype {x // p x}] (h : ∀ (x : α), p xp (1 x)) :
theorem equiv.perm.disjoint.order_of {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :
order_of * τ) = (order_of σ).lcm (order_of τ)
theorem equiv.perm.disjoint.extend_domain {β : Type v} {α : Type u_1} {p : β → Prop} [decidable_pred p] (f : α subtype p) {σ τ : equiv.perm α} (h : σ.disjoint τ) :
theorem equiv.perm.support_pow_coprime {α : Type u} [decidable_eq α] [fintype α] {σ : equiv.perm α} {n : } (h : n.coprime (order_of σ)) :
^ n).support = σ.support
def equiv.perm.swap_factors_aux {α : Type u} [decidable_eq α] (l : list α) (f : equiv.perm α) :
(∀ {x : α}, f x xx l){l // l.prod = f ∀ (g : equiv.perm α), g l → g.is_swap}

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
def equiv.perm.swap_factors {α : Type u} [decidable_eq α] [fintype α] [linear_order α] (f : equiv.perm α) :
{l // l.prod = f ∀ (g : equiv.perm α), g l → g.is_swap}

swap_factors 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 trunc_swap_factors can be used.

Equations
def equiv.perm.trunc_swap_factors {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :
trunc {l // l.prod = f ∀ (g : equiv.perm α), g l → g.is_swap}

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

Equations
theorem equiv.perm.swap_induction_on {α : Type u} [decidable_eq α] [fintype α] {P : equiv.perm α → Prop} (f : equiv.perm α) :
P 1(∀ (f : equiv.perm α) (x y : α), x yP fP ((equiv.swap x y) * 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.closure_is_swap {α : Type u} [decidable_eq α] [fintype α] :
theorem equiv.perm.swap_induction_on' {α : Type u} [decidable_eq α] [fintype α] {P : equiv.perm α → Prop} (f : equiv.perm α) :
P 1(∀ (f : equiv.perm α) (x y : α), x yP fP (f * equiv.swap x y))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.is_conj_swap {α : Type u} [decidable_eq α] {w x y z : α} (hwx : w x) (hyz : y z) :
def equiv.perm.fin_pairs_lt (n : ) :
finset (Σ (a : fin n), fin n)

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

Equations
theorem equiv.perm.mem_fin_pairs_lt {n : } {a : Σ (a : fin n), fin n} :
def equiv.perm.sign_aux {n : } (a : equiv.perm (fin n)) :

sign_aux σ 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
@[simp]
theorem equiv.perm.sign_aux_one (n : ) :
def equiv.perm.sign_bij_aux {n : } (f : equiv.perm (fin n)) (a : Σ (a : fin n), fin n) :
Σ (a : fin n), fin n

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

Equations
theorem equiv.perm.sign_bij_aux_inj {n : } {f : equiv.perm (fin n)} (a b : Σ (a : fin n), fin n) :
theorem equiv.perm.sign_bij_aux_surj {n : } {f : equiv.perm (fin n)} (a : Σ (a : fin n), fin n) (H : a equiv.perm.fin_pairs_lt n) :
∃ (b : Σ (a : fin n), fin n) (H : b equiv.perm.fin_pairs_lt n), a = f.sign_bij_aux b
@[simp]
theorem equiv.perm.sign_aux_mul {n : } (f g : equiv.perm (fin n)) :
theorem equiv.perm.sign_aux_swap {n : } {x y : fin n} (hxy : x y) :
def equiv.perm.sign_aux2 {α : Type u} [decidable_eq α] :
list αequiv.perm αˣ

When the list l : list α contains all nonfixed points of the permutation f : perm α, sign_aux2 l f recursively calculates the sign of f.

Equations
theorem equiv.perm.sign_aux_eq_sign_aux2 {α : Type u} [decidable_eq α] {n : } (l : list α) (f : equiv.perm α) (e : α fin n) (h : ∀ (x : α), f x xx l) :
def equiv.perm.sign_aux3 {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) {s : multiset α} :
(∀ (x : α), x s)ˣ

When the multiset s : multiset α contains all nonfixed points of the permutation f : perm α, sign_aux2 f _ recursively calculates the sign of f.

Equations
theorem equiv.perm.sign_aux3_mul_and_swap {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) (s : multiset α) (hs : ∀ (x : α), x s) :
(f * g).sign_aux3 hs = (f.sign_aux3 hs) * g.sign_aux3 hs ∀ (x y : α), x y(equiv.swap x y).sign_aux3 hs = -1
def equiv.perm.sign {α : Type u} [decidable_eq α] [fintype α] :

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
@[simp]
@[simp]
theorem equiv.perm.sign_one {α : Type u} [decidable_eq α] [fintype α] :
@[simp]
theorem equiv.perm.sign_refl {α : Type u} [decidable_eq α] [fintype α] :
@[simp]
@[simp]
theorem equiv.perm.sign_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (h : x y) :
@[simp]
theorem equiv.perm.sign_swap' {α : Type u} [decidable_eq α] [fintype α] {x y : α} :
equiv.perm.sign (equiv.swap x y) = ite (x = y) 1 (-1)
theorem equiv.perm.is_swap.sign_eq {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f.is_swap) :
theorem equiv.perm.sign_aux3_symm_trans_trans {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (e : α β) {s : multiset α} {t : multiset β} (hs : ∀ (x : α), x s) (ht : ∀ (x : β), x t) :
@[simp]
theorem equiv.perm.sign_symm_trans_trans {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (e : α β) :
@[simp]
theorem equiv.perm.sign_trans_trans_symm {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm β) (e : α β) :
theorem equiv.perm.sign_prod_list_swap {α : Type u} [decidable_eq α] [fintype α] {l : list (equiv.perm α)} (hl : ∀ (g : equiv.perm α), g l → g.is_swap) :
theorem equiv.perm.sign_subtype_perm {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) {p : α → Prop} [decidable_pred p] (h₁ : ∀ (x : α), p x p (f x)) (h₂ : ∀ (x : α), f x xp x) :
theorem equiv.perm.sign_eq_sign_of_equiv {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (g : equiv.perm β) (e : α β) (h : ∀ (x : α), e (f x) = g (e x)) :
theorem equiv.perm.sign_bij {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] {f : equiv.perm α} {g : equiv.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)) :
theorem equiv.perm.prod_prod_extend_right {β : Type v} {α : Type u_1} [decidable_eq α] (σ : α → equiv.perm β) {l : list α} (hl : l.nodup) (mem_l : ∀ (a : α), a l) :

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

@[simp]
theorem equiv.perm.sign_prod_extend_right {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (a : α) (σ : equiv.perm β) :
theorem equiv.perm.sign_prod_congr_right {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (σ : α → equiv.perm β) :
theorem equiv.perm.sign_prod_congr_left {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (σ : α → equiv.perm β) :
@[simp]
theorem equiv.perm.sign_perm_congr {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (e : α β) (p : equiv.perm α) :
@[simp]
theorem equiv.perm.sign_sum_congr {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (σa : equiv.perm α) (σb : equiv.perm β) :
@[simp]
theorem equiv.perm.sign_subtype_congr {α : Type u} [decidable_eq α] [fintype α] {p : α → Prop} [decidable_pred p] (ep : equiv.perm {a // p a}) (en : equiv.perm {a // ¬p a}) :
@[simp]
theorem equiv.perm.sign_extend_domain {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (e : equiv.perm α) {p : β → Prop} [decidable_pred p] (f : α subtype p) :