The disjoining list: the final strict transforms and the centres

Alongside disjoinList m F this module carries the family the recursion ends with — the strict transforms of the components along the whole list, disjoinFinal m F on the last stage — and proves Kollár's conclusions in [Kol07, 72]:

• "After (k − 1) steps we get rid of all pairwise intersections as well": the final strict transforms form a simple normal crossings divisor whose members are pairwise disjoint (no point lies on two of them, meetLocus 2 = ∅), so that "we can just declare that E is a single divisor" (Collapse.lean);
• every centre lies over the multiple locus Sing E — the m-fold meet loci for m ≥ 2 are inside Sing, and the multiple locus of the strict transforms lies over the multiple locus (CentersOver F.sing, the hypothesis of isAnalyticIsoOver_stageMap for clause (3) of [Kol07, Theorem 35] in ClauseThree.lean);
• the bridge to the boundary family: the member j of disjoinFinal is the strict transform strictTransformSeq (F.hyp j) at the last stage (the cons rule cons_strictTransformSeq_succ at every step) — the member originalIdx j of the boundary family totalTransformSeqFrom F there (hyp_originalIdx).

The Hironaka library has the corresponding statements in Hironaka/Resolution/Algebraic/Kol07/Thm35/Disjoin.lean.

theorem Manifold.HypersurfaceFamily.singularLocus_strictTransforms_subset {𝕜 : 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} {Y : Set M} {c : ℕ} {F : HypersurfaceFamily M} (h : IsBlowUp ψ Y c π) (hF : IsSnc ψ F) : (strictTransforms π Y F).singularLocus ⊆ π ⁻¹' F.singularLocus

A point on two distinct strict transforms lies over a point on the two members — the multiple locus of the strict transforms lies over the multiple locus (the disjoining centres of [Kol07, 72] stay over Sing E).

@[reducible, inline]

noncomputable abbrev Hironaka.Manifold.disjoinNext {𝕜 : 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) {m : ℕ} (hm : F.meetLocus (m + 2 + 1) = ∅) : Manifold.HypersurfaceFamily (Manifold.blowUp ψ₀ ⋯).carrier

The strict transforms under the first disjoining blow-up — the family the recursion disjoinList continues with at m + 2.

Equations

• Hironaka.Manifold.disjoinNext F hF hm = Manifold.HypersurfaceFamily.strictTransforms (⇑(Manifold.blowUpπ ψ₀ ⋯)) (F.meetLocus (m + 2)) F

theorem Hironaka.Manifold.disjoinNext_isSnc {𝕜 : 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) {m : ℕ} (hm : F.meetLocus (m + 2 + 1) = ∅) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (disjoinNext F hF hm)

theorem Hironaka.Manifold.meetLocus_disjoinNext {𝕜 : 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) {m : ℕ} (hm : F.meetLocus (m + 2 + 1) = ∅) : (disjoinNext F hF hm).meetLocus (m + 1 + 1) = ∅

theorem Hironaka.Manifold.disjoinList_succ_succ {𝕜 : 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) {m : ℕ} (hm : F.meetLocus (m + 2 + 1) = ∅) : disjoinList (m + 2) F hF hm = AnalyticManifold.BlowUpSequence.cons ⋯ (disjoinList (m + 1) (disjoinNext F hF hm) ⋯ ⋯)

The computation rule of disjoinList at m + 2 (definitional).

noncomputable def Hironaka.Manifold.disjoinFinalHyp {𝕜 : 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) = ∅) : F.ι → Set ((disjoinList m F hF hm).stage (Fin.last (disjoinList m F hF hm).length)).carrier

The strict transform of the component j along the whole disjoining list, on the last stage (by the recursion of disjoinList).

Equations

• Hironaka.Manifold.disjoinFinalHyp 0 x_1 x_2 x_4 x_3 = x_1.hyp x_3
• Hironaka.Manifold.disjoinFinalHyp 1 x_1 x_2 x_4 x_3 = x_1.hyp x_3
• Hironaka.Manifold.disjoinFinalHyp m.succ.succ x_1 x_2 x_4 x_3 = Hironaka.Manifold.disjoinFinalHyp (m + 1) (Hironaka.Manifold.disjoinNext x_1 x_2 x_4) ⋯ ⋯ x_3

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

The strict transforms of the components along the whole disjoining list — the family the recursion disjoinList ends with, on the last stage; indexed by the components of F.

Equations

• Hironaka.Manifold.disjoinFinal m F hF hm = { ι := F.ι, countable := ⋯, linearOrder := F.linearOrder, hyp := Hironaka.Manifold.disjoinFinalHyp m F hF hm }

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

theorem Hironaka.Manifold.disjoinFinal_succ_succ {𝕜 : 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) {m : ℕ} (hm : F.meetLocus (m + 2 + 1) = ∅) : disjoinFinal (m + 2) F hF hm = disjoinFinal (m + 1) (disjoinNext F hF hm) ⋯ ⋯

The computation rule of disjoinFinal at m + 2 (definitional).

theorem Hironaka.Manifold.disjoinFinal_isSnc {𝕜 : 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) = ∅) : Manifold.HypersurfaceFamily.IsSnc ψ₀ (disjoinFinal m F hF hm)

The final family is a simple normal crossings divisor (isSnc_strictTransforms at every step).

theorem Hironaka.Manifold.meetLocus_two_disjoinFinal_eq_empty {𝕜 : 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) = ∅) : (disjoinFinal m F hF hm).meetLocus 2 = ∅

Kollár's "after (k − 1) steps we get rid of all pairwise intersections" [Kol07, 72]: the final strict transforms are pairwise disjoint — no point lies on two of them (the invariant meetLocus (m + 1) = ∅ carried down to m = 1).

theorem Hironaka.Manifold.centersOver_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).toSuccession.CentersOver F.singularLocus

Every centre of the disjoining list of [Kol07, 72] lies over the multiple locus Sing F — the (m + 2)-fold meet locus is inside Sing F, and the centres of the rest lie over the multiple locus of the strict transforms, which lies over Sing F.

theorem Hironaka.Manifold.hyp_disjoinFinal {𝕜 : 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) = ∅) (j : F.ι) : (disjoinFinal m F hF hm).hyp j = (disjoinList m F hF hm).toSuccession.strictTransformSeq (F.hyp j) (Fin.last (disjoinList m F hF hm).toSuccession.length)

The members of the final family are the strict transforms of the components along the list (strictTransformSeq at the last stage; the cons rule is cons_strictTransformSeq_succ) — hence, by hyp_originalIdx, the members originalIdx j of the boundary family totalTransformSeqFrom F at the last stage.