The isomorphism locus of a blow-up sequence

In the proof of Theorem 107, Kollár runs the order reduction of the monomial part M(I) on X ∖ cosupp N(I), where I = M(I) [Kol07, 111, Step 3]. This library runs it on X itself for (M(I), m) and reads the result for (I, m). Over cosupp N(I) nothing happens: every center lies in cosupp(M_i, m), which misses the preimage of cosupp N(I) because there ord M_i = ord M(I) ≤ ord I < m after the second step; and a blow-up sequence whose centers avoid the preimages of a set C is an isomorphism over C, with the marked transform there the pullback of the starting ideal.

This module proves the two halves of that statement for any scheme (identities of stalks off the centers; no field, no smoothness) and the propagation of the disjointness along a smooth sequence:

• stalkIdeal_markedTransform_congr, stalkIdeal_markedTransformSeq_congr: the stalk of a marked transform at x depends only on the stalk of the starting ideal at the image of x (the marked transform is (π^* I) : (π^* Z)^m with π^* Z invertible, and colons by invertible ideals are read stalkwise); so ideals with equal stalks over an open have equal marked transforms over its preimage, Kollár's "I = M(I) off cosupp N(I)" transported along the sequence;
• ord_markedTransform_of_notMem: off the exceptional divisor the order of the marked transform is the order at the image (the marked analogue of ord_weakTransform_of_notMem);
• isIso_over_of_centers_disjoint, ord_markedTransformSeq_eq_of_disjoint: along a sequence whose centers avoid the preimages of C, at every point over C the stage map is an isomorphism of stalks (a blow-up is an isomorphism off its center, isIso_stalkMap_π_of_notMem_support, composed along the stages) and the marked transform's stalk is the stalk of the pulled-back ideal (the exceptional stalk is the unit ideal there, stalkIdeal_markedTransform_of_notMem); hence the order there is the order at the image;
• center_disjoint_of_isOrderGeSeq_of_lt: a smooth blow-up sequence of order ≥ m for (M, m, E) on a smooth scheme over a field of characteristic zero has every center disjoint from the preimage of any set on which ord M < m. By induction along the sequence: the center lies in cosupp(M_i, m) (condition (4′) of [Kol07, Definition 66] at the generic points, at every point by upper semicontinuity), and over the set the order is unchanged (the earlier blow-ups are isomorphisms there).

The restriction-level form of the isomorphism statement, IsIso (S.composite ∣_ U), is in Hironaka/Resolution/Algebraic/Kol07/IsoRestrict.lean.

theorem Hironaka.Sequence.stalkIdeal_markedTransform_congr {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) {I J : X.IdealSheafData} (m : ℕ) {y : ↥D.blowUp} (h : I.stalkIdeal (D.blowUpπ y) = J.stalkIdeal (D.blowUpπ y)) : (I.markedTransform D m).stalkIdeal y = (J.markedTransform D m).stalkIdeal y

The stalk of a marked transform (π^* I) : (π^* Z)^m [Kol07, Definition 60] at y is determined by the stalk of the ideal at π y: two ideals with the same stalk at π y have marked transforms with the same stalk at y (the colon by the invertible (π^* Z)^m is read stalkwise).

theorem Hironaka.Sequence.stalkIdeal_markedTransformSeq_congr {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {I J : X.IdealSheafData} (m : ℕ) (i : Fin (S.length + 1)) (x : ↥(S.stage i)) (h : I.stalkIdeal ((S.stageMap i) x) = J.stalkIdeal ((S.stageMap i) x)) : (S.markedTransformSeq I m i).stalkIdeal x = (S.markedTransformSeq J m i).stalkIdeal x

The stalk of the marked transform (I_i, m) at x is determined by the stalk of I at Π_i x: two starting ideals with the same stalk at Π_i x have marked transforms with the same stalk at x (Kollár's "I = M(I)" off cosupp N(I), [Kol07, 111, Step 2], transported along a sequence).

theorem Hironaka.Sequence.ord_markedTransform_of_notMem {X : AlgebraicGeometry.Scheme} (Z K : X.IdealSheafData) (c : ℕ) {q : ↥Z.blowUp} (hq : q ∉ (Z.comap Z.blowUpπ).support) : (K.markedTransform Z c).ord q = K.ord (Z.blowUpπ q)

Off the exceptional divisor the order of the marked transform is the order of the ideal at the image point: the blow-up is a local isomorphism there and the order is read in isomorphic local rings (ord_map_ringEquiv). The marked analogue of ord_weakTransform_of_notMem.

theorem Hironaka.Sequence.isIso_over_of_centers_disjoint {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {I : X.IdealSheafData} {m : ℕ} {C : Set ↥X} (hZ : ∀ (i : Fin S.length), Disjoint (↑(S.center i).support) (⇑(S.stageMap i.castSucc) ⁻¹' C)) (i : Fin (S.length + 1)) (x : ↥(S.stage i)) (hx : (S.stageMap i) x ∈ C) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap i) x) ∧ (S.markedTransformSeq I m i).stalkIdeal x = (I.comap (S.stageMap i)).stalkIdeal x

Along a blow-up sequence whose centers avoid the preimages of a set C, the sequence is an isomorphism over C and the marked transform there is the pullback: at every point over C the stage map is an isomorphism of stalks (a blow-up is an isomorphism off its center, isIso_stalkMap_π_of_notMem_support, composed along the stages) and the marked transform's stalk is the stalk of the pulled-back ideal (the exceptional stalk is the unit ideal there, stalkIdeal_markedTransform_of_notMem). Not in the sources; holds on any scheme.

theorem Hironaka.Sequence.ord_markedTransformSeq_eq_of_disjoint {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {I : X.IdealSheafData} {m : ℕ} {C : Set ↥X} (hZ : ∀ (i : Fin S.length), Disjoint (↑(S.center i).support) (⇑(S.stageMap i.castSucc) ⁻¹' C)) (i : Fin (S.length + 1)) (x : ↥(S.stage i)) (hx : (S.stageMap i) x ∈ C) : (S.markedTransformSeq I m i).ord x = I.ord ((S.stageMap i) x)

The order form of isIso_over_of_centers_disjoint: at a point over C the marked transform has the order of the ideal at the image (the order is read in isomorphic local rings, ord_map_ringEquiv). Holds on any scheme.

theorem Hironaka.Sequence.center_disjoint_of_isOrderGeSeq_of_lt {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (S : X.BlowUpSequence) {M : X.IdealSheafData} {m : ℕ} {E : X.DivisorFamily} : S.IsOrderGeSeq f M m E → ∀ {C : Set ↥X}, (∀ x ∈ C, M.ord x < ↑m) → ∀ (i : Fin S.length), Disjoint (↑(S.center i).support) (⇑(S.stageMap i.castSucc) ⁻¹' C)

Along a smooth blow-up sequence of order ≥ m for (M, m, E), every center avoids the preimage of a set C on which ord M < m. By induction along the sequence: the center Z_i lies in cosupp(M_i, m) (at its generic points by condition (4′) of [Kol07, Definition 66], at every point by upper semicontinuity), while over C the order of M_i is the order of M at the image (ord_markedTransform_of_notMem, the earlier blow-ups being isomorphisms there), hence < m.