The monomial formula at a stalk, for one blow-up

Kollár's explicit formula for the principalization, Π^* I = 𝒪(−∑ Π^*_{r,j+1} F_j) [Kol07, 72], is assembled stage by stage in MonomialSeq.lean; this module holds the facts about one blowing-up π : M' → M along a centre Y having simple normal crossings with the boundary F:

• exact division at mark 1 ([Kol07, (60.1)]): the total transform of an ideal sheaf J of order ≥ 1 along Y is the exceptional ideal times the marked transform, π⁻¹(J) = I_F · π_*^{-1}(J, 1) at every stalk (stalkIdeal_totalTransform_eq_mul_birationalTransform) — the marked transform's stalk is the colon (π⁻¹(J)_p : I_{F,p}) and π⁻¹(J)_p ⊆ I_{F,p} because J_a ⊆ I_{Y,a} on the centre, so the colon by the principal ideal I_{F,p} = (u) divides exactly (Ideal.span_singleton_mul_colon_of_le);
• the stalks of the exceptional ideal are the vanishing ideals of the exceptional divisor (IsBlowUp.stalkIdeal_exceptionalIdealSheaf_eq_vanishingStalk; more generally an ideal sheaf of a closed submanifold has its vanishing ideals as stalks, IsIdealSheafOf.stalkIdeal_eq_vanishingStalk);
• the transport of a boundary member: the vanishing ideal of a member E^j through π p pulls back along π to I_{F,p}^ε times the vanishing ideal of its strict transform, ε ∈ {0, 1} (exists_map_germMap_vanishingStalk_hyp_eq'). In a blow-up chart of index i over an adapted chart (germMap_coord_self, germMap_coord_of_ne, germMap_coord_off): the coordinate z_{c j} of the member pulls back to u_i when c j = σ i (the strict transform misses the chart, ε = 1), to u_i · u_{c j} for a block coordinate c j = σ k, k ≠ i (ε = 1), and to u_{c j} off the block (ε = 0); in each case the strict transform is the zero set of u_{c j} in the chart (strictTransform_inter_source_self, _of_ne, _off), so its vanishing ideal is (u_{c j}). Off the exceptional divisor the blowing-up is a local isomorphism (condition (1) of [BM88, Definition 4.1]), the strict transform is the preimage there and the vanishing ideal pulls back along the bijective germ map (ε = 0).

This is the computation behind Bierstone–Milman's remark that when the centre and the boundary "simultaneously have only normal crossings", the transformed boundary is again a collection of smooth hypersurfaces having only normal crossings [BM97, (1.2)], and behind the total transform of a divisor in [Kol07, Definition 25].

Vanishing ideals of closed hypersurfaces

theorem Hironaka.Manifold.vanishingStalk_inter_of_mem_nhds {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z t : Set M} {x : M} (ht : t ∈ nhds x) : Manifold.vanishingStalk (Z ∩ t) x = Manifold.vanishingStalk Z x

The vanishing ideal at x sees only the germ of the set: Z ∩ t = Z near x for a neighbourhood t of x.

theorem Hironaka.Manifold.vanishingStalk_eq_top_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z : Set M} (hZ : IsClosed Z) {x : M} (hx : x ∉ Z) : Manifold.vanishingStalk Z x = ⊤

Off a closed set the vanishing ideal is the unit ideal.

theorem Manifold.IsClosedSubmanifold.vanishingStalk_eq_span_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z : Set M} (hZ : IsClosedSubmanifold ψ Z 1) {φ : OpenPartialHomeomorph M E} {σ : Fin 1 ↪ Fin n} (hφ : IsAdaptedChart ψ Z φ σ) {p : M} (hp : p ∈ φ.source) : vanishingStalk Z p = Ideal.span {coord E ψ φ ⋯ hp (σ 0)}

In a chart adapted to a closed hypersurface Z, the vanishing ideal of Z at a point of the chart is spanned by the adapted coordinate — also off Z, where the coordinate is a unit and both sides are the unit ideal.

theorem Manifold.IsClosedSubmanifold.vanishingStalk_eq_span_coord_of_inter_source {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z : Set M} (hZ : IsClosedSubmanifold ψ Z 1) {φ : OpenPartialHomeomorph M E} (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {k : Fin n} (hS : ∀ x ∈ φ.source, x ∈ Z ↔ ψ (↑φ x) k = 0) {p : M} (hp : p ∈ φ.source) : vanishingStalk Z p = Ideal.span {coord E ψ φ hφ hp k}

The vanishing ideal of a closed hypersurface Z at a point of a chart in which Z is the zero set of the coordinate k.

theorem Manifold.IsIdealSheafOf.stalkIdeal_eq_vanishingStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) {J : IdealSheaf (structureSheaf 𝕜 E M)} (hJ : IsIdealSheafOf ψ Y c J) (a : M) : J.stalkIdeal a = vanishingStalk Y a

An ideal sheaf of the closed submanifold Y (IsIdealSheafOf) has the vanishing ideals of Y as stalks: the span of the adapted coordinates is the kernel of the restriction of germs, the unit ideal off Y.

theorem Manifold.IsClosedSubmanifold.stalkIdeal_idealSheaf_eq_vanishingStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Y : Set M} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (a : M) : hY.idealSheaf.stalkIdeal a = vanishingStalk Y a

The ideal sheaf of a closed submanifold has the vanishing ideals as stalks.

theorem Manifold.IsClosedSubmanifold.exists_vanishingStalk_eq_span_singleton {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {Z : Set M} (hZ : IsClosedSubmanifold ψ Z 1) (p : M) : ∃ (u : ↑((structureSheaf 𝕜 E M).presheaf.stalk p)), vanishingStalk Z p = Ideal.span {u}

A closed hypersurface has principal vanishing ideals (the adapted coordinate on it, 1 off it).

One blowing-up: exact division at mark 1 and the transport of the members

theorem Manifold.IsBlowUp.stalkIdeal_exceptionalIdealSheaf_eq_vanishingStalk {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} (hY : IsClosedSubmanifold ψ Y c) (h : IsBlowUp ψ Y c π) (p : M'.carrier) : (IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal p = vanishingStalk (π ⁻¹' Y) p

The stalks of the exceptional ideal I_F = π^*I_Y are the vanishing ideals of the exceptional divisor π⁻¹(Y).

theorem Hironaka.Manifold.stalkIdeal_totalTransform_eq_mul_birationalTransform {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (J : M.IdealSheaf) (hm : ∀ a ∈ Y, ↑1 ≤ hY.idealSheaf.ordAlongIdeal J a) (p : M'.carrier) : (Manifold.IdealSheaf.pullback π ⋯ J).stalkIdeal p = (Manifold.IdealSheaf.pullback π ⋯ hY.idealSheaf).stalkIdeal p * (Manifold.MarkedIdealSheaf.birationalTransform hY h { I := J, m := 1 }).I.stalkIdeal p

Kollár's (60.1) at mark 1, in its exact form [Kol07, (60.1)]: when ord_Y J ≥ 1, the total transform of J is the exceptional ideal times the marked transform at every stalk, π⁻¹(J)_p = I_{F,p} · π_*^{-1}(J, 1)_p — the marked transform's stalk is the colon (π⁻¹(J)_p : I_{F,p}) (isDivExceptional_birationalTransform), π⁻¹(J)_p ⊆ I_{F,p} because J_a ⊆ I_{Y,a} on the centre, and I_{F,p} is principal.

theorem Hironaka.Manifold.exists_map_germMap_vanishingStalk_hyp_eq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) {φ : OpenPartialHomeomorph M.carrier E} {σ : Fin c ↪ Fin n} (hφ : Manifold.IsAdaptedChart ψ Y φ σ) {p : M'.carrier} {cidx : { j : F.ι // π p ∈ F.hyp j } → Fin n} (hc : Manifold.HypersurfaceFamily.IsSncChartAt ψ F φ (π p) cidx) {i : Fin c} {Φ : OpenPartialHomeomorph M'.carrier E} (hΦ : Manifold.IsBlowUpChart ψ π φ σ i Φ) (hp : p ∈ Φ.source) (j : { j : F.ι // π p ∈ F.hyp j }) : ∃ ε ≤ 1, Ideal.map (Manifold.germMap π ⋯ p) (Manifold.vanishingStalk (F.hyp ↑j) (π p)) = Manifold.vanishingStalk (π ⁻¹' Y) p ^ ε * Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl ↑j))) p

The chart formulas for a boundary member: in a blow-up chart Φ of index i over a chart φ adapted to Y which is an snc chart of F at π p, the vanishing ideal of the member E^j through π p pulls back to I_{F,p}^ε · (vanishing ideal of its strict transform), ε = 1 iff the member's coordinate c j lies in the centre's block σ: z_{σ i} ∘ π = u_i (the strict transform misses the chart), z_{σ k} ∘ π = u_i · u_{σ k} for k ≠ i, and z_j ∘ π = u_j off the block, the strict transform being {u_{c j} = 0} in the chart in the last two cases.

theorem Hironaka.Manifold.exists_map_germMap_vanishingStalk_hyp_eq_of_mem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) {p : M'.carrier} (hpY : π p ∈ Y) (j : { j : F.ι // π p ∈ F.hyp j }) : ∃ ε ≤ 1, Ideal.map (Manifold.germMap π ⋯ p) (Manifold.vanishingStalk (F.hyp ↑j) (π p)) = Manifold.vanishingStalk (π ⁻¹' Y) p ^ ε * Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl ↑j))) p

The member transport at a point over the centre: the charts of HasSncWith and a blow-up chart through the point (condition (2) of [BM88, Definition 4.1]).

theorem Hironaka.Manifold.map_germMap_vanishingStalk_hyp_of_notMem {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) {p : M'.carrier} (hpY : π p ∉ Y) (j : F.ι) : Ideal.map (Manifold.germMap π ⋯ p) (Manifold.vanishingStalk (F.hyp j) (π p)) = Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl j))) p

Off the exceptional divisor the blowing-up is a local analytic isomorphism (condition (1) of [BM88, Definition 4.1]): the vanishing ideal of a member pulls back along the bijective germ map to the vanishing ideal of its preimage, which is the strict transform there.

theorem Hironaka.Manifold.exists_map_germMap_vanishingStalk_hyp_eq' {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} {ψ : E ≃L[𝕜] Fin n → 𝕜} {M M' : AnalyticManifold 𝕜 E} {π : M'.carrier → M.carrier} {Y : Set M.carrier} {c : ℕ} {F : Manifold.HypersurfaceFamily M.carrier} (hY : Manifold.IsClosedSubmanifold ψ Y c) (h : Manifold.IsBlowUp ψ Y c π) (hF : Manifold.HypersurfaceFamily.IsSnc ψ F) (hsnc : Manifold.HypersurfaceFamily.HasSncWith ψ F Y c) (p : M'.carrier) (j : { j : F.ι // π p ∈ F.hyp j }) : ∃ ε ≤ 1, Ideal.map (Manifold.germMap π ⋯ p) (Manifold.vanishingStalk (F.hyp ↑j) (π p)) = Manifold.vanishingStalk (π ⁻¹' Y) p ^ ε * Manifold.vanishingStalk ((Manifold.HypersurfaceFamily.totalTransform π Y F).hyp (toLex (Sum.inl ↑j))) p

The member transport at every point: over the centre by the chart formulas, off it by the local isomorphism (with ε = 0).