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/*.
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 := _}
@[protected, instance]
Equations
- equiv.perm.r.decidable_rel i j = λ (σ τ : equiv.perm α), or.decidable
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) :
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] :
set.maps_to ⇑f⁻¹ s s ↔ set.maps_to ⇑f s 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 x → p (⇑f x))
{x : α}
(hx : p x) :
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.
@[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}) :
@[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
theorem
equiv.perm.perm_maps_to_inl_iff_maps_to_inr
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype n]
(σ : equiv.perm (m ⊕ n)) :
theorem
equiv.perm.mem_sum_congr_hom_range_of_perm_maps_to_inl
{m : Type u_1}
{n : Type u_2}
[fintype m]
[fintype 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
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)
theorem
equiv.perm.support_pow_coprime
{α : Type u}
[decidable_eq α]
[fintype α]
{σ : equiv.perm α}
{n : ℕ}
(h : n.coprime (order_of σ)) :
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 α), _⟩
def
equiv.perm.swap_factors
{α : Type u}
[decidable_eq α]
[fintype α]
[linear_order α]
(f : equiv.perm α) :
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
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)) _
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 ≠ 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.
theorem
equiv.perm.closure_is_swap
{α : Type u}
[decidable_eq α]
[fintype α] :
subgroup.closure {σ : equiv.perm α | σ.is_swap} = ⊤
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 ≠ 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.
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)
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 _)
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₂
sign_bij_aux f ⟨a, b⟩ returns the pair consisting of f a and f b in decreasing order.
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
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
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
@[simp]
theorem
equiv.perm.sign_aux_swap
{n : ℕ}
{x y : fin n}
(hxy : x ≠ y) :
(equiv.swap x y).sign_aux = -1
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
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
def
equiv.perm.sign_aux3
{α : Type u}
[decidable_eq α]
[fintype α]
(f : equiv.perm α)
{s : multiset α} :
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) _
theorem
equiv.perm.sign_aux3_mul_and_swap
{α : Type u}
[decidable_eq α]
[fintype α]
(f g : equiv.perm α)
(s : multiset α)
(hs : ∀ (x : α), x ∈ s) :
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
@[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
@[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
@[simp]
@[simp]
theorem
equiv.perm.sign_refl
{α : Type u}
[decidable_eq α]
[fintype α] :
⇑equiv.perm.sign (equiv.refl α) = 1
@[simp]
@[simp]
theorem
equiv.perm.sign_swap
{α : Type u}
[decidable_eq α]
[fintype α]
{x y : α}
(h : x ≠ y) :
⇑equiv.perm.sign (equiv.swap x y) = -1
@[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) :
⇑equiv.perm.sign f = -1
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 : α ≃ β) :
⇑equiv.perm.sign ((e.symm.trans f).trans e) = ⇑equiv.perm.sign f
@[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
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.eq_sign_of_surjective_hom
{α : Type u}
[decidable_eq α]
[fintype α]
{s : equiv.perm α →* ℤˣ}
(hs : function.surjective ⇑s) :
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
@[simp]
theorem
equiv.perm.sign_of_subtype
{α : Type u}
[decidable_eq α]
[fintype α]
{p : α → Prop}
[decidable_pred p]
(f : equiv.perm (subtype p)) :
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) :
(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 σ.
@[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 β) :
⇑equiv.perm.sign (equiv.prod_congr_right σ) = ∏ (k : α), ⇑equiv.perm.sign (σ k)
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 σ) = ∏ (k : α), ⇑equiv.perm.sign (σ k)
@[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
@[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
@[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
@[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) :