The blow-up chart map in the coordinates of a flag

The identification S_{i+1} ≅ Bl_{Z_i ∩ S_i} S_i of the stages of a restricted blow-up sequence [Kol07, Definition 30.2] is checked in charts. Kollár's computation for a hypersurface S = (x_1 = 0) containing the centre [Kol07, Theorem 88, proof] observes that the blow-up charts whose distinguished coordinate is not x_1 cover the strict transform S_1; this module carries out the corresponding computation in a flag chart, for arbitrary codimensions. In a flag chart Y = {z_σ = 0} ⊆ S = {z_{σ (τ j)} = 0} (τ : Fin s ↪ Fin c) the blow-up chart map blowUpChartMap σ i of [BM88, Definition 4.1] for an index i ∉ range τ preserves the coordinate subspace {z_{σ (τ j)} = 0} and acts on the complementary coordinates 𝕜^{n-s} (projCompl, embedCompl along τ.trans σ) as the blow-up chart map of the induced data: the embedding restrictEmb σ τ : Fin (c - s) ↪ Fin (n - s) of the remaining centre indices σ k, k ∉ range τ, among the complementary coordinates, and the index restrictIdx τ hi of i among them. This is the computation behind the description of the blow-up charts of S' as the ambient charts of index ∉ range τ read in the complementary coordinates. Not in the sources beyond Kollár's remark; the proofs are coordinate computations.

theorem Manifold.apply_notMem_range_trans {n c s : ℕ} {σ : Fin c ↪ Fin n} {τ : Fin s ↪ Fin c} {k : Fin c} (hk : k ∉ Set.range ⇑τ) : σ k ∉ Set.range ⇑(τ.trans σ)

The index of σ k, k ∉ range τ, among the complementary coordinates of τ.trans σ.

noncomputable def Manifold.restrictEmb {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) : Fin (c - s) ↪ Fin (n - s)

The remaining centre indices σ k, k ∉ range τ, read among the coordinates of 𝕜^{n-s} complementary to range (τ.trans σ): the block embedding of the centre Y ⊆ S inside the bundled S.

Equations

• Manifold.restrictEmb σ τ = { toFun := fun (m : Fin (c - s)) => (Manifold.complEquiv (τ.trans σ)) ⟨σ ↑((Manifold.complEquiv τ).symm m), ⋯⟩, inj' := ⋯ }

theorem Manifold.restrictEmb_apply {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) (m : Fin (c - s)) : (restrictEmb σ τ) m = (complEquiv (τ.trans σ)) ⟨σ ↑((complEquiv τ).symm m), ⋯⟩

theorem Manifold.symm_restrictEmb {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) (m : Fin (c - s)) : ↑((complEquiv (τ.trans σ)).symm ((restrictEmb σ τ) m)) = σ ↑((complEquiv τ).symm m)

The coordinate of 𝕜^n read by the m-th coordinate of restrictEmb σ τ.

noncomputable def Manifold.restrictIdx {c s : ℕ} (τ : Fin s ↪ Fin c) {i : Fin c} (hi : i ∉ Set.range ⇑τ) : Fin (c - s)

The index of a centre index i ∉ range τ among the remaining ones.

Equations

• Manifold.restrictIdx τ hi = (Manifold.complEquiv τ) ⟨i, hi⟩

theorem Manifold.symm_restrictIdx {c s : ℕ} (τ : Fin s ↪ Fin c) {i : Fin c} (hi : i ∉ Set.range ⇑τ) : ↑((complEquiv τ).symm (restrictIdx τ hi)) = i

theorem Manifold.symm_restrictEmb_restrictIdx {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) {i : Fin c} (hi : i ∉ Set.range ⇑τ) : ↑((complEquiv (τ.trans σ)).symm ((restrictEmb σ τ) (restrictIdx τ hi))) = σ i

theorem Manifold.restrictIdx_ne {c s : ℕ} (τ : Fin s ↪ Fin c) {i k : Fin c} (hi : i ∉ Set.range ⇑τ) (hk : k ∉ Set.range ⇑τ) (hki : k ≠ i) : restrictIdx τ hk ≠ restrictIdx τ hi

theorem Manifold.eq_restrictEmb_restrictIdx {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) {m : Fin (n - s)} {k : Fin c} (hk : k ∉ Set.range ⇑τ) (h : ↑((complEquiv (τ.trans σ)).symm m) = σ k) : m = (restrictEmb σ τ) (restrictIdx τ hk)

A complementary coordinate reading σ k, k ∉ range τ, is the restrictIdx-th coordinate of restrictEmb.

theorem Manifold.restrictEmb_ne_of_forall_ne {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) {m : Fin (n - s)} (hm : ∀ (k : Fin c), σ k ≠ ↑((complEquiv (τ.trans σ)).symm m)) (k' : Fin (c - s)) : (restrictEmb σ τ) k' ≠ m

A complementary coordinate off the block of σ is off the block of restrictEmb σ τ.

theorem Manifold.projCompl_blowUpChartMap {𝕜 : Type} [RCLike 𝕜] {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) {i : Fin c} (hi : i ∉ Set.range ⇑τ) (x : Fin n → 𝕜) : projCompl (τ.trans σ) (blowUpChartMap σ i x) = blowUpChartMap (restrictEmb σ τ) (restrictIdx τ hi) (projCompl (τ.trans σ) x)

In the complementary coordinates of τ.trans σ, the blow-up chart map of an index i ∉ range τ is the blow-up chart map of the induced data (restrictEmb σ τ, restrictIdx τ hi); compare the charts covering the strict transform S_1 in [Kol07, Theorem 88, proof].

theorem Manifold.blowUpChartMap_embedCompl {𝕜 : Type} [RCLike 𝕜] {n c s : ℕ} (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c) {i : Fin c} (hi : i ∉ Set.range ⇑τ) (v : Fin (n - s) → 𝕜) : blowUpChartMap σ i (embedCompl (τ.trans σ) v) = embedCompl (τ.trans σ) (blowUpChartMap (restrictEmb σ τ) (restrictIdx τ hi) v)

The blow-up chart map of an index i ∉ range τ preserves the coordinate subspace {z_{σ (τ j)} = 0}, on which it is the blow-up chart map of the induced data read through embedCompl.