English
If there exists a constructive bijection i between the non-fixed points that intertwines f and g, then the signs of f and g coincide.
Русский
Если между неприкосновенными точками существует биекции, связывающая f и g, то знаки f и g совпадают.
LaTeX
$$$\\forall i,\\; (\\forall x_1,x_2,\\dots) \\; \\operatorname{sign}(f)=\\operatorname{sign}(g)$$$
Lean4
theorem sign_bij [DecidableEq β] [Fintype β] {f : Perm α} {g : Perm β} (i : ∀ x : α, f x ≠ x → β)
(h : ∀ x hx hx', i (f x) hx' = g (i x hx)) (hi : ∀ x₁ x₂ hx₁ hx₂, i x₁ hx₁ = i x₂ hx₂ → x₁ = x₂)
(hg : ∀ y, g y ≠ y → ∃ x hx, i x hx = y) : sign f = sign g :=
calc
sign f = sign (subtypePerm f <| by simp : Perm { x // f x ≠ x }) := (sign_subtypePerm _ _ fun _ => id).symm
_ = sign (subtypePerm g <| by simp : Perm { x // g x ≠ x }) :=
(sign_eq_sign_of_equiv _ _
(Equiv.ofBijective
(fun x : { x // f x ≠ x } =>
(⟨i x.1 x.2, by
have : f (f x) ≠ f x := mt (fun h => f.injective h) x.2
rw [← h _ x.2 this]
exact mt (hi _ _ this x.2) x.2⟩ :
{ y // g y ≠ y }))
⟨fun ⟨_, _⟩ ⟨_, _⟩ h => Subtype.eq (hi _ _ _ _ (Subtype.mk.inj h)), fun ⟨y, hy⟩ =>
let ⟨x, hfx, hx⟩ := hg y hy
⟨⟨x, hfx⟩, Subtype.eq hx⟩⟩)
fun ⟨x, _⟩ => Subtype.eq (h x _ _))
_ = sign g := sign_subtypePerm _ _ fun _ => id
