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

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

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

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

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

    Instances For
      def derangements.subtypeEquiv {α : Type u_1} (p : αProp) [DecidablePred p] :
      ↑(derangements (Subtype p)) { f // ∀ (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.

      Instances For

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

        • derangements on α
        • derangements on α minus a.
        Instances For

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

          Instances For

            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".

            Instances For
              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}ᶜ".

              Instances For