A composite of two blow-ups is a single blow-up: the descended centre

A morphism obtained by a finite succession of monoidal transformations is a single monoidal transformation with a suitably chosen centre [Hir64, Ch. 0, §3, pp. 132–133]; [TSPA, Tag 080B]: for b = IdealSheafData.blowUpπ I : X' ⟶ X and an ideal sheaf J' on X', the blow-up of X' along J' followed by b is the blow-up of X along the single centre I * K_m, where K_m is Hironaka's J(m),

descendCenter I J' m := I ^ m ⊓ (J' * E ^ m).map b,

the ideal sheaf of the functions x ∈ I^m whose pullback b^*x lies in J'·E^m (E the exceptional ideal). Hironaka's J(m) is a coherent ideal sheaf with f₀⁻¹(J(m)) = f₀⁻¹(J₀)^m J₁ for m large, and the single centre D' is defined by J(m) J₀. This module holds the definition and the generic parts of the argument; Hironaka.Scheme.BlowUp.Composite.Main proves K_m.comap b = J' * E^m for m large and Hironaka.Scheme.BlowUp.Composite.Iso assembles the isomorphism of blow-ups.

• blowUp.exists_mul_isInvertible_iso (the trivial factor): blowing up J * L with L invertible is blowing up J — the blow-up of a product centre (Hironaka.Scheme.BlowUp.Glue.Product) with the second blow-up trivial.
• descendCenter, descendCenter_le_pow, comap_descendCenter_le (the easy half): K_m ≤ I^m and K_m.comap b ≤ J' * E^m, the Galois connection map ⊣ comap.
• mem_ideal_map_iff_of_le_iSup (the pushforward criterion): for a quasi-compact f : X ⟶ Y, an affine open U of Y and affine opens V i ⊆ f⁻¹U covering f⁻¹U, x ∈ (L.map f).ideal U iff each f.appLE U (V i) x ∈ L.ideal (V i) — Mathlib's Hom.ker_apply for the kernel of V(L) → Y, ker_subschemeι_app on the affine pieces, and the sheaf condition of V(L).
• support_mul_descendCenter: the support of I * K_m is |Z| ∪ b(|Z'|) once K_m.comap b = J' * E^m.
• blowUp.isLocallyNoetherian, blowUp.isNoetherian: the blow-up of a (locally) Noetherian scheme is (locally) Noetherian, through the Noetherianity of the chart rings R[I/a].

The definition and these lemmas are also imported by the sequence modules (Hironaka.Scheme.BlowUpSequence.Triple, Hironaka.Resolution.Algebraic.Snc.DictionaryBoundary, Hironaka.Scheme.BlowUpSequence.StrictTransformIntegral) and by the worked examples.

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.exists_mul_isInvertible_iso {Y : Scheme} (J L : Y.IdealSheafData) (hL : L.IsInvertible) : ∃ (e : (J * L).blowUp ≅ J.blowUp), CategoryTheory.CategoryStruct.comp e.hom J.blowUpπ = (J * L).blowUpπ ∧ ∀ (ψ : (J * L).blowUp ⟶ J.blowUp), CategoryTheory.CategoryStruct.comp ψ J.blowUpπ = (J * L).blowUpπ → ψ = e.hom

The trivial factor ([TSPA, Tag 080B]: a power of the exceptional ideal cuts out an effective Cartier divisor, and blowing up an effective Cartier divisor changes nothing): blowing up J * L with L invertible is blowing up J, canonically over Y. The blow-up of J * L is the blow-up of B_J Y along L.comap (IdealSheafData.blowUpπ J) (blowUp.exists_mulIso), which is invertible (blowUp.isInvertible_comap_of_isInvertible), so that second blow-up map is an isomorphism (blowUp.isIso_π_of_isInvertible).

theorem AlgebraicGeometry.mem_ideal_map_iff_of_le_iSup {X Y : Scheme} (f : X ⟶ Y) [QuasiCompact f] (L : X.IdealSheafData) {ι : Type u_1} (U : ↑Y.affineOpens) (V : ι → ↑X.affineOpens) (hV : ∀ (i : ι), ↑(V i) ≤ (TopologicalSpace.Opens.map f.base).obj ↑U) (hcov : (TopologicalSpace.Opens.map f.base).obj ↑U ≤ ⨆ (i : ι), ↑(V i)) (x : ↑(Y.presheaf.obj (Opposite.op ↑U))) : x ∈ (L.map f).ideal U ↔ ∀ (i : ι), (CategoryTheory.ConcreteCategory.hom (Scheme.Hom.appLE f ↑U ↑(V i) ⋯)) x ∈ L.ideal (V i)

The pushforward criterion: for f quasi-compact, U an affine open of Y and affine opens V i ⊆ f⁻¹U covering f⁻¹U, a function x on U lies in the pushforward L.map f iff its pullback to every V i lies in L. (L.map f is the kernel of V(L) → Y; on the affine pieces that kernel is L, and a section of 𝒪_{V(L)} vanishing on a cover vanishes.)

noncomputable def AlgebraicGeometry.descendCenter {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (m : ℕ) : X.IdealSheafData

Hironaka's descended centre J(m) [Hir64, Ch. 0, §3, p. 133] in intrinsic form: the functions of I^m whose pullback along the blow-up map lies in J' · E^m, E the exceptional ideal. On the chart of a ∈ I(U) the exceptional ideal is (a) with a a nonzerodivisor (affineBlowUp.comap_exceptionalIdeal_chart), so b^*x ∈ J'·(a^m) iff x/a^m ∈ J' there: K_m = {x ∈ I^m : x/a^m ∈ J'_a on every chart}.

Equations

• AlgebraicGeometry.descendCenter I J' m = I ^ m ⊓ (J' * I.exceptionalDivisor ^ m).map I.blowUpπ

theorem AlgebraicGeometry.descendCenter_le_pow {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (m : ℕ) : descendCenter I J' m ≤ I ^ m

K_m ≤ I^m.

theorem AlgebraicGeometry.comap_descendCenter_le {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (m : ℕ) : (descendCenter I J' m).comap I.blowUpπ ≤ J' * I.exceptionalDivisor ^ m

The easy half of K_m.comap b = J' * E^m: K_m.comap b ≤ J' * E^m (the Galois connection map ⊣ comap).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.existsUnique_preimage_of_notMem_support {X : Scheme} (I : X.IdealSheafData) {x : ↥X} (hx : x ∉ I.support) : ∃! x' : ↥I.blowUp, I.blowUpπ x' = x

Off the centre the blow-up map is a bijection on points (it is an isomorphism over the complement of the centre, Hironaka.Scheme.BlowUp.Glue.Trivial): every x ∉ V(I) has exactly one preimage.

theorem AlgebraicGeometry.support_mul_descendCenter {X : Scheme} (I : X.IdealSheafData) (J' : I.blowUp.IdealSheafData) (m : ℕ) (hm : (descendCenter I J' m).comap I.blowUpπ = J' * I.exceptionalDivisor ^ m) : ↑(I * descendCenter I J' m).support = ↑I.support ∪ ⇑I.blowUpπ '' ↑J'.support

The support of the descended centre [TSPA, Tag 080B]: if K_m.comap b = J' * E^m, the support of I * K_m is |Z| ∪ b(|Z'|) set-theoretically. V(I K_m) = V(I) ∪ V(K_m); b⁻¹V(K_m) = V(J') ∪ V(E^m) with V(E^m) ⊆ b⁻¹V(I); off Z every point has a unique preimage, so x ∉ Z lies in V(K_m) iff its preimage lies in Z'.

theorem AlgebraicGeometry.affineBlowUpAlgebra_span_eq_adjoin {R : Type u} [CommRing R] (s : Set R) (a : R) : affineBlowUpAlgebra (Ideal.span s) a = Algebra.adjoin R ((fun (x : R) => Localization.mk x ⟨a, ⋯⟩) '' s)

The affine blow-up algebra of span s is generated by the fractions x/a, x ∈ s: a fraction y/a with y = Σ rᵢ xᵢ is Σ rᵢ (xᵢ/a).

theorem AlgebraicGeometry.affineBlowUpAlgebra_fg {R : Type u} [CommRing R] {I : Ideal R} (hI : I.FG) (a : R) : (affineBlowUpAlgebra I a).FG

The affine blow-up algebra of a finitely generated ideal is a finitely generated algebra.

theorem AlgebraicGeometry.isNoetherianRing_affineBlowUpAlgebra {R : Type u} [CommRing R] [IsNoetherianRing R] (I : Ideal R) (a : R) : IsNoetherianRing ↥(affineBlowUpAlgebra I a)

Over a Noetherian ring the chart rings R[I/a] are Noetherian (Hilbert's basis theorem for the finitely generated algebra R[I/a]).

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isLocallyNoetherian {X : Scheme} (I : X.IdealSheafData) [IsLocallyNoetherian X] : IsLocallyNoetherian I.blowUp

The blow-up of a locally Noetherian scheme is locally Noetherian: its charts are the spectra of the Noetherian rings Γ(X, U)[I(U)/a].

theorem AlgebraicGeometry.Scheme.IdealSheafData.blowUp.isNoetherian {X : Scheme} (I : X.IdealSheafData) [IsNoetherian X] : IsNoetherian I.blowUp

The blow-up of a Noetherian scheme is Noetherian (locally Noetherian, and quasi-compact as the source of the proper map π to a quasi-compact scheme).