mathlib documentation

group_theory.​perm.​sign

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}

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

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 α

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

Equations
theorem equiv.​perm.​swap_mul_eq_mul_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) (x 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}

Equations
def equiv.​perm.​swap_factors {α : Type u} [decidable_eq α] [fintype α] [decidable_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}

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 zequiv.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} :

Equations
@[simp]

def equiv.​perm.​sign_bij_aux {n : } :
equiv.perm (fin n)(Σ (a : fin n), fin n)(Σ (a : fin n), fin n)

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)

theorem equiv.​perm.​sign_aux_swap {n : } {x y : fin n} :
x y(equiv.swap x y).sign_aux = -1

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

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]
theorem equiv.​perm.​sign_one {α : 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

Equations
theorem equiv.​perm.​is_cycle_swap {α : Type u} [decidable_eq α] [fintype α] {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} [decidable_eq α] [fintype α] (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} [decidable_eq α] [fintype α] (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} [decidable_eq α] [fintype α] {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} [decidable_eq α] [fintype α] {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 α] [_inst_2 _inst_3 : fintype α] {x y : α} :
x y(equiv.swap x y).support = {x, y}

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

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