English
Equivalence between various representations of derangements on a subtype and ambient permutations; structural equivalences preserve derangements.
Русский
Эквивалентности различных представлений дерangements на подмножестве и на всей области сохраняют структуру дерangements.
LaTeX
$$see above$$
Lean4
/-- Derangements on a subtype are equivalent to permutations on the original type where points are
fixed iff they are not in the subtype. -/
protected def subtypeEquiv (p : α → Prop) [DecidablePred p] :
derangements (Subtype p) ≃ { f : Perm α // ∀ a, ¬p a ↔ a ∈ fixedPoints f } :=
calc
derangements (Subtype p) ≃
{ f : { f : Perm α // ∀ a, ¬p a → a ∈ fixedPoints f } // ∀ a, a ∈ fixedPoints f → ¬p a } :=
by
refine (Perm.subtypeEquivSubtypePerm p).subtypeEquiv fun f => ⟨fun hf a hfa ha => ?_, ?_⟩
· refine hf ⟨a, ha⟩ (Subtype.ext ?_)
simp_rw [mem_fixedPoints, IsFixedPt, Perm.subtypeEquivSubtypePerm, Equiv.coe_fn_mk,
Perm.ofSubtype_apply_of_mem _ ha] at hfa
assumption
rintro hf ⟨a, ha⟩ hfa
refine hf _ ?_ ha
simp only [Perm.subtypeEquivSubtypePerm_apply_coe, mem_fixedPoints]
dsimp [IsFixedPt]
simp_rw [Perm.ofSubtype_apply_of_mem _ ha, hfa]
_ ≃ { f : Perm α // ∃ _h : ∀ a, ¬p a → a ∈ fixedPoints f, ∀ a, a ∈ fixedPoints f → ¬p a } :=
(subtypeSubtypeEquivSubtypeExists _ _)
_ ≃ { f : Perm α // ∀ a, ¬p a ↔ a ∈ fixedPoints f } :=
subtypeEquivRight fun f => by simp_rw [exists_prop, ← forall_and, ← iff_iff_implies_and_implies]
