Ordered pairs of distinct elements of Fin n, by their difference

An ordered pair (a, b) of distinct elements of Fin n is determined by its source a and its nonzero cyclic difference b - a. Shifting the difference down by one gives an equivalence {p : Fin n × Fin n // p.1 ≠ p.2} ≃ Fin (n - 1) × Fin n. Composed with finProdFinEquiv, it lists the pairs of difference 1 first, then those of difference 2, and so on, each group by its source. The root systems of types Aₙ and Dₙ enumerate their roots this way, so that the pairs (a, a + 1) behind the simple roots come first.

Main definitions

• TauCeti.finDistinctPairsEquiv: the equivalence, with the evaluation lemmas TauCeti.finDistinctPairsEquiv_apply_fst_val, TauCeti.finDistinctPairsEquiv_apply_snd and TauCeti.finDistinctPairsEquiv_symm_apply_coe.

def TauCeti.finDistinctPairsEquiv (n : ℕ) : { p : Fin n × Fin n // p.fst ≠ p.snd } ≃ Fin (n - 1) × Fin n

The ordered pairs of distinct elements of Fin n, by their nonzero cyclic difference b - a shifted down to Fin (n - 1), and their source a.

Equations

• One or more equations did not get rendered due to their size.

@[simp]

theorem TauCeti.finDistinctPairsEquiv_apply_fst_val {n : ℕ} (p : { p : Fin n × Fin n // p.fst ≠ p.snd }) : ↑((finDistinctPairsEquiv n) p).fst = ↑((↑p).snd - (↑p).fst) - 1

The first coordinate of finDistinctPairsEquiv is the cyclic difference minus one.

@[simp]

theorem TauCeti.finDistinctPairsEquiv_apply_snd {n : ℕ} (p : { p : Fin n × Fin n // p.fst ≠ p.snd }) : ((finDistinctPairsEquiv n) p).snd = (↑p).fst

The second coordinate of finDistinctPairsEquiv is the source.

@[simp]

theorem TauCeti.finDistinctPairsEquiv_symm_apply_coe {n : ℕ} (q : Fin (n - 1) × Fin n) : ↑((finDistinctPairsEquiv n).symm q) = (q.snd, q.snd + ⟨↑q.fst + 1, ⋯⟩)

The inverse of finDistinctPairsEquiv sends a difference index i and a source a to the pair (a, a + (i + 1)).