Documentation

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

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.

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

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

    Equations
    • e.derangementsCongr = e.permCongr.subtypeEquiv
    Instances For
      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.

      Equations
      • One or more equations did not get rendered due to their size.
      Instances For

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

        • derangements on α
        • derangements on α minus a.
        Equations
        • One or more equations did not get rendered due to their size.
        Instances For

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

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

            Equations
            • One or more equations did not get rendered due to their size.
            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}ᶜ".

              Equations
              • derangements.derangementsRecursionEquiv = derangements.derangementsOptionEquivSigmaAtMostOneFixedPoint.trans (Equiv.sigmaCongrRight derangements.atMostOneFixedPointEquivSum_derangements)
              Instances For