English
For any a, the fiber over some a corresponds to fixed-point constrained derangements.
Русский
Для любого a,fiber над some a соответствует дерangements с ограничением по фиксации.
LaTeX
$$$\operatorname{RemoveNone}.\operatorname{fiber}(\text{some } a) \simeq \{ f: \mathrm{Perm}\, \alpha \mid \operatorname{fixedPoints}(f) \subseteq \{a\} \}$$$
Lean4
/-- For any `a : α`, the fiber over `some a` is the set of permutations
where `a` is the only possible fixed point. -/
theorem fiber_some (a : α) : RemoveNone.fiber (some a) = {f : Perm α | fixedPoints f ⊆ { a }} :=
by
ext f
constructor
· rw [RemoveNone.mem_fiber]
rintro ⟨F, F_derangement, F_none, rfl⟩ x x_fixed
rw [mem_fixedPoints_iff] at x_fixed
apply_fun some at x_fixed
rcases Fx : F (some x) with - | y
· rwa [removeNone_none F Fx, F_none, Option.some_inj, eq_comm] at x_fixed
· exfalso
rw [removeNone_some F ⟨y, Fx⟩] at x_fixed
exact F_derangement _ x_fixed
· intro h_opfp
use Equiv.Perm.decomposeOption.symm (some a, f)
constructor
· intro x
apply_fun fun x => Equiv.swap none (some a) x
simp only [Perm.decomposeOption_symm_apply, Perm.coe_mul]
rcases x with - | x
· simp
simp only [comp, optionCongr_apply, Option.map_some, swap_apply_self]
by_cases x_vs_a : x = a
· rw [x_vs_a, swap_apply_right]
apply Option.some_ne_none
have ne_1 : some x ≠ none := Option.some_ne_none _
have ne_2 : some x ≠ some a := (Option.some_injective α).ne_iff.mpr x_vs_a
rw [swap_apply_of_ne_of_ne ne_1 ne_2, (Option.some_injective α).ne_iff]
intro contra
exact x_vs_a (h_opfp contra)
· rw [apply_symm_apply]
