Flag coordinates for a closed submanifold containing the centre

In the proof of [Kol07, Theorem 88], Kollár chooses coordinates x_1, …, x_n with S = (x_1 = 0) and the centre of the blow-up π equal to (x_1 = ⋯ = x_r = 0), without proof. On manifolds, and for a submanifold S of any codimension s: at a point a of a closed submanifold Y ⊆ S of codimension c there is a chart adapted to Y in which S is the zero set of s of the c centre coordinates (exists_adaptedChart_flag). The pair-chart lemma exists_adaptedChart_pair of Hironaka.Manifold.BlowUp.Transform.StrictCharts is the case s = 1; this file proves the general case by the same argument, generalized from one function to s:

• the adapted coordinates h_1, …, h_s of S at a vanish on Y, so their germs lie in the stalk ideal of Y, which is spanned by the centre coordinates z_1, …, z_c of an adapted chart of Y (stalkIdeal_idealSheaf_eq_span): h_j = ∑_k g_{jk} z_k near a with analytic g_{jk};
• the differentials satisfy dh_j(a) = ∑_k g_{jk}(a) dz_k(a) and are independent (S is a submanifold), so by the exchange lemma (exists_finset_linearIndependent_sum) there is a set K of c − s centre indices such that the dh_j(a) together with the dz_k(a), k ∈ K, are independent; the complementary s indices are enumerated by τ : Fin s ↪ Fin c;
• the family z' (the h_j in the slots τ j, the z_k in the slots k ∈ K) has independent differentials, so the chart completion exists_adaptedChart_zeroSet' makes it the coordinates of a chart at a; its common zero set is Y near a: the s × s matrix (g_{j (τ j')}(a)) is invertible (the independence of the exchanged family says exactly that), hence invertible near a, and on {z_K = 0} the system h = G_τ · z_τ gives h = 0 ⟺ z_τ = 0.

The argument is not in the sources. Flag coordinates are the setting of the codimension-s description of the strict transform in Hironaka.Manifold.BlowUp.Transform.Strict.

theorem Manifold.germ_coe_sum {α : Type u_1} {β : Type u_2} {ι : Type u_3} [AddCommMonoid β] {l : Filter α} (s : Finset ι) (f : ι → α → β) : ∑ i ∈ s, ↑(f i) = ↑(∑ i ∈ s, f i)

The coercion to germs commutes with finite sums.

Linear algebra: the exchange lemma

theorem Manifold.exists_finset_linearIndependent_sum {𝕜 : Type u_1} [Field 𝕜] {V : Type u_2} [AddCommGroup V] [Module 𝕜 V] {c s : ℕ} (e : Fin c → V) (he : LinearIndependent 𝕜 e) (d : Fin s → V) (hd : LinearIndependent 𝕜 d) (hsub : ∀ (j : Fin s), d j ∈ Submodule.span 𝕜 (Set.range e)) : ∃ (K : Finset (Fin c)), s + K.card = c ∧ LinearIndependent 𝕜 (Sum.elim d fun (k : ↥K) => e ↑k)

The exchange lemma: an independent family d of s vectors inside the span of an independent family e of c vectors can be completed to a basis of that span by c − s of the vectors e k, k ∈ K.

theorem Manifold.exists_embedding_range_eq_compl {c s : ℕ} (K : Finset (Fin c)) (h : s + K.card = c) : ∃ (τ : Fin s ↪ Fin c), ∀ (k : Fin c), k ∈ Set.range ⇑τ ↔ k ∉ K

An enumeration of the complement of a finset of c − s indices by Fin s.

Flag coordinates

theorem Manifold.exists_adaptedChart_flag {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M] {Y S : Set M} {c s : ℕ} (hY : IsClosedSubmanifold ψ Y c) (hS : IsClosedSubmanifold ψ S s) (hYS : Y ⊆ S) {a : M} (ha : a ∈ Y) : ∃ (φ : OpenPartialHomeomorph M E) (σ : Fin c ↪ Fin n) (τ : Fin s ↪ Fin c), a ∈ φ.source ∧ IsAdaptedChart ψ Y φ σ ∧ ∀ x ∈ φ.source, x ∈ S ↔ ∀ (j : Fin s), ψ (↑φ x) (σ (τ j)) = 0

At a point of a closed submanifold Y of codimension c contained in a closed submanifold S of codimension s, there is a chart adapted to Y in which S is the zero set of s of the c centre coordinates.