English
If you restrict a permutation to a predicate-defined subtype, the sign of the restricted permutation equals the sign of the original permutation, provided the predicate is preserved by the permutation and handles non-fixed points appropriately.
Русский
Если ограничить перестановку до подтипа, заданного предикатом p, то знак ограниченной перестановки равен знаку исходной перестановки, при условии сохранения предиката и контроля за точками, не зафиксированными.
LaTeX
$$$\\operatorname{sign}(\\operatorname{subtypePerm}(f,f_1)) = \\operatorname{sign}(f)$$$
Lean4
theorem sign_subtypePerm (f : Perm α) {p : α → Prop} [DecidablePred p] (h₁ : ∀ x, p (f x) ↔ p x)
(h₂ : ∀ x, f x ≠ x → p x) : sign (subtypePerm f h₁) = sign f :=
by
let l := (truncSwapFactors (subtypePerm f h₁)).out
have hl' : ∀ g' ∈ l.1.map ofSubtype, IsSwap g' := fun g' hg' =>
let ⟨g, hg⟩ := List.mem_map.1 hg'
hg.2 ▸ (l.2.2 _ hg.1).of_subtype_isSwap
have hl'₂ : (l.1.map ofSubtype).prod = f := by rw [l.1.prod_hom ofSubtype, l.2.1, ofSubtype_subtypePerm _ h₂]
conv =>
congr
rw [← l.2.1]
simp_rw [← hl'₂]
rw [sign_prod_list_swap l.2.2, sign_prod_list_swap hl', List.length_map]
