mathlib documentation

group_theory.perm.sign

def equiv.perm.subtype_perm {α : Type u} (f : equiv.perm α) {p : α → Prop} :
(∀ (x : α), p x p (f x))equiv.perm {x // p x}

If the permutation f fixes the subtype {x // p x}, then this returns the permutation on {x // p x} induced by f.

Equations
@[simp]
theorem equiv.perm.subtype_perm_one {α : Type u} (p : α → Prop) (h : ∀ (x : α), p x p (1 x)) :

def equiv.perm.of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] :

The inclusion map of permutations on a subtype of α into permutations of α, fixing the other points.

Equations
theorem equiv.perm.eq_inv_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :
x = f⁻¹ y f x = y

theorem equiv.perm.inv_eq_iff_eq {α : Type u} {f : equiv.perm α} {x y : α} :
f⁻¹ x = y x = f y

def equiv.perm.disjoint {α : Type u} :
equiv.perm αequiv.perm α → Prop

Two permutations f and g are disjoint if their supports are disjoint, i.e., every element is fixed either by f, or by g.

Equations
theorem equiv.perm.disjoint.symm {α : Type u} {f g : equiv.perm α} :
f.disjoint gg.disjoint f

theorem equiv.perm.disjoint_comm {α : Type u} {f g : equiv.perm α} :

theorem equiv.perm.disjoint_mul_comm {α : Type u} {f g : equiv.perm α} :
f.disjoint gf * g = g * f

@[simp]
theorem equiv.perm.disjoint_one_left {α : Type u} (f : equiv.perm α) :

@[simp]
theorem equiv.perm.disjoint_one_right {α : Type u} (f : equiv.perm α) :

theorem equiv.perm.disjoint_mul_left {α : Type u} {f g h : equiv.perm α} :
f.disjoint hg.disjoint h(f * g).disjoint h

theorem equiv.perm.disjoint_mul_right {α : Type u} {f g h : equiv.perm α} :
f.disjoint gf.disjoint hf.disjoint (g * h)

theorem equiv.perm.disjoint_prod_right {α : Type u} {f : equiv.perm α} (l : list (equiv.perm α)) :
(∀ (g : equiv.perm α), g lf.disjoint g)f.disjoint l.prod

theorem equiv.perm.disjoint_prod_perm {α : Type u} {l₁ l₂ : list (equiv.perm α)} :
list.pairwise equiv.perm.disjoint l₁l₁ ~ l₂l₁.prod = l₂.prod

theorem equiv.perm.of_subtype_subtype_perm {α : Type u} {f : equiv.perm α} {p : α → Prop} [decidable_pred p] (h₁ : ∀ (x : α), p x p (f x)) :
(∀ (x : α), f x xp x)equiv.perm.of_subtype (f.subtype_perm h₁) = f

theorem equiv.perm.of_subtype_apply_of_not_mem {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) {x : α} :

theorem equiv.perm.mem_iff_of_subtype_apply_mem {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) (x : α) :

@[simp]
theorem equiv.perm.subtype_perm_of_subtype {α : Type u} {p : α → Prop} [decidable_pred p] (f : equiv.perm (subtype p)) :

theorem equiv.perm.pow_apply_eq_self_of_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hfx : f x = x) (n : ) :
(f ^ n) x = x

theorem equiv.perm.gpow_apply_eq_self_of_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hfx : f x = x) (n : ) :
(f ^ n) x = x

theorem equiv.perm.pow_apply_eq_of_apply_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hffx : f (f x) = x) (n : ) :
(f ^ n) x = x (f ^ n) x = f x

theorem equiv.perm.gpow_apply_eq_of_apply_apply_eq_self {α : Type u} {f : equiv.perm α} {x : α} (hffx : f (f x) = x) (i : ) :
(f ^ i) x = x (f ^ i) x = f x

def equiv.perm.support {α : Type u} [decidable_eq α] [fintype α] :
equiv.perm αfinset α

The finset of nonfixed points of a permutation.

Equations
@[simp]
theorem equiv.perm.mem_support {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
x f.support f x x

def equiv.perm.is_swap {α : Type u} [decidable_eq α] :
equiv.perm α → Prop

f.is_swap indicates that the permutation f is a transposition of two elements.

Equations
theorem equiv.perm.swap_mul_eq_mul_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :
(equiv.swap x y) * f = f * equiv.swap (f⁻¹ x) (f⁻¹ y)

theorem equiv.perm.mul_swap_eq_swap_mul {α : Type u} [decidable_eq α] (f : equiv.perm α) (x y : α) :
f * equiv.swap x y = (equiv.swap (f x) (f y)) * f

@[simp]
theorem equiv.perm.swap_mul_self_mul {α : Type u} [decidable_eq α] (i j : α) (σ : equiv.perm α) :
(equiv.swap i j) * (equiv.swap i j) * σ = σ

Multiplying a permutation with swap i j twice gives the original permutation.

This specialization of swap_mul_self is useful when using cosets of permutations.

theorem equiv.perm.swap_mul_eq_iff {α : Type u} [decidable_eq α] {i j : α} {σ : equiv.perm α} :
(equiv.swap i j) * σ = σ i = j

theorem equiv.perm.is_swap_of_subtype {α : Type u} [decidable_eq α] {p : α → Prop} [decidable_pred p] {f : equiv.perm (subtype p)} :

theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u} [decidable_eq α] {f : equiv.perm α} {x y : α} :
((equiv.swap x (f x)) * f) y yf y y y x

theorem equiv.perm.support_swap_mul_eq {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
f (f x) x((equiv.swap x (f x)) * f).support = f.support.erase x

theorem equiv.perm.card_support_swap_mul {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
f x x((equiv.swap x (f x)) * f).support.card < f.support.card

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

theorem equiv.perm.swap_mul_swap_mul_swap {α : Type u} [decidable_eq α] {x y z : α} :
x yx z((equiv.swap y z) * equiv.swap x y) * equiv.swap y z = equiv.swap z x

theorem equiv.perm.is_conj_swap {α : Type u} [decidable_eq α] {w x y z : α} :
w xy zis_conj (equiv.swap w x) (equiv.swap 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} :

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 : } :
equiv.perm (fin n)(Σ (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) :
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} :
x y(equiv.swap x y).sign_aux = -1

def equiv.perm.sign_aux2 {α : Type u} [decidable_eq α] :
list αequiv.perm αunits

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) :
(∀ (x : α), f x xx l)equiv.perm.sign_aux ((e.symm.trans f).trans e) = equiv.perm.sign_aux2 l f

def equiv.perm.sign_aux3 {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) {s : multiset α} :
(∀ (x : α), x s)units

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]

theorem equiv.perm.sign_swap {α : Type u} [decidable_eq α] [fintype α] {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.sign_eq_of_is_swap {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} :

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) :

theorem equiv.perm.sign_symm_trans_trans {α : 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 α)} :
(∀ (g : equiv.perm α), g l → g.is_swap)equiv.perm.sign l.prod = (-1) ^ l.length

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)) :
(∀ (x : α), f x xp x)equiv.perm.sign (f.subtype_perm h₁) = equiv.perm.sign f

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 : α β) :
(∀ (x : α), e (f x) = g (e x))equiv.perm.sign f = equiv.perm.sign g

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 → β) :
(∀ (x : α) (hx : f x x) (hx' : f (f x) f x), i (f x) hx' = g (i x hx))(∀ (x₁ x₂ : α) (hx₁ : f x₁ x₁) (hx₂ : f x₂ x₂), i x₁ hx₁ = i x₂ hx₂x₁ = x₂)(∀ (y : β), g y y(∃ (x : α) (hx : f x x), i x hx = y))equiv.perm.sign f = equiv.perm.sign g

def equiv.perm.is_cycle {β : Type v} :
equiv.perm β → Prop

A permutation is a cycle when any two nonfixed points of the permutation are related by repeated application of the permutation.

Equations
theorem equiv.perm.is_cycle_swap {α : Type u_1} [decidable_eq α] {x y : α} :
x y(equiv.swap x y).is_cycle

theorem equiv.perm.is_cycle_inv {β : Type v} {f : equiv.perm β} :

theorem equiv.perm.exists_gpow_eq_of_is_cycle {β : Type v} {f : equiv.perm β} (hf : f.is_cycle) {x y : β} :
f x xf y y(∃ (i : ), (f ^ i) x = y)

theorem equiv.perm.is_cycle_swap_mul_aux₁ {α : Type u_1} [decidable_eq α] (n : ) {b x : α} {f : equiv.perm α} :
((equiv.swap x (f x)) * f) b b(f ^ n) (f x) = b(∃ (i : ), (((equiv.swap x (f x)) * f) ^ i) (f x) = b)

theorem equiv.perm.is_cycle_swap_mul_aux₂ {α : Type u_1} [decidable_eq α] (n : ) {b x : α} {f : equiv.perm α} :
((equiv.swap x (f x)) * f) b b(f ^ n) (f x) = b(∃ (i : ), (((equiv.swap x (f x)) * f) ^ i) (f x) = b)

theorem equiv.perm.eq_swap_of_is_cycle_of_apply_apply_eq_self {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} :
f x xf (f x) = xf = equiv.swap x (f x)

theorem equiv.perm.is_cycle_swap_mul {α : Type u_1} [decidable_eq α] {f : equiv.perm α} (hf : f.is_cycle) {x : α} :
f x xf (f x) x((equiv.swap x (f x)) * f).is_cycle

@[simp]
theorem equiv.perm.support_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} :
x y(equiv.swap x y).support = {x, y}

theorem equiv.perm.card_support_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} :
x y(equiv.swap x y).support.card = 2

theorem equiv.perm.sign_cycle {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} :

theorem equiv.perm.prod_prod_extend_right {β : Type v} {α : Type u_1} [decidable_eq α] (σ : α → equiv.perm β) {l : list α} :
l.nodup(∀ (a : α), a l)(list.map (λ (a : α), equiv.perm.prod_extend_right a (σ a)) l).prod = equiv.prod_congr_right σ

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

theorem equiv.perm.sign_prod_extend_right {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [fintype β] (a : α) (σ : equiv.perm β) :

theorem equiv.perm.sign_prod_congr_right {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [fintype β] (σ : α → equiv.perm β) :

theorem equiv.perm.sign_prod_congr_left {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [fintype β] (σ : α → equiv.perm β) :