Blow-up calculus for the single-centre form of Main Theorem I

Hironaka's Main Theorem I asks for a single monoidal transformation resolving X with centre exactly the singular locus; his strong form obtains the resolving morphism as a finite succession of monoidal transformations, and he remarks that a finite succession of monoidal transformations can be replaced by a single monoidal transformation with a suitably chosen centre [Hir64, pp. 132–133]. This file proves two general facts of the blow-up calculus used to make that remark precise (Hironaka.Resolution.Algebraic.Hir64.SingleCenter):

• isIntegral_last_of_forall_support_ne_top: a finite succession of monoidal transformations with proper centres starting at an integral locally Noetherian scheme ends at an integral scheme (the blow-up of an integral scheme in a proper centre is integral [TSPA, Tag 0BFL], iterated). Every stage X_i is read as the closed subscheme V(⊥) of itself: the strict transform of ⊥ along a blow-up is ⊥ (the saturation of ⊥ by the invertible exceptional ideal is ⊥), so strictTransformSeq ⊥ i = ⊥ at every stage and AlgebraicGeometry.isIntegral_strictTransformSeq (the strict transform of an integral closed subscheme contained in no centre stays integral) applies with J = ⊥; "no centre is a whole stage" is exactly "no centre contains V(⊥)", and V(⊥) ≅ X_i transports integrality.
• exists_iso_blowUp_mul_of_isInvertible_comap: blowing up K * J is blowing up K when the pullback of J to blowUp K is invertible, because blowUp (K * J) ≅ blowUp_{blowUp K} (J·𝒪) over the base [TSPA, Tag 080A] and the blow-up of an invertible ideal is an isomorphism [TSPA, Tag 0807]. This is Hironaka's centre J(m)·J₀ for two successive monoidal transformations [Hir64, p. 133].

The file also records that a point off a closed set over which all centres lie has a point of every stage above it, that the generic point of an integral scheme is regular, and that if every centre lies over the singular locus of a reduced irreducible scheme, no centre is a whole stage.

theorem Hironaka.Resolution.strictTransform_bot {Y : AlgebraicGeometry.Scheme} (D : Y.IdealSheafData) : ⊥.strictTransform D = ⊥

The strict transform of the zero ideal (the whole scheme as a closed subscheme) along a blow-up is the zero ideal: (⊥.comap π).saturate E = ⊥.saturate E = ⊥ for the invertible exceptional ideal E (saturate_bot_of_isInvertible).

theorem Hironaka.Resolution.strictTransformSeq_bot {Y : AlgebraicGeometry.Scheme} (S : Y.BlowUpSequence) (i : Fin (S.length + 1)) : S.strictTransformSeq ⊥ i = ⊥

Along a finite succession the strict transform of ⊥ stays ⊥ at every stage.

theorem Hironaka.Resolution.isIntegral_last_of_forall_support_ne_top {Y : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral Y] [AlgebraicGeometry.IsLocallyNoetherian Y] (S : Y.BlowUpSequence) (h : ∀ (i : Fin S.length), (S.center i).support ≠ ⊤) : AlgebraicGeometry.IsIntegral S.last

A finite succession of monoidal transformations with proper centres (no centre a whole stage) starting at an integral locally Noetherian scheme ends at an integral scheme ([TSPA, Tag 0BFL] iterated): the strict transform of the integral closed subscheme V(⊥) = Y along the succession (AlgebraicGeometry.isIntegral_strictTransformSeq), read back on the stage through V(⊥) ≅ X_i.

theorem Hironaka.Resolution.exists_iso_blowUp_mul_of_isInvertible_comap {Y : AlgebraicGeometry.Scheme} (K J : Y.IdealSheafData) (h : (J.comap K.blowUpπ).IsInvertible) : ∃ (e : (K * J).blowUp ≅ K.blowUp), CategoryTheory.CategoryStruct.comp e.hom K.blowUpπ = (K * J).blowUpπ

If the pullback of J to K.blowUp is invertible, then (K * J).blowUp ≅ K.blowUp over Y: the blow-up of a product is the blow-up of the pullback of the second factor on the blow-up of the first [TSPA, Tag 080A], and the blow-up of an invertible ideal is an isomorphism [TSPA, Tag 0807]. This is Hironaka's remark that two successive monoidal transformations are one monoidal transformation with centre J(m)·J₀ [Hir64, p. 133].

theorem Hironaka.Resolution.exists_stage_point_over_of_forall_center_mem {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (Z : Set ↥X) : (∀ (i : Fin S.length), ∀ z ∈ (S.center i).support, (S.stageMap i.castSucc) z ∈ Z) → ∀ x ∉ Z, ∀ (i : Fin (S.length + 1)), ∃ (z : ↥(S.stage i)), (S.stageMap i) z = x

A point x of X not in a set Z over which all the centres of S lie has a point of every stage above it: at each blow-up a point off the centre has exactly one preimage (blowUp.existsUnique_preimage_of_notMem_support).

theorem Hironaka.Resolution.isRegularAt_genericPoint_of_isIntegral {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsIntegral X] : X.IsRegularAt (genericPoint ↥X)

The generic point of an integral scheme is a regular point: its stalk is the function field, a field, and a field is a regular local ring (a local principal ideal domain).

theorem Hironaka.Resolution.support_center_ne_top_of_forall_mem_singularLocus (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsReduced X] [IrreducibleSpace ↥X] (S : X.BlowUpSequence) (hcenters : ∀ (i : Fin S.length), ∀ z ∈ (S.center i).support, (S.stageMap i.castSucc) z ∈ X.singularLocus) (i : Fin S.length) : (S.center i).support ≠ ⊤

If every centre lies over the singular locus of the reduced irreducible X, no centre is a whole stage: the generic point of X is regular and has a point of every stage above it.