group_theory.perm.sign - mathlib3 docs

source

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

setoid (equiv.perm α)

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

equiv.perm.mod_swap i j = {r := λ (σ τ : equiv.perm α), σ = τ ∨ σ = equiv.swap i j * τ, iseqv := _}

source

@[protected, instance]

def equiv.perm.r.decidable_rel {α : Type u_1} [fintype α] [decidable_eq α] (i j : α) :

decidable_rel setoid.r

Equations

equiv.perm.r.decidable_rel i j = λ (σ τ : equiv.perm α), or.decidable

source

theorem equiv.perm.perm_inv_on_of_perm_on_finset {α : Type u} {s : finset α} {f : equiv.perm α} (h : ∀ (x : α), x ∈ s → ⇑f x ∈ s) {y : α} (hy : y ∈ s) :

⇑f⁻¹ y ∈ s

source

theorem equiv.perm.perm_inv_maps_to_of_maps_to {α : Type u} (f : equiv.perm α) {s : set α} [finite ↥s] (h : set.maps_to ⇑f s s) :

set.maps_to ⇑f⁻¹ s s

source

@[simp]

theorem equiv.perm.perm_inv_maps_to_iff_maps_to {α : Type u} {f : equiv.perm α} {s : set α} [finite ↥s] :

set.maps_to ⇑f⁻¹ s s ↔ set.maps_to ⇑f s s

source

theorem equiv.perm.perm_inv_on_of_perm_on_finite {α : Type u} {f : equiv.perm α} {p : α → Prop} [finite {x // p x}] (h : ∀ (x : α), p x → p (⇑f x)) {x : α} (hx : p x) :

p (⇑f⁻¹ x)

source

@[reducible]

def equiv.perm.subtype_perm_of_fintype {α : Type u} (f : equiv.perm α) {p : α → Prop} [fintype {x // p x}] (h : ∀ (x : α), p x → p (⇑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.

source

@[simp]

theorem equiv.perm.subtype_perm_of_fintype_apply {α : Type u} (f : equiv.perm α) {p : α → Prop} [fintype {x // p x}] (h : ∀ (x : α), p x → p (⇑f x)) (x : {x // p x}) :

⇑(f.subtype_perm_of_fintype h) x = ⟨⇑f ↑x, _⟩

source

@[simp]

theorem equiv.perm.subtype_perm_of_fintype_one {α : Type u} (p : α → Prop) [fintype {x // p x}] (h : ∀ (x : α), p x → p (⇑1 x)) :

1.subtype_perm_of_fintype h = 1

source

theorem equiv.perm.perm_maps_to_inl_iff_maps_to_inr {m : Type u_1} {n : Type u_2} [finite m] [finite n] (σ : equiv.perm (m ⊕ n)) :

set.maps_to ⇑σ (set.range sum.inl) (set.range sum.inl) ↔ set.maps_to ⇑σ (set.range sum.inr) (set.range sum.inr)

source

theorem equiv.perm.mem_sum_congr_hom_range_of_perm_maps_to_inl {m : Type u_1} {n : Type u_2} [finite m] [finite n] {σ : equiv.perm (m ⊕ n)} (h : set.maps_to ⇑σ (set.range sum.inl) (set.range sum.inl)) :

σ ∈ (equiv.perm.sum_congr_hom m n).range

source

theorem equiv.perm.disjoint.order_of {α : Type u} {σ τ : equiv.perm α} (hστ : σ.disjoint τ) :

order_of (σ * τ) = (order_of σ).lcm (order_of τ)

source

theorem equiv.perm.disjoint.extend_domain {β : Type v} {α : Type u_1} {p : β → Prop} [decidable_pred p] (f : α ≃ subtype p) {σ τ : equiv.perm α} (h : σ.disjoint τ) :

(σ.extend_domain f).disjoint (τ.extend_domain f)

source

theorem equiv.perm.support_pow_coprime {α : Type u} [decidable_eq α] [fintype α] {σ : equiv.perm α} {n : ℕ} (h : n.coprime (order_of σ)) :

(σ ^ n).support = σ.support

source

def equiv.perm.swap_factors_aux {α : Type u} [decidable_eq α] (l : list α) (f : equiv.perm α) :

(∀ {x : α}, ⇑f x ≠ x → x ∈ 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

equiv.perm.swap_factors_aux (x :: l) = λ (f : equiv.perm α) (h : ∀ {x_1 : α}, ⇑f x_1 ≠ x_1 → x_1 ∈ x :: l), dite (x = ⇑f x) (λ (hfx : x = ⇑f x), equiv.perm.swap_factors_aux l f _) (λ (hfx : ¬x = ⇑f x), let m : {l // l.prod = equiv.swap x (⇑f x) * f ∧ ∀ (g : equiv.perm α), g ∈ l → g.is_swap} := equiv.perm.swap_factors_aux l (equiv.swap x (⇑f x) * f) _ in ⟨equiv.swap x (⇑f x) :: m.val, _⟩)
equiv.perm.swap_factors_aux list.nil = λ (f : equiv.perm α) (h : ∀ {x : α}, ⇑f x ≠ x → x ∈ list.nil), ⟨list.nil (equiv.perm α), _⟩

source

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

f.swap_factors = equiv.perm.swap_factors_aux (finset.sort has_le.le finset.univ) f _

source

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

f.trunc_swap_factors = quotient.rec_on_subsingleton finset.univ.val (λ (l : list α) (h : ∀ (x : α), ⇑f x ≠ x → x ∈ ⟦l⟧), trunc.mk (equiv.perm.swap_factors_aux l f h)) _

source

theorem equiv.perm.swap_induction_on {α : Type u} [decidable_eq α] [finite α] {P : equiv.perm α → Prop} (f : equiv.perm α) :

P 1 → (∀ (f : equiv.perm α) (x y : α), x ≠ y → P f → P (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.

source

theorem equiv.perm.closure_is_swap {α : Type u} [decidable_eq α] [finite α] :

subgroup.closure {σ : equiv.perm α | σ.is_swap} = ⊤

source

theorem equiv.perm.swap_induction_on' {α : Type u} [decidable_eq α] [finite α] {P : equiv.perm α → Prop} (f : equiv.perm α) :

P 1 → (∀ (f : equiv.perm α) (x y : α), x ≠ y → P f → P (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.

source

theorem equiv.perm.is_conj_swap {α : Type u} [decidable_eq α] {w x y z : α} (hwx : w ≠ x) (hyz : y ≠ z) :

is_conj (equiv.swap w x) (equiv.swap y z)

source

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

equiv.perm.fin_pairs_lt n = finset.univ.sigma (λ (a : fin n), (finset.range ↑a).attach_fin _)

source

theorem equiv.perm.mem_fin_pairs_lt {n : ℕ} {a : Σ (a : fin n), fin n} :

a ∈ equiv.perm.fin_pairs_lt n ↔ a.snd < a.fst

source

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

a.sign_aux = (equiv.perm.fin_pairs_lt n).prod (λ (x : Σ (a : fin n), fin n), ite (⇑a x.fst ≤ ⇑a x.snd) (-1) 1)

source

@[simp]

theorem equiv.perm.sign_aux_one (n : ℕ) :

1.sign_aux = 1

source

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

f.sign_bij_aux a = dite (⇑f a.snd < ⇑f a.fst) (λ (hxa : ⇑f a.snd < ⇑f a.fst), ⟨⇑f a.fst, ⇑f a.snd⟩) (λ (hxa : ¬⇑f a.snd < ⇑f a.fst), ⟨⇑f a.snd, ⇑f a.fst⟩)

source

theorem equiv.perm.sign_bij_aux_inj {n : ℕ} {f : equiv.perm (fin n)} (a b : Σ (a : fin n), fin n) :

a ∈ equiv.perm.fin_pairs_lt n → b ∈ equiv.perm.fin_pairs_lt n → f.sign_bij_aux a = f.sign_bij_aux b → a = b

source

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

source

theorem equiv.perm.sign_bij_aux_mem {n : ℕ} {f : equiv.perm (fin n)} (a : Σ (a : fin n), fin n) :

a ∈ equiv.perm.fin_pairs_lt n → f.sign_bij_aux a ∈ equiv.perm.fin_pairs_lt n

source

@[simp]

theorem equiv.perm.sign_aux_inv {n : ℕ} (f : equiv.perm (fin n)) :

f⁻¹.sign_aux = f.sign_aux

source

theorem equiv.perm.sign_aux_mul {n : ℕ} (f g : equiv.perm (fin n)) :

(f * g).sign_aux = f.sign_aux * g.sign_aux

source

theorem equiv.perm.sign_aux_swap {n : ℕ} {x y : fin n} (hxy : x ≠ y) :

(equiv.swap x y).sign_aux = -1

source

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

equiv.perm.sign_aux2 (x :: l) f = ite (x = ⇑f x) (equiv.perm.sign_aux2 l f) (-equiv.perm.sign_aux2 l (equiv.swap x (⇑f x) * f))
equiv.perm.sign_aux2 list.nil f = 1

source

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 ≠ x → x ∈ l) :

equiv.perm.sign_aux ((e.symm.trans f).trans e) = equiv.perm.sign_aux2 l f

source

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

f.sign_aux3 = quotient.hrec_on s (λ (l : list α) (h : ∀ (x : α), x ∈ ⟦l⟧), equiv.perm.sign_aux2 l f) _

source

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

source

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

equiv.perm α →* ℤ ˣ

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

equiv.perm.sign = monoid_hom.mk' (λ (f : equiv.perm α), f.sign_aux3 finset.mem_univ) equiv.perm.sign._proof_1

source

@[simp]

theorem equiv.perm.sign_mul {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) :

⇑equiv.perm.sign (f * g) = ⇑equiv.perm.sign f * ⇑equiv.perm.sign g

source

@[simp]

theorem equiv.perm.sign_trans {α : Type u} [decidable_eq α] [fintype α] (f g : equiv.perm α) :

⇑equiv.perm.sign (equiv.trans f g) = ⇑equiv.perm.sign g * ⇑equiv.perm.sign f

source

@[simp]

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

⇑equiv.perm.sign 1 = 1

source

@[simp]

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

⇑equiv.perm.sign (equiv.refl α) = 1

source

@[simp]

theorem equiv.perm.sign_inv {α : Type u} [decidable_eq α] [fintype α] (f : equiv.perm α) :

⇑equiv.perm.sign f⁻¹ = ⇑equiv.perm.sign f

source

@[simp]

theorem equiv.perm.sign_symm {α : Type u} [decidable_eq α] [fintype α] (e : equiv.perm α) :

⇑equiv.perm.sign (equiv.symm e) = ⇑equiv.perm.sign e

source

theorem equiv.perm.sign_swap {α : Type u} [decidable_eq α] [fintype α] {x y : α} (h : x ≠ y) :

⇑equiv.perm.sign (equiv.swap x y) = -1

source

@[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)

source

theorem equiv.perm.is_swap.sign_eq {α : Type u} [decidable_eq α] [fintype α] {f : equiv.perm α} (h : f.is_swap) :

⇑equiv.perm.sign f = -1

source

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

equiv.perm.sign_aux3 ((e.symm.trans f).trans e) ht = f.sign_aux3 hs

source

@[simp]

theorem equiv.perm.sign_symm_trans_trans {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm α) (e : α ≃ β) :

⇑equiv.perm.sign ((e.symm.trans f).trans e) = ⇑equiv.perm.sign f

source

@[simp]

theorem equiv.perm.sign_trans_trans_symm {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (f : equiv.perm β) (e : α ≃ β) :

⇑equiv.perm.sign ((e.trans f).trans e.symm) = ⇑equiv.perm.sign f

source

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

⇑equiv.perm.sign l.prod = (-1) ^ l.length

source

theorem equiv.perm.sign_surjective (α : Type u) [decidable_eq α] [fintype α] [nontrivial α] :

function.surjective ⇑equiv.perm.sign

source

theorem equiv.perm.eq_sign_of_surjective_hom {α : Type u} [decidable_eq α] [fintype α] {s : equiv.perm α →* ℤ ˣ} (hs : function.surjective ⇑s) :

s = equiv.perm.sign

source

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 ≠ x → p x) :

⇑equiv.perm.sign (f.subtype_perm h₁) = ⇑equiv.perm.sign f

source

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

⇑equiv.perm.sign f = ⇑equiv.perm.sign g

source

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

⇑equiv.perm.sign f = ⇑equiv.perm.sign g

source

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

(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 σ.

source

@[simp]

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

⇑equiv.perm.sign (equiv.perm.prod_extend_right a σ) = ⇑equiv.perm.sign σ

source

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

⇑equiv.perm.sign (equiv.prod_congr_right σ) = finset.univ.prod (λ (k : α), ⇑equiv.perm.sign (σ k))

source

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

⇑equiv.perm.sign (equiv.prod_congr_left σ) = finset.univ.prod (λ (k : α), ⇑equiv.perm.sign (σ k))

source

@[simp]

theorem equiv.perm.sign_perm_congr {α : Type u} {β : Type v} [decidable_eq α] [fintype α] [decidable_eq β] [fintype β] (e : α ≃ β) (p : equiv.perm α) :

⇑equiv.perm.sign (⇑(e.perm_congr) p) = ⇑equiv.perm.sign p

source

@[simp]

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

⇑equiv.perm.sign (σa.sum_congr σb) = ⇑equiv.perm.sign σa * ⇑equiv.perm.sign σb

source

@[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}) :

⇑equiv.perm.sign (ep.subtype_congr en) = ⇑equiv.perm.sign ep * ⇑equiv.perm.sign en

source

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

⇑equiv.perm.sign (e.extend_domain f) = ⇑equiv.perm.sign e

source

@[simp]

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

⇑equiv.perm.sign (⇑equiv.perm.of_subtype f) = ⇑equiv.perm.sign f

mathlib3 documentation

Sign of a permutation #