Inversions of a map on a finite set

For a map f : α → β between linear orders and a finite set s ⊆ α, the inversions of f on s are the pairs a < b of elements of s whose order f reverses, f b < f a. When f is injective, the parity of their number is the sign of the permutation of s obtained by comparing the order of s with the order of its image f(s). For a permutation σ of Fin n, TauCeti.sign_eq_neg_one_pow_card_inversion identifies (-1) ^ #(Finset.univ.inversions σ) with Equiv.Perm.sign σ.

These signs compare two orderings of the same finite set. In a signed cube totalization the edge S ⟶ S ∪ {a} carries the sign (-1) ^ #{b ∈ S | b < a}, and reordering the indices of the cube by f changes these signs by the inversion signs of f on the two vertices of the edge (Finset.neg_one_pow_card_inversions_insert). Inversion signs are multiplicative under composition (Finset.neg_one_pow_card_inversions_comp).

Main definitions

• Finset.inversions f s: the pairs (a, b) of elements of s with a < b and f b < f a.

Main results

• Finset.inversions_univ: on a whole finite type, the inversions are all pairs a < b with f b < f a.
• Finset.card_inversions_insert: adjoining a new element a to s adds the inversions involving a.
• Finset.card_inversions_insert_add_card_filter_lt: for an injective map, the same comparison of insert a s with s as a count of elements, up to an even number.
• Finset.neg_one_pow_card_inversions_insert: the inversion sign of an injective map on insert a s, compared with that on s, is the sign relating the position of a in s to the position of f a in f(s).
• Finset.even_card_inversions_comp: the inversion counts of f on s, of g on f(s) and of g ∘ f on s add up to an even number.
• Finset.neg_one_pow_card_inversions_comp: the inversion sign of g ∘ f on s is the product of the inversion signs of f on s and of g on f(s).
• Finset.card_univ_inversions_eq_comp_succAbove: deleting the entry at k of a tuple removes the inversions involving k.
• Finset.neg_one_pow_card_univ_inversions_comp_succAbove: the inversion sign of a tuple compared with the inversion sign of the tuple with its entry at k deleted.

def Finset.inversions {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) (s : Finset α) : Finset (α × α)

The inversions of f on s: the pairs (a, b) of elements of s with a < b whose order f reverses, f b < f a.

@[simp]

theorem Finset.mem_inversions {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Finset α} {p : α × α} : p ∈ inversions f s ↔ p.1 ∈ s ∧ p.2 ∈ s ∧ p.1 < p.2 ∧ f p.2 < f p.1

@[simp]

theorem Finset.inversions_empty {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) : inversions f ∅ = ∅

theorem Finset.inversions_eq_empty_of_monotone {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Monotone f) (s : Finset α) : inversions f s = ∅

A monotone map has no inversions.

theorem Finset.inversions_univ {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] [Fintype α] (f : α → β) : inversions f univ = {p : α × α | p.1 < p.2 ∧ f p.2 < f p.1}

On the whole of a finite type, the inversions of f are all the pairs a < b with f b < f a.

@[simp]

theorem Finset.inversions_id {α : Type u_1} [LinearOrder α] (s : Finset α) : inversions id s = ∅

theorem Finset.inversions_congr {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f g : α → β} {s : Finset α} (h : ∀ a ∈ s, f a = g a) : inversions f s = inversions g s

The inversions of f on s only depend on the values of f on s.

theorem Finset.card_inversions_comp_swap_lt {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} {s : Finset α} {i j : α} (h : (i, j) ∈ inversions f s) : (inversions (f ∘ ⇑(Equiv.swap i j)) s).card < (inversions f s).card

Exchanging the values at an inversion lowers the inversion count. If (i, j) is an inversion of f on s, then f ∘ swap i j, which takes the value f j at i and f i at j, has strictly fewer inversions on s than f.

theorem Finset.card_inversions_insert {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] (f : α → β) {s : Finset α} {a : α} (ha : a ∉ s) : (inversions f (insert a s)).card = (inversions f s).card + {b ∈ s | b < a ∧ f a < f b}.card + {b ∈ s | a < b ∧ f b < f a}.card

Adjoining a new element a to s adds the inversions (b, a) with b < a and the inversions (a, b) with a < b.

theorem Finset.card_inversions_insert_add_card_filter_lt {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {f : α → β} (hf : Function.Injective f) {s : Finset α} {a : α} (ha : a ∉ s) : (inversions f (insert a s)).card + {b ∈ s | b < a}.card = (inversions f s).card + {b ∈ s | f b < f a}.card + 2 * {b ∈ s | b < a ∧ f a < f b}.card

For an injective map and a ∉ s, the inversions on insert a s and the elements of s below a together count the inversions on s and the elements of s whose image lies below f a, up to an even number.

theorem Finset.neg_one_pow_card_inversions_insert {α : Type u_1} {β : Type u_2} [LinearOrder α] [LinearOrder β] {R : Type u_4} [Monoid R] [HasDistribNeg R] {f : α → β} (hf : Function.Injective f) {s : Finset α} {a : α} (ha : a ∉ s) : (-1) ^ (inversions f (insert a s)).card * (-1) ^ {b ∈ s | b < a}.card = (-1) ^ (inversions f s).card * (-1) ^ {b ∈ s | f b < f a}.card

Reordering signs along an edge. For an injective map f and a ∉ s, the inversion sign of f on insert a s, times the sign recording the position of a in s, is the inversion sign of f on s times the sign recording the position of f a in f(s).

theorem Finset.even_card_inversions_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [LinearOrder β] [LinearOrder γ] {f : α ↪ β} {g : β → γ} (hg : Function.Injective g) (s : Finset α) : Even ((inversions (g ∘ ⇑f) s).card + (inversions (⇑f) s).card + (inversions g (map f s)).card)

The parities of the inversion counts of f on s, of g on f(s) and of g ∘ f on s add up to zero.

theorem Finset.neg_one_pow_card_inversions_comp {α : Type u_1} {β : Type u_2} {γ : Type u_3} [LinearOrder α] [LinearOrder β] [LinearOrder γ] {R : Type u_4} [Monoid R] [HasDistribNeg R] (f : α ↪ β) {g : β → γ} (hg : Function.Injective g) (s : Finset α) : (-1) ^ (inversions (g ∘ ⇑f) s).card = (-1) ^ (inversions (⇑f) s).card * (-1) ^ (inversions g (map f s)).card

Inversion signs are multiplicative. For an embedding f and an injective map g, the inversion sign of g ∘ f on s is the product of the inversion signs of f on s and of g on f(s).

theorem Finset.card_univ_inversions_eq_comp_succAbove {β : Type u_2} [LinearOrder β] {n : ℕ} (b : Fin (n + 1) → β) (k : Fin (n + 1)) : (inversions b univ).card = (inversions (b ∘ k.succAbove) univ).card + {j : Fin (n + 1) | k < j ∧ b j < b k}.card + {i : Fin (n + 1) | i < k ∧ b k < b i}.card

Deleting the entry at k of a tuple b removes the inversions (k, j) and (i, k).

theorem Finset.neg_one_pow_card_univ_inversions_comp_succAbove {β : Type u_2} [LinearOrder β] {n : ℕ} {R : Type u_4} [Monoid R] [HasDistribNeg R] (b : Fin (n + 1) → β) (k : Fin (n + 1)) : (-1) ^ (inversions b univ).card * (-1) ^ {i : Fin (n + 1) | i < k ∧ b i = b k}.card = (-1) ^ ({i : Fin (n + 1) | b i < b k}.card + ↑k) * (-1) ^ (inversions (b ∘ k.succAbove) univ).card

Deleting an entry changes the inversion sign by a position count. The inversion sign of a tuple b, times the sign recording the earlier entries equal to b k, is the sign recording the position k and the number of entries smaller than b k, times the inversion sign of the tuple with its entry at k deleted.