def
equiv.perm.subtype_perm
{α : Type u}
(f : equiv.perm α)
{p : α → Prop} :
(∀ (x : α), p x ↔ p (⇑f x)) → equiv.perm {x // p x}
@[simp]
theorem
equiv.perm.subtype_perm_one
{α : Type u}
(p : α → Prop)
(h : ∀ (x : α), p x ↔ p (⇑1 x)) :
1.subtype_perm h = 1
def
equiv.perm.of_subtype
{α : Type u}
{p : α → Prop}
[decidable_pred p] :
equiv.perm (subtype p) →* equiv.perm α
Equations
Two permutations f and g are disjoint if their supports are disjoint, i.e.,
every element is fixed either by f, or by g.
@[simp]
@[simp]
theorem
equiv.perm.disjoint_prod_right
{α : Type u}
{f : equiv.perm α}
(l : list (equiv.perm α)) :
(∀ (g : equiv.perm α), g ∈ l → f.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 ≠ x → p 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 : α} :
¬p x → ⇑(⇑equiv.perm.of_subtype f) x = x
theorem
equiv.perm.mem_iff_of_subtype_apply_mem
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(f : equiv.perm (subtype p))
(x : α) :
p x ↔ p (⇑(⇑equiv.perm.of_subtype f) x)
@[simp]
theorem
equiv.perm.subtype_perm_of_subtype
{α : Type u}
{p : α → Prop}
[decidable_pred p]
(f : equiv.perm (subtype p)) :
(⇑equiv.perm.of_subtype f).subtype_perm _ = f
theorem
equiv.perm.pow_apply_eq_self_of_apply_eq_self
{α : Type u}
{f : equiv.perm α}
{x : α}
(hfx : ⇑f x = x)
(n : ℕ) :
theorem
equiv.perm.gpow_apply_eq_self_of_apply_eq_self
{α : Type u}
{f : equiv.perm α}
{x : α}
(hfx : ⇑f x = x)
(n : ℤ) :
Equations
- f.support = finset.filter (λ (x : α), ⇑f x ≠ x) finset.univ
@[simp]
theorem
equiv.perm.mem_support
{α : Type u}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x : α} :
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)} :
f.is_swap → (⇑equiv.perm.of_subtype f).is_swap
theorem
equiv.perm.ne_and_ne_of_swap_mul_apply_ne_self
{α : Type u}
[decidable_eq α]
{f : equiv.perm α}
{x y : α} :
theorem
equiv.perm.support_swap_mul_eq
{α : Type u}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x : α} :
theorem
equiv.perm.card_support_swap_mul
{α : Type u}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
{x : α} :
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 α]
[decidable_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
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
theorem
equiv.perm.swap_mul_swap_mul_swap
{α : Type u}
[decidable_eq α]
{x y z : α} :
x ≠ y → x ≠ 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 ≠ x → 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.val).attach_fin _)
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) :
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]
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) :
(∀ (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 α} :
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]
@[simp]
theorem
equiv.perm.sign_refl
{α : Type u}
[decidable_eq α]
[fintype α] :
⇑equiv.perm.sign (equiv.refl α) = 1
@[simp]
theorem
equiv.perm.sign_swap
{α : Type u}
[decidable_eq α]
[fintype α]
{x y : α} :
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.sign_eq_of_is_swap
{α : Type u}
[decidable_eq α]
[fintype α]
{f : equiv.perm α} :
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) :
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
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.eq_sign_of_surjective_hom
{α : Type u}
[decidable_eq α]
[fintype α]
{s : equiv.perm α →* units ℤ} :
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 ≠ 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 : α ≃ β) :
(∀ (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 → β) :
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_swap_mul_aux₁
{α : Type u}
[decidable_eq α]
[fintype α]
(n : ℕ)
{b x : α}
{f : equiv.perm α} :
theorem
equiv.perm.is_cycle_swap_mul_aux₂
{α : Type u}
[decidable_eq α]
[fintype α]
(n : ℤ)
{b x : α}
{f : equiv.perm α} :
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 : α} :
theorem
equiv.perm.is_cycle_swap_mul
{α : Type u}
[decidable_eq α]
[fintype α]
{f : equiv.perm α}
(hf : f.is_cycle)
{x : α} :
@[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 α} :