English
For a fixed a in α, the set of permutations with fixedPoints ⊆ {a} is equivalent to the disjoint sum of derangements on {a}^c and derangements on α.
Русский
Для фиксированного a∈α множество перестановок с fixedPoints ⊆ {a} эквивалентно вкладыванию дерangements на комплемент {a} и дерangements на α.
LaTeX
$$$\{ f: \mathrm{Perm}\, \alpha \mid \operatorname{fixedPoints}(f) \subseteq \{a\} \} \simeq \mathrm{derangements}({a}^c) \oplus \mathrm{derangements}(\alpha)$$$
Lean4
/-- The set of permutations that fix either `a` or nothing is equivalent to the sum of:
- derangements on `α`
- derangements on `α` minus `a`. -/
def atMostOneFixedPointEquivSum_derangements [DecidableEq α] (a : α) :
{ f : Perm α // fixedPoints f ⊆ { a } } ≃ (derangements ({ a }ᶜ : Set α)) ⊕ (derangements α) :=
calc
{ f : Perm α // fixedPoints f ⊆ { a } } ≃
{ f : { f : Perm α // fixedPoints f ⊆ { a } } // a ∈ fixedPoints f } ⊕
{ f : { f : Perm α // fixedPoints f ⊆ { a } } // a ∉ fixedPoints f } :=
(Equiv.sumCompl _).symm
_ ≃
{ f : Perm α // fixedPoints f ⊆ { a } ∧ a ∈ fixedPoints f } ⊕
{ f : Perm α // fixedPoints f ⊆ { a } ∧ a ∉ fixedPoints f } :=
by
refine Equiv.sumCongr ?_ ?_
· exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (a ∈ fixedPoints ·)
· exact subtypeSubtypeEquivSubtypeInter (fun x : Perm α => fixedPoints x ⊆ { a }) (a ∉ fixedPoints ·)
_ ≃ { f : Perm α // fixedPoints f = { a } } ⊕ { f : Perm α // fixedPoints f = ∅ } :=
by
refine Equiv.sumCongr (subtypeEquivRight fun f => ?_) (subtypeEquivRight fun f => ?_)
· rw [Set.eq_singleton_iff_unique_mem, and_comm]
rfl
· rw [Set.eq_empty_iff_forall_notMem]
exact ⟨fun h x hx => h.2 (h.1 hx ▸ hx), fun h => ⟨fun x hx => (h _ hx).elim, h _⟩⟩
_ ≃ derangements ({ a }ᶜ : Set α) ⊕ derangements α :=
by
refine
Equiv.sumCongr ((derangements.subtypeEquiv _).trans <| subtypeEquivRight fun x => ?_).symm
(subtypeEquivRight fun f => mem_derangements_iff_fixedPoints_eq_empty.symm)
rw [eq_comm, Set.ext_iff]
simp_rw [Set.mem_compl_iff, Classical.not_not]
