Kollár's disjoining blow-ups

The preliminary blow-ups of [Kol07, 72]: blow up the locus Z_0 where all k members of the boundary meet; the strict transforms have no k-fold intersection, so the next centre Z_1 is smooth, and "after (k − 1) steps we get rid of all pairwise intersections as well". This module proves the step — after blowing up the m-fold meet locus of an snc family with no (m + 1)-fold points, the strict transforms have no m-fold point (meetLocus_strictTransforms_eq_empty, Kollár's "do not have any k-fold intersections", by the chart computation: in the blow-up chart of index i the strict transform of the member whose coordinate is the block coordinate σ i is empty, and every member through a point of the centre is one of the block) — and defines the disjoining list of centres disjoinList m F by recursion on the multiplicity m = k, k − 1, …, 2, with the invariant carried as a hypothesis. Its properties (the final strict transforms are pairwise disjoint, every centre lies over Sing F, the centres have snc with the running total transform, compatibility with open inclusions) follow in DisjoinLemmas.lean, DisjoinBoundary.lean and DisjoinNatural.lean. The Hironaka library has the same construction for schemes (Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin.lean).

theorem Manifold.HypersurfaceFamily.meetLocus_strictTransforms_eq_empty {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {M' : Type u} [TopologicalSpace M'] [ChartedSpace E M'] [IsManifold (modelWithCornersSelf 𝕜 E) ⊤ M'] [T2Space M'] [SecondCountableTopology M'] {π : M' → M} {F : HypersurfaceFamily M} (hF : IsSnc ψ F) {m : ℕ} (hm : F.meetLocus (m + 1) = ∅) (h : IsBlowUp ψ (F.meetLocus m) m π) : (strictTransforms π (F.meetLocus m) F).meetLocus m = ∅

The step of [Kol07, 72]: where no point lies on m + 1 members, after blowing up the m-fold meet locus no point lies on m of the strict transforms. Off the centre the strict transforms are the preimages, so an m-fold point would map to a point of the centre; over a point a of the centre the m members through a are exactly the block of the adapted chart, the blow-up chart of index i through the point kills the strict transform of the member whose coordinate is σ i, while every strict transform through the point comes from a member through a — so at most m − 1 of them pass.

The disjoining list of centres

noncomputable def Hironaka.Manifold.disjoinList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) : Manifold.HypersurfaceFamily.IsSnc ψ₀ F → F.meetLocus (m + 1) = ∅ → AnalyticManifold.BlowUpSequence ψ₀ M

The disjoining blow-ups of [Kol07, 72] for an snc family with no (m + 1)-fold points, as a list of centres — nothing for m ≤ 1; for m + 2, blow up the (m + 2)-fold meet locus (a closed submanifold of codimension m + 2, IsSnc.isClosedSubmanifold_meetLocus) and continue with the strict transforms, which have no (m + 2)-fold point (meetLocus_strictTransforms_eq_empty). These are Kollár's k − 1 steps from m = k; the empty m-fold loci give empty centres, deleted by eraseEmpty afterwards ("ultimately the difference is only in some empty blow ups, and we can forget about those at the end", [Kol07, 72]; [Kol07, 32]).

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Manifold.disjoinList 0 x_1 x_2 x_3 = AnalyticManifold.BlowUpSequence.nil x
• Hironaka.Manifold.disjoinList 1 x_1 x_2 x_3 = AnalyticManifold.BlowUpSequence.nil x

@[simp]

theorem Hironaka.Manifold.disjoinList_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus 1 = ∅) : disjoinList 0 F hF hm = AnalyticManifold.BlowUpSequence.nil M

@[simp]

theorem Hironaka.Manifold.disjoinList_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus 2 = ∅) : disjoinList 1 F hF hm = AnalyticManifold.BlowUpSequence.nil M

theorem Hironaka.Manifold.length_disjoinList {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ₀ : E ≃L[𝕜] Fin n → 𝕜} (m : ℕ) {M : AnalyticManifold 𝕜 E} (F : Manifold.HypersurfaceFamily M.carrier) (hF : Manifold.HypersurfaceFamily.IsSnc ψ₀ F) (hm : F.meetLocus (m + 1) = ∅) : (disjoinList m F hF hm).length = m - 1

Kollár's "k − 1 steps" from m = k: the list at m + 2 has m + 1 centres.