# mathlibdocumentation

combinatorics.derangements.basic

# Derangements on types #

In this file we define derangements α, the set of derangements on a type α.

We also define some equivalences involving various subtypes of perm α and derangements α:

• derangements_option_equiv_sigma_at_most_one_fixed_point: An equivalence between derangements (option α) and the sigma-type Σ a : α, {f : perm α // fixed_points f ⊆ a}.
• derangements_recursion_equiv: An equivalence between derangements (option α) and the sigma-type Σ a : α, (derangements (({a}ᶜ : set α) : Type _) ⊕ derangements α) which is later used to inductively count the number of derangements.

In order to prove the above, we also prove some results about the effect of equiv.remove_none on derangements: remove_none.fiber_none and remove_none.fiber_some.

def derangements (α : Type u_1) :

A permutation is a derangement if it has no fixed points.

Equations
• = {f : | ∀ (x : α), f x x}
theorem mem_derangements_iff_fixed_points_eq_empty {α : Type u_1} {f : equiv.perm α} :
def equiv.derangements_congr {α : Type u_1} {β : Type u_2} (e : α β) :

If α is equivalent to β, then derangements α is equivalent to derangements β.

Equations
def derangements.subtype_equiv {α : Type u_1} (p : α → Prop)  :
(derangements (subtype p)) {f // ∀ (a : α), ¬p a

Derangements on a subtype are equivalent to permutations on the original type where points are fixed iff they are not in the subtype.

Equations

The set of permutations that fix either a or nothing is equivalent to the sum of:

• derangements on α
• derangements on α minus a.
Equations
def derangements.equiv.remove_none.fiber {α : Type u_1} [decidable_eq α] (a : option α) :

The set of permutations f such that the preimage of (a, f) under equiv.perm.decompose_option is a derangement.

Equations
• = {f : | (a, f)
theorem derangements.equiv.remove_none.mem_fiber {α : Type u_1} [decidable_eq α] (a : option α) (f : equiv.perm α) :
∃ (F : equiv.perm (option α)), F = a
theorem derangements.equiv.remove_none.fiber_some {α : Type u_1} [decidable_eq α] (a : α) :
= {f : | {a}}

For any a : α, the fiber over some a is the set of permutations where a is the only possible fixed point.

The set of derangements on option α is equivalent to the union over a : α of "permutations with a the only possible fixed point".

Equations

The set of derangements on option α is equivalent to the union over all a : α of "derangements on α ⊕ derangements on {a}ᶜ".

Equations