The sign pairing #
For two duplicate-free same-membership lists, the product of their mapped sorting signs is the reindexing permutation's sign: the transport plus a square.
theorem
RS.sortSign_key_pair
{γ : Type u_1}
[DecidableEq γ]
{β : Type}
[LinearOrder β]
(g : γ → β)
(hg : Function.Injective g)
(l₁ l₂ : List γ)
(h₁ : l₁.Nodup)
(h₂ : l₂.Nodup)
(hmem : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂)
(hlen : l₁.length = l₂.length)
:
↑(sortSign (List.map g l₁)) * ↑(sortSign (List.map g l₂)) = ↑↑(Equiv.Perm.sign (listIndexPerm l₁ l₂ h₁ h₂ hmem hlen))
The sign pairing: mapped sorting signs of two enumerations multiply to the reindexing sign.