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 α:

• derangementsOptionEquivSigmaAtMostOneFixedPoint: An equivalence between derangements (Option α) and the sigma-type Σ a : α, {f : Perm α // fixedPoints f ⊆ a}.
• derangementsRecursionEquiv: 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.removeNone on derangements: RemoveNone.fiber_none and RemoveNone.fiber_some.

def derangements (α : Type u_1) : Set (Equiv.Perm α)

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

theorem mem_derangements_iff_fixedPoints_eq_empty {α : Type u_1} {f : Equiv.Perm α} : f ∈ derangements α ↔ Function.fixedPoints ⇑f = ∅

def Equiv.derangementsCongr {α : Type u_1} {β : Type u_2} (e : α ≃ β) : ↑(derangements α) ≃ ↑(derangements β)

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

def derangements.subtypeEquiv {α : Type u_1} (p : α → Prop) [DecidablePred p] : ↑(derangements (Subtype p)) ≃ { f : Equiv.Perm α // ∀ (a : α), ¬p a ↔ a ∈ Function.fixedPoints ⇑f }

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

def derangements.atMostOneFixedPointEquivSum_derangements {α : Type u_1} [DecidableEq α] (a : α) : { f : Equiv.Perm α // Function.fixedPoints ⇑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.

def derangements.Equiv.RemoveNone.fiber {α : Type u_1} [DecidableEq α] (a : Option α) : Set (Equiv.Perm α)

The set of permutations f such that the preimage of (a, f) under Equiv.Perm.decomposeOption is a derangement.

theorem derangements.Equiv.RemoveNone.mem_fiber {α : Type u_1} [DecidableEq α] (a : Option α) (f : Equiv.Perm α) : f ∈ fiber a ↔ ∃ F ∈ derangements (Option α), F none = a ∧ Equiv.removeNone F = f

theorem derangements.Equiv.RemoveNone.fiber_none {α : Type u_1} [DecidableEq α] : fiber none = ∅

theorem derangements.Equiv.RemoveNone.fiber_some {α : Type u_1} [DecidableEq α] (a : α) : fiber (some a) = {f : Equiv.Perm α | Function.fixedPoints ⇑f ⊆ {a}}

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

def derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint {α : Type u_1} [DecidableEq α] : ↑(derangements (Option α)) ≃ (a : α) × ↑{f : Equiv.Perm α | Function.fixedPoints ⇑f ⊆ {a}}

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

def derangements.derangementsRecursionEquiv {α : Type u_1} [DecidableEq α] : ↑(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}ᶜ".