The pulled-back exceptional divisors form a simple normal crossing divisor

In the proof of the principalization theorem [Kol07, 72], Π^* I = I_r · 𝒪_{X_r}(F) for an effective divisor F "supported on the total transform of ∑ E^i", and F is a simple normal crossing divisor, where F = ∑_j Π_{r,j+1}^* F_j is the sum of the exceptional divisors of the steps pulled back to the end result. This module proves that statement for every smooth blow-up sequence of order ≥ m starting with a marked triple: the ideal sheaf ∏_j Π_{r,j+1}^* F_j is invertible (each F_j is the inverse image of the center, an invertible ideal sheaf, and invertible ideal sheaves pull back to invertible ones along blow-ups) and its support lies in the final total transform E_r (π^{-1}(V(E_i)) ⊆ V(E_{i+1}): a point off the exceptional divisor lies on the strict transform of the member below it). By the uniqueness in the decomposition of an ideal into its monomial and nonmonomial parts [Kol07, Definition–Lemma 110], also [BM08, equation (5.2)] (eq_monomialPart_of_isInvertible_of_support_le), it is therefore the monomial of E_r with exponents ord_D at the irreducible components D, and a monomial of a simple normal crossing family is the ideal sheaf of a simple normal crossing divisor (Hironaka/Resolution/Algebraic/Snc/MonomialComponents.lean). The final family E_r has simple normal crossings by condition (3′) of [Kol07, Definition 66] iterated (IsOrderGeSeq.isSnc_totalTransformSeq), so the multiplicities accumulate exactly as Kollár's sum does.

• isInvertible_exceptionalAt, isInvertible_comap_stageMapBetween;
• preimage_support_subset_support_totalTransform, preimage_stageMap_support_subset, preimage_stageMapBetween_support_subset, support_exceptionalAt_le_support_totalTransformSeq;
• isIdealOfSncDivisor_prod_comap_exceptionalAt: the theorem on a marked triple.

Invertibility

theorem Hironaka.Sequence.isInvertible_exceptionalAt {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (i : Fin S.length) : (S.exceptionalAt i).IsInvertible

The exceptional divisor F_{i+1} = π_i^{-1}(Z_i) of a step [Kol07, Notation 19] is an invertible ideal sheaf (the exceptional ideal of a blow-up is invertible, carried across the cast X_1 = D.blowUp at the first step).

theorem Hironaka.Sequence.isInvertible_comap_stageMapBetween {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {i j : Fin (S.length + 1)} (h : j ≤ i) {K : (S.stage j).IdealSheafData} : K.IsInvertible → (K.comap (S.stageMapBetween i j h)).IsInvertible

An invertible ideal sheaf on X_j pulls back along Π_{ij} : X_i ⟶ X_j to an invertible one: the inverse image of an invertible ideal sheaf under a blow-up is invertible, iterated along the sequence.

Supports

theorem Hironaka.Sequence.preimage_support_subset_support_totalTransform {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (D : X.IdealSheafData) : ⇑D.blowUpπ ⁻¹' ↑E.support ⊆ ↑(E.totalTransform D).support

The inverse image of V(E) under the blow-up lies in the support of the total transform [Kol07, Definition 25]: a point off the exceptional divisor lies on the strict transform of a member through its image (mem_support_strictTransformAlong_iff_of_notMem_support).

theorem Hironaka.Sequence.preimage_stageMap_support_subset {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) : ⇑(S.stageMap i) ⁻¹' ↑E.support ⊆ ↑(S.totalTransformSeq E i).support

Π_i^{-1}(V(E)) ⊆ V(E_i) ([Kol07, Definition 25] iterated).

theorem Hironaka.Sequence.preimage_stageMapBetween_support_subset {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) {i l : Fin (S.length + 1)} (h : i ≤ l) : ⇑(S.stageMapBetween l i h) ⁻¹' ↑(S.totalTransformSeq E i).support ⊆ ↑(S.totalTransformSeq E l).support

Π_{li}^{-1}(V(E_i)) ⊆ V(E_l) for i ≤ l ([Kol07, Definition 25] iterated between two stages).

theorem Hironaka.Sequence.support_exceptionalAt_le_support_totalTransformSeq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (j : Fin S.length) : (S.exceptionalAt j).support ≤ (S.totalTransformSeq E j.succ).support

The exceptional divisor F_{j+1} is the last member of E_{j+1} = (π_j)^{-1}_{tot} E_j [Kol07, Definition 66, condition (1)], so its support lies in V(E_{j+1}).

The theorem

theorem Hironaka.Sequence.isIdealOfSncDivisor_prod_comap_exceptionalAt {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (S : T.X.left.BlowUpSequence) (hS : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E) : (∏ j : Fin S.length, (S.exceptionalAt j).comap (S.stageMapBetween (Fin.last S.length) j.succ ⋯)).IsIdealOfSncDivisor

Along a smooth blow-up sequence of order ≥ m starting with the marked triple T, the product of the exceptional divisors of the steps pulled back to the end result along the later steps, ∏_j Π_{r,j+1}^* F_j, is the ideal sheaf of an effective divisor supported on a simple normal crossing family ("F is a simple normal crossing divisor", [Kol07, 72]): it is invertible, its support lies in the final total transform E_r (which has simple normal crossings by condition (3′) of Definition 66 iterated), so it is its own monomial part [Kol07, Definition–Lemma 110], a monomial of the family E_r with exponents ord_D at the irreducible components D.