The total exceptional locus and the points off the centers

The total exceptional set of a sequence of blow-ups is Ex_tot(Π) := ⋃_i (π_i ∘ ⋯ ∘ π_{r−1})⁻¹(Z_i), the union of the preimages of the centers [Kol07, Definition 25], and a blow-up is an isomorphism off its center, so the composite Π_i is a local isomorphism at every point of X_i lying over no center, with the strict transform there the pull-back of the subscheme. The proof of resolution from principalization needs both facts along a sequence, at the level of points and stalks ("g⁻¹(Sing X̄) = Z_j ∩ Ex_tot(π_0 ⋯ π_{j−1})" in the proof of [Kol07, Theorem 27]):

• mem_support_totalTransformSeq_iff: a point of the i-th stage lies on the total transform of the family E iff it lies over E or over one of the earlier centers ([Kol07, Definition 25], by induction from the one-step support_totalTransform_eq).
• isIso_stalkMap_stageMap_of_forall_notMem, stalkIdeal_strictTransformSeq_of_forall_notMem: at a point over no earlier center the stage map is an isomorphism on stalks and the strict transform's stalk is the image of the subscheme's stalk (the one-step isIso_stalkMap_π_of_notMem_support and stalkIdeal_strictTransformAlong_of_notMem_support, composed along the stages; the pointwise form of isIso_over_of_centers_disjoint).

The schemes are arbitrary, locally Noetherian where the support law of the strict transform needs it.

The support of the total transform along a sequence

theorem Hironaka.Sequence.mem_support_totalTransform_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (F : X.DivisorFamily) (D : X.IdealSheafData) (x' : ↥D.blowUp) : x' ∈ (F.totalTransform D).support ↔ D.blowUpπ x' ∈ F.support ∨ D.blowUpπ x' ∈ D.support

support_totalTransform_eq, pointwise: a point of the blow-up lies on the total transform of F iff its image lies on F or on the center.

theorem Hironaka.Sequence.mem_support_totalTransformSeq_iff_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) [AlgebraicGeometry.IsLocallyNoetherian X] (E : X.DivisorFamily) (j : ℕ) (hj : j < S.length + 1) (p : ↥(S.stage ⟨j, hj⟩)) : p ∈ (S.totalTransformSeq E ⟨j, hj⟩).support ↔ (S.stageMap ⟨j, hj⟩) p ∈ E.support ∨ ∃ (m : ℕ) (hm : m < S.length) (hmj : m < j), (S.stageMapBetween ⟨j, hj⟩ ⟨m, ⋯⟩ ⋯) p ∈ (S.center ⟨m, hm⟩).support

The total exceptional set [Kol07, Definition 25], in the ⟨j, hj⟩ form: a point of the j-th stage lies on the total transform of E iff its image lies on E or its image at some earlier stage m < j lies on the center Z_m.

theorem Hironaka.Sequence.mem_support_totalTransformSeq_iff {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (E : X.DivisorFamily) (i : Fin (S.length + 1)) (p : ↥(S.stage i)) : p ∈ (S.totalTransformSeq E i).support ↔ (S.stageMap i) p ∈ E.support ∨ ∃ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) p ∈ (S.center m).support

A point of a stage lies on the total transform of E iff it lies over E or over one of the earlier centers [Kol07, Definition 25].

Off the centers: stalk isomorphisms and the strict transform

theorem Hironaka.Sequence.stalkIdeal_map_stalkMap_id {X : AlgebraicGeometry.Scheme} (J : X.IdealSheafData) (p : ↥X) : Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (CategoryTheory.CategoryStruct.id X) p)) (J.stalkIdeal ((CategoryTheory.CategoryStruct.id X) p)) = J.stalkIdeal p

The identity's stalk map is the identity on ideals.

theorem Hironaka.Sequence.isIso_stalkMap_stageMap_and_stalkIdeal_strictTransformSeq_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (j : ℕ) (hj : j < S.length + 1) (p : ↥(S.stage ⟨j, hj⟩)) : (∀ (m : ℕ) (hm : m < S.length) (hmj : m < j), (S.stageMapBetween ⟨j, hj⟩ ⟨m, ⋯⟩ ⋯) p ∉ (S.center ⟨m, hm⟩).support) → CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap ⟨j, hj⟩) p) ∧ (S.strictTransformSeq J ⟨j, hj⟩).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap ⟨j, hj⟩) p)) (J.stalkIdeal ((S.stageMap ⟨j, hj⟩) p))

A blow-up is an isomorphism off its center, along a sequence, pointwise, in the ⟨j, hj⟩ form: at a point of the j-th stage lying over no earlier center, the stage map is an isomorphism on stalks and the strict transform of J has the stalk of the pull-back of J.

theorem Hironaka.Sequence.isIso_stalkMap_stageMap_of_forall_notMem {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (i : Fin (S.length + 1)) (p : ↥(S.stage i)) (h : ∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) p ∉ (S.center m).support) : CategoryTheory.IsIso (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap i) p)

At a point over no earlier center the stage map is an isomorphism on stalks (a blow-up is an isomorphism off its center).

theorem Hironaka.Sequence.stalkIdeal_strictTransformSeq_of_forall_notMem {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (i : Fin (S.length + 1)) (p : ↥(S.stage i)) (h : ∀ (m : Fin S.length) (hmi : ↑m < ↑i), (S.stageMapBetween i m.castSucc ⋯) p ∉ (S.center m).support) : (S.strictTransformSeq J i).stalkIdeal p = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap (S.stageMap i) p)) (J.stalkIdeal ((S.stageMap i) p))

At a point over no earlier center the strict transform of J has the stalk of the pull-back (the birational transform of [Kol07, 30.2] off the centers).