mathlib documentation

group_theory.perm.sign

Sign of a permutation #

The main definition of this file is equiv.perm.sign, associating a units 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 data/equiv/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
@[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)) :
def equiv.perm.disjoint {α : Type u} (f g : 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 α} (h : f.disjoint g) :
f * 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 α} (H1 : f.disjoint h) (H2 : g.disjoint h) :
(f * g).disjoint h
theorem equiv.perm.disjoint.mul_right {α : Type u} {f g h : equiv.perm α} (H1 : f.disjoint g) (H2 : f.disjoint h) :
f.disjoint (g * h)
theorem equiv.perm.disjoint_prod_right {α : Type u} {f : equiv.perm α} (l : list (equiv.perm α)) (h : ∀ (g : equiv.perm α), g lf.disjoint g) :
theorem equiv.perm.disjoint_prod_perm {α : Type u} {l₁ l₂ : list (equiv.perm α)} (hl : list.pairwise equiv.perm.disjoint l₁) (hp : l₁ ~ l₂) :
l₁.prod = l₂.prod
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
theorem equiv.perm.disjoint.mul_apply_eq_iff {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) {a : α} :
(σ * τ) a = a σ a = a τ a = a
theorem equiv.perm.disjoint.mul_eq_one_iff {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :
σ * τ = 1 σ = 1 τ = 1
theorem equiv.perm.disjoint.gpow_disjoint_gpow {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ) :
^ m).disjoint ^ n)
theorem equiv.perm.disjoint.pow_disjoint_pow {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) (m n : ) :
^ m).disjoint ^ n)
theorem equiv.perm.disjoint.order_of {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :
order_of * τ) = (order_of σ).lcm (order_of τ)
def equiv.perm.support {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :

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
@[simp]
theorem equiv.perm.support_eq_empty_iff {α : Type u} [decidable_eq α] [fintype α] {σ : equiv.perm α} :
σ.support = σ = 1
@[simp]
theorem equiv.perm.support_one {α : Type u} [decidable_eq α] [fintype α] :
theorem equiv.perm.support_mul_le {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) :
theorem equiv.perm.exists_mem_support_of_mem_support_prod {α : Type u} [decidable_eq α] [fintype α] {l : list (equiv.perm α)} {x : α} (hx : x l.prod.support) :
∃ (f : equiv.perm α), f l x f.support
theorem equiv.perm.support_pow_le {α : Type u} [decidable_eq α] [fintype α] (σ : equiv.perm α) (n : ) :
^ n).support σ.support
@[simp]
theorem equiv.perm.support_inv {α : Type u} [decidable_eq α] [fintype α] (σ : equiv.perm α) :
@[simp]
theorem equiv.perm.apply_mem_support {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} :
def equiv.perm.is_swap {α : Type u} [decidable_eq α] (f : equiv.perm α) :
Prop

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

Equations
theorem equiv.perm.is_swap.of_subtype_is_swap {α : Type u} [decidable_eq α] {p : α → Prop} [decidable_pred p] {f : equiv.perm (subtype p)} (h : f.is_swap) :
theorem equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self {α : Type u} [decidable_eq α] {f : equiv.perm α} {x y : α} (hy : ((equiv.swap x (f x)) * f) y y) :
f y y y x
theorem equiv.perm.support_swap_mul_eq {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hffx : f (f x) x) :
((equiv.swap x (f x)) * f).support = f.support.erase x
@[simp]
theorem equiv.perm.card_support_eq_zero {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card = 0 f = 1
theorem equiv.perm.one_lt_card_support_of_ne_one {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f 1) :
theorem equiv.perm.card_support_ne_one {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :
@[simp]
theorem equiv.perm.card_support_le_one {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} :
f.support.card 1 f = 1
theorem equiv.perm.two_le_card_support_of_ne_one {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f 1) :
theorem equiv.perm.card_support_swap_mul {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} {x : α} (hx : f x x) :
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.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 α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) (h : ∀ (x : α), f x xx l) :
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]
@[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)) :
@[simp]
theorem equiv.perm.support_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (hxy : x y) :
(equiv.swap x y).support = {x, y}
theorem equiv.perm.card_support_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (hxy : x y) :
@[simp]
theorem equiv.perm.card_support_eq_two {α : 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 α} (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) :
theorem equiv.perm.disjoint.disjoint_support {α : Type u} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.disjoint.support_mul {α : Type u} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.disjoint.card_support_mul {α : Type u} [decidable_eq α] [fintype α] {f g : equiv.perm α} (h : f.disjoint g) :
theorem equiv.perm.disjoint_prod_list_of_disjoint {β : Type v} [fintype β] {f : equiv.perm β} {l : list (equiv.perm β)} (h : ∀ (g : equiv.perm β), g lf.disjoint g) :
def alternating_subgroup (α : Type u) [fintype α] [decidable_eq α] :

The alternating group on a finite type, realized as a subgroup of equiv.perm. For $A_n$, use alternating_subgroup (fin n).

Equations
@[simp]