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
.
Equations
- f.support = finset.filter (λ (x : α), ⇑f x ≠ x) finset.univ
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.
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 α), _⟩
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)) _
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 _)
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
Equations
- f.sign_aux3 = quotient.hrec_on s (λ (l : list α) (h : ∀ (x : α), x ∈ ⟦l⟧), equiv.perm.sign_aux2 l f) _
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