A blow-up whose centre misses a closed subscheme

In the isolation passage of the proof of [Wlo05, Theorem 4.7.1], after the strict transform of a component is isolated, the later centres of the modified run either miss the isolated strict transforms or are strata of the boundary transversal to them. This module is the first case: a blow-up whose centre is disjoint from a closed subscheme Z changes nothing near Z. The blow-up is an isomorphism off the exceptional divisor (isIso_stalkMap_π_of_notMem_support), so the pull-back of the ideal of Z is its strict transform, simple normal crossings with the boundary pass to the total transform and the strict transform (the snc coordinates transport along the isomorphism of stalks, exists_snc_data_totalTransform_of_notMem_support), and "contained in no member near any point" passes as well. Stalkwise throughout; no coordinates are computed. Simple normal crossings and the total transform are those of [Kol07, Definition 24] and [Kol07, Definition 25]. Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedProtected and, for the two elementary lemmas on disjoint closed sets, throughout the loop modules.

theorem Hironaka.Resolution.notMem_of_disjoint_closeds {X : AlgebraicGeometry.Scheme} {A B : TopologicalSpace.Closeds ↥X} (h : Disjoint A B) {x : ↥X} (hx : x ∈ A) : x ∉ B

A point of one of two disjoint closed sets is not in the other.

theorem Hironaka.Resolution.disjoint_closeds_iff {X : AlgebraicGeometry.Scheme} {A B : TopologicalSpace.Closeds ↥X} : Disjoint A B ↔ ∀ x ∈ A, x ∉ B

Two closed sets are disjoint iff no point of the first lies in the second.

theorem Hironaka.Resolution.notMem_support_exceptionalDivisor_of_mem_support_strictTransform {X : AlgebraicGeometry.Scheme} (D Z : X.IdealSheafData) [AlgebraicGeometry.IsLocallyNoetherian X] (hdisj : Disjoint D.support Z.support) {x' : ↥D.blowUp} (hx' : x' ∈ (Z.strictTransform D).support) : x' ∉ D.exceptionalDivisor.support

A point of the strict transform of Z along a centre disjoint from Z is off the exceptional divisor.

theorem Hironaka.Resolution.stalkIdeal_strictTransform_of_notMem_support_exceptionalDivisor {X : AlgebraicGeometry.Scheme} (D Z : X.IdealSheafData) {x' : ↥D.blowUp} (hx' : x' ∉ D.exceptionalDivisor.support) : (Z.strictTransform D).stalkIdeal x' = Ideal.map (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.stalkMap D.blowUpπ x')) (Z.stalkIdeal (D.blowUpπ x'))

Off the exceptional divisor the stalk of the strict transform is the image of the stalk below (stalkIdeal_strictTransformAlong_of_notMem_support for strictTransform).

theorem Hironaka.Resolution.comap_blowUpπ_eq_strictTransform_of_disjoint {X : AlgebraicGeometry.Scheme} (D Z : X.IdealSheafData) (hdisj : Disjoint D.support Z.support) : Z.comap D.blowUpπ = Z.strictTransform D

The pull-back of the ideal of a closed subscheme along a blow-up whose centre misses it is its strict transform (the isolation passage of the proof of [Wlo05, Theorem 4.7.1], the disjoint case): stalkwise the unit ideal on the exceptional divisor, the image of the stalk below elsewhere.

theorem Hironaka.Resolution.hasSncWith_totalTransform_strictTransform_of_disjoint {X : AlgebraicGeometry.Scheme} (D Z : X.IdealSheafData) [AlgebraicGeometry.IsLocallyNoetherian X] (E : X.DivisorFamily) (hdisj : Disjoint D.support Z.support) (hZ : E.HasSncWith Z) : (E.totalTransform D).HasSncWith (Z.strictTransform D)

[Kol07, Definition 25] read off the centre: if Z has simple normal crossings with E and the centre D misses Z, the strict transform of Z has simple normal crossings with the total transform of E — the snc coordinates at the point below transport along the isomorphism of stalks, and the stalk of the strict transform is the image of that of Z.

theorem Hironaka.Resolution.notContainedInMembers_totalTransform_strictTransform_of_disjoint {X : AlgebraicGeometry.Scheme} (D Z : X.IdealSheafData) [AlgebraicGeometry.IsLocallyNoetherian X] (E : X.DivisorFamily) (hdisj : Disjoint D.support Z.support) (hZ : NotContainedInMembers E Z) : NotContainedInMembers (E.totalTransform D) (Z.strictTransform D)

The last sentence of [Kol07, Definition 24] off the centre: if no member of E contains Z near any of its points and the centre D misses Z, no member of the total transform contains the strict transform of Z near any of its points — the members through a point off the exceptional divisor are the strict transforms of the members below, with the transported stalks.