The total transform off the centre

[Kol07, Definition 25] and the proof of [Hau14, Proposition 5.3]: off the exceptional divisor the blow-up π : B_Z X → X is a local isomorphism, so the total transform π^{-1}_{tot}(E) = (π_*^{-1} E^i, F) "restricts to E" there. At a point x' ∈ B_Z X with π(x') ∉ Z:

• the stalk map π^* : 𝒪_{X,π(x')} → 𝒪_{B,x'} is an isomorphism (isIso_stalkMap_π_of_notMem_support: π is an isomorphism over X ∖ Z, and Mathlib's stalkwise characterization of isomorphisms);
• the exceptional ideal has stalk (1) at x', so the saturation defining the strict transform is trivial there and (π_*^{-1} D)_{x'} = π^*(D_{π(x')}) (stalkIdeal_strictTransformAlong_of_notMem_support), whence x' ∈ π_*^{-1} D ⟺ π(x') ∈ D (mem_support_strictTransformAlong_iff_of_notMem_support);
• Kollár's conditions (1)–(3) at π(x') for E — a regular system of parameters z and an injective assignment of coordinates to the components through π(x') — transport along π^* to the family (π_*^{-1} E^i, F) at x', the entry F being absent (exists_snc_data_totalTransform_of_notMem_support).

These are the facts about a blow-up sequence away from its centres that Hironaka.Sequence (OffCenters, CosuppTransport, TransformDerivative) and Hironaka.Resolution (OffCentreTransport, Absorption) use.

Sources: [Kol07, Definition 25]; [Hau14, Proposition 5.3] (the proof).

theorem AlgebraicGeometry.π_mem_compl_support_of_notMem_support {X : Scheme} (Z : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) : Z.blowUpπ x' ∈ Z.support.compl

A point of the blow-up off the exceptional divisor lies over the complement of the centre.

theorem AlgebraicGeometry.isIso_stalkMap_π_of_notMem_support {X : Scheme} (Z : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) : CategoryTheory.IsIso (Scheme.Hom.stalkMap Z.blowUpπ x')

[Kol07, Definition 25]: at a point x' of B_Z X over X ∖ Z, the stalk map π^* : 𝒪_{X,π(x')} → 𝒪_{B,x'} is an isomorphism — π is an isomorphism over X ∖ Z, and an isomorphism of schemes has isomorphic stalk maps.

noncomputable def AlgebraicGeometry.stalkMapπEquiv {X : Scheme} (Z : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) : ↑(X.presheaf.stalk (Z.blowUpπ x')) ≃+* ↑(Z.blowUp.presheaf.stalk x')

The stalk map at a point off the exceptional divisor, as a ring equivalence.

Equations

• AlgebraicGeometry.stalkMapπEquiv Z hx' = (CategoryTheory.asIso (AlgebraicGeometry.Scheme.Hom.stalkMap Z.blowUpπ x')).commRingCatIsoToRingEquiv

theorem AlgebraicGeometry.stalkMapπEquiv_apply {X : Scheme} (Z : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) (a : ↑(X.presheaf.stalk (Z.blowUpπ x'))) : (stalkMapπEquiv Z hx') a = (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) a

theorem Ideal.colon_coe_top {R : Type u_1} [CommRing R] (I : Ideal R) : Submodule.colon I ↑⊤ = I

The colon by the unit ideal is the ideal itself.

theorem AlgebraicGeometry.stalkIdeal_strictTransformAlong_of_notMem_support {X : Scheme} (Z D : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) : (D.strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)).stalkIdeal x' = Ideal.map (CommRingCat.Hom.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) (D.stalkIdeal (Z.blowUpπ x'))

At x' off the exceptional divisor the strict transform of D has stalk π^*(D_{π(x')}) — the exceptional ideal has stalk (1), so the saturation is trivial.

theorem AlgebraicGeometry.mem_support_strictTransformAlong_iff_of_notMem_support {X : Scheme} (Z D : X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) : x' ∈ (D.strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)).support ↔ Z.blowUpπ x' ∈ D.support

Off the exceptional divisor, x' lies on the strict transform of D iff π(x') lies on D.

noncomputable def AlgebraicGeometry.totalTransformFamily {X : Scheme} (Z : X.IdealSheafData) {ι : Type u_1} (E : ι → X.IdealSheafData) : ι ⊕ PUnit.{u + 1} → Z.blowUp.IdealSheafData

The unbundled total-transform family (π_*^{-1} E^i, F) on B_Z X, indexed by ι ⊕ PUnit (the body of DivisorFamily.totalTransform).

Equations

• AlgebraicGeometry.totalTransformFamily Z E = Sum.elim (fun (i : ι) => (E i).strictTransformAlong Z.blowUpπ (Z.comap Z.blowUpπ)) fun (x : PUnit.{?u.2 + 1}) => Z.comap Z.blowUpπ

theorem AlgebraicGeometry.exists_snc_data_totalTransform_of_notMem_support {X : Scheme} (Z : X.IdealSheafData) {ι : Type u_1} (E : ι → X.IdealSheafData) {x' : ↥Z.blowUp} (hx' : x' ∉ (Z.comap Z.blowUpπ).support) {n : ℕ} {z : Fin n → ↑(X.presheaf.stalk (Z.blowUpπ x'))} (hz : IsLocalRing.maximalIdeal ↑(X.presheaf.stalk (Z.blowUpπ x')) = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim ↑(X.presheaf.stalk (Z.blowUpπ x'))) (c : { i : ι // Z.blowUpπ x' ∈ (E i).support } → Fin n) (hcinj : Function.Injective c) (hc : ∀ (i : { i : ι // Z.blowUpπ x' ∈ (E i).support }), (E ↑i).stalkIdeal (Z.blowUpπ x') = Ideal.span {z (c i)}) : (IsLocalRing.maximalIdeal ↑(Z.blowUp.presheaf.stalk x') = Ideal.span (Set.range fun (i : Fin n) => (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) (z i)) ∧ ↑n = ringKrullDim ↑(Z.blowUp.presheaf.stalk x')) ∧ ∃ (c' : { k : ι ⊕ PUnit.{u + 1} // x' ∈ (totalTransformFamily Z E k).support } → Fin n), Function.Injective c' ∧ ∀ (k : { k : ι ⊕ PUnit.{u + 1} // x' ∈ (totalTransformFamily Z E k).support }), (totalTransformFamily Z E ↑k).stalkIdeal x' = Ideal.span {(CategoryTheory.ConcreteCategory.hom (Scheme.Hom.stalkMap Z.blowUpπ x')) (z (c' k))}

[Kol07, Definition 25], the proof of [Hau14, Proposition 5.3]: Kollár's conditions (1)–(3) at a point x' of B_Z X off the exceptional divisor — the regular system of parameters z at x = π(x') and the injective assignment c of coordinates to the components of E through x transport along the isomorphism π^* to the family (π_*^{-1} E^i, F) at x'; the entry F is absent there.