The index permutation between two orderings of the same list

Two duplicate-free lists with the same members are reorderings of one another, and the reordering is a permutation of positions: the index permutation. Its sign is what a summand pays for being written in one order rather than the other, so sorting signs along any injective relabelling differ by exactly it, and the sign is multiplicative along a chain of reorderings.

Length equality from Nodup + same membership

theorem RS.length_eq_of_nodup_mem {γ : Type u_1} (l₁ l₂ : List γ) (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (hmem : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂) : l₁.length = l₂.length

Duplicate-free lists with the same members have the same length.

The canonical index permutation

noncomputable def RS.listIndexPerm {γ : Type u_1} [DecidableEq γ] (l₁ l₂ : List γ) (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (hmem : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂) (hlen : l₁.length = l₂.length) : Equiv.Perm (Fin l₁.length)

The index permutation carrying one list to another with the same members: the position in the second list of the entry at each position of the first.

Equations

• RS.listIndexPerm l₁ l₂ h₁ h₂ hmem hlen = (List.Nodup.getEquiv l₁ h₁).trans ((Equiv.subtypeEquivRight ⋯).trans ((List.Nodup.getEquiv l₂ h₂).symm.trans (finCongr ⋯)))

Defining property

theorem RS.listIndexPerm_getElem {γ : Type u_1} [DecidableEq γ] (l₁ l₂ : List γ) (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (hmem : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂) (hlen : l₁.length = l₂.length) (i : Fin l₁.length) : l₂[↑((listIndexPerm l₁ l₂ h₁ h₂ hmem hlen) i)] = l₁[↑i]

Its defining property: it matches the two lists entrywise.

Helper: inverse index property

Main transport theorem

theorem RS.sortSign_map_listIndexPerm {γ : Type u_1} [DecidableEq γ] {β : Type} [LinearOrder β] (l₁ l₂ : List γ) (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (hmem : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂) (hlen : l₁.length = l₂.length) (g : γ → β) (hg : (List.map g l₁).Nodup) : sortSign (List.map g l₂) = ↑(Equiv.Perm.sign (listIndexPerm l₁ l₂ h₁ h₂ hmem hlen)) * sortSign (List.map g l₁)

Sorting signs differ by the index permutation's sign, along any injective relabelling of the entries.

Composition triangle (sign level)

theorem RS.sign_listIndexPerm_trans {γ : Type u_1} [DecidableEq γ] (l₁ l₂ l₃ : List γ) (h₁ : l₁.Nodup) (h₂ : l₂.Nodup) (h₃ : l₃.Nodup) (hmem₁₂ : ∀ (x : γ), x ∈ l₁ ↔ x ∈ l₂) (hmem₂₃ : ∀ (x : γ), x ∈ l₂ ↔ x ∈ l₃) (hlen₁₂ : l₁.length = l₂.length) (hlen₂₃ : l₂.length = l₃.length) : Equiv.Perm.sign (listIndexPerm l₁ l₃ h₁ h₃ ⋯ ⋯) = Equiv.Perm.sign (listIndexPerm l₁ l₂ h₁ h₂ hmem₁₂ hlen₁₂) * Equiv.Perm.sign (listIndexPerm l₂ l₃ h₂ h₃ hmem₂₃ hlen₂₃)

The index permutation composes across three lists, so its sign is multiplicative along a chain.