Kollár's coordinate order for a blow-up chart

Kollár's chart of the blowing-up [Kol07, Definition 60, (60.2)] lists the coordinates so that the centre's coordinates other than the divisor coordinate come first (positions < r), the divisor coordinate x_r is at position r, and the coordinates transversal to the centre come after. Given the block indices σ : Fin c ↪ Fin n of an adapted chart and the index i of the blow-up chart, exists_kollarPerm produces r = c - 1 and a permutation τ of Fin n with τ r = σ i and {j | j < r} = τ⁻¹(σ '' {k | k ≠ i}). These are the hypotheses under which a blow-up chart is read in Kollár's coordinates (blowUpChartMap_eq_kollarChart of Hironaka.Manifold.BlowUp.Quadratic) and the chart-ring homomorphism exists_chartRing_hom of Hironaka.Manifold.BlowUp.Transform.KollarChart is built. Pure combinatorics; not in the sources.

def Manifold.kollarFirst {c n : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : Finset (Fin n)

The centre indices other than σ i.

Equations

• Manifold.kollarFirst σ i = (Finset.map σ Finset.univ).erase (σ i)

def Manifold.kollarLast {c n : ℕ} (σ : Fin c ↪ Fin n) : Finset (Fin n)

The indices outside the centre.

Equations

• Manifold.kollarLast σ = (Finset.map σ Finset.univ)ᶜ

theorem Manifold.card_kollarFirst {c n : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : (kollarFirst σ i).card = c - 1

theorem Manifold.card_kollarLast {c n : ℕ} (σ : Fin c ↪ Fin n) : (kollarLast σ).card = n - c

theorem Manifold.c_le_n {c n : ℕ} (σ : Fin c ↪ Fin n) : c ≤ n

theorem Manifold.c_pos {c : ℕ} (i : Fin c) : 0 < c

theorem Manifold.exists_kollarPerm {c n : ℕ} (σ : Fin c ↪ Fin n) (i : Fin c) : ∃ (r : Fin n) (τ : Fin n ≃ Fin n), τ r = σ i ∧ ∀ (j : Fin n), j < r ↔ ∃ (k : Fin c), k ≠ i ∧ τ j = σ k

A permutation τ of the coordinate indices with the centre's other coordinates at the positions < r = c - 1, the divisor coordinate σ i at r, and the transversal coordinates after, as in Kollár's chart [Kol07, Definition 60, (60.2)].