Derangements on types #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

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.

source

def derangements (α : Type u_1) :

set (equiv.perm α)

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

Equations

derangements α = {f : equiv.perm α | ∀ (x : α), ⇑f x ≠ x}

Instances for derangements

derangements.decidable_pred

Instances for ↥derangements

derangements.fintype

source

theorem mem_derangements_iff_fixed_points_eq_empty {α : Type u_1} {f : equiv.perm α} :

f ∈ derangements α ↔ function.fixed_points ⇑f = ∅

source

def equiv.derangements_congr {α : Type u_1} {β : Type u_2} (e : α ≃ β) :

↥(derangements α) ≃ ↥(derangements β)

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

Equations

e.derangements_congr = e.perm_congr.subtype_equiv _

source

@[protected]

def derangements.subtype_equiv {α : Type u_1} (p : α → Prop) [decidable_pred p] :

↥(derangements (subtype p)) ≃ {f // ∀ (a : α), ¬p a ↔ a ∈ function.fixed_points ⇑f}

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

Equations

derangements.subtype_equiv p = (((equiv.perm.subtype_equiv_subtype_perm p).subtype_equiv _).trans (equiv.subtype_subtype_equiv_subtype_exists (λ (f : equiv.perm α), ∀ (a : α), ¬p a → a ∈ function.fixed_points ⇑f) (λ (f : {f // ∀ (a : α), ¬p a → a ∈ function.fixed_points ⇑f}), ∀ (a : α), a ∈ function.fixed_points ⇑f → ¬p a))).trans (equiv.subtype_equiv_right _)

source

def derangements.at_most_one_fixed_point_equiv_sum_derangements {α : Type u_1} [decidable_eq α] (a : α) :

{f // function.fixed_points ⇑f ⊆ {a}} ≃ ↥(derangements ↥{a}ᶜ) ⊕ ↥(derangements α)

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

derangements on α
derangements on α minus a.

Equations

derangements.at_most_one_fixed_point_equiv_sum_derangements a = (((equiv.sum_compl (λ (f : {f // function.fixed_points ⇑f ⊆ {a}}), a ∈ function.fixed_points ⇑f)).symm.trans ((_.mpr (equiv.subtype_subtype_equiv_subtype_inter (λ (f : equiv.perm α), function.fixed_points ⇑f ⊆ {a}) (λ (f : equiv.perm α), a ∈ function.fixed_points ⇑f))).sum_congr (_.mpr (equiv.subtype_subtype_equiv_subtype_inter (λ (f : equiv.perm α), function.fixed_points ⇑f ⊆ {a}) (λ (f : equiv.perm α), a ∉ function.fixed_points ⇑f))))).trans ((equiv.subtype_equiv_right _).sum_congr (equiv.subtype_equiv_right _))).trans (((derangements.subtype_equiv (λ (x : α), x ∈ {a}ᶜ)).trans (equiv.subtype_equiv_right _)).symm.sum_congr (equiv.subtype_equiv_right derangements.at_most_one_fixed_point_equiv_sum_derangements._proof_6))

source

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

set (equiv.perm α)

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

Equations

derangements.equiv.remove_none.fiber a = {f : equiv.perm α | (a, f) ∈ ⇑equiv.perm.decompose_option '' derangements (option α)}

source

theorem derangements.equiv.remove_none.mem_fiber {α : Type u_1} [decidable_eq α] (a : option α) (f : equiv.perm α) :

f ∈ derangements.equiv.remove_none.fiber a ↔ ∃ (F : equiv.perm (option α)), F ∈ derangements (option α) ∧ ⇑F option.none = a ∧ equiv.remove_none F = f

source

theorem derangements.equiv.remove_none.fiber_none {α : Type u_1} [decidable_eq α] :

derangements.equiv.remove_none.fiber option.none = ∅

source

theorem derangements.equiv.remove_none.fiber_some {α : Type u_1} [decidable_eq α] (a : α) :

derangements.equiv.remove_none.fiber (option.some a) = {f : equiv.perm α | function.fixed_points ⇑f ⊆ {a}}

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

source

def derangements.derangements_option_equiv_sigma_at_most_one_fixed_point {α : Type u_1} [decidable_eq α] :

↥(derangements (option α)) ≃ Σ (a : α), ↥{f : equiv.perm α | function.fixed_points ⇑f ⊆ {a}}

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

Equations

derangements.derangements_option_equiv_sigma_at_most_one_fixed_point = (((equiv.perm.decompose_option.image (derangements (option α))).trans (equiv.set_prod_equiv_sigma (⇑equiv.perm.decompose_option '' derangements (option α)))).trans (equiv.sigma_option_equiv_of_some (λ (a : option α), ↥(derangements.equiv.remove_none.fiber a)) derangements.derangements_option_equiv_sigma_at_most_one_fixed_point._proof_1)).trans (derangements.derangements_option_equiv_sigma_at_most_one_fixed_point._proof_2.mpr (equiv.refl (Σ (a : α), ↥{f : equiv.perm α | function.fixed_points ⇑f ⊆ {a}})))

source

def derangements.derangements_recursion_equiv {α : Type u_1} [decidable_eq α] :

↥(derangements (option α)) ≃ Σ (a : α), ↥(derangements ↥{a}ᶜ) ⊕ ↥(derangements α)

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

Equations

derangements.derangements_recursion_equiv = derangements.derangements_option_equiv_sigma_at_most_one_fixed_point.trans (equiv.sigma_congr_right derangements.at_most_one_fixed_point_equiv_sum_derangements)