Blow-ups commute with flat base change

For a flat g : X₁ ⟶ X₂ and a centre I on X₂, the blow-up of X₁ along I·𝒪_{X₁} = I.comap g is the fibre product X₁ ×_{X₂} B_I X₂ [TSPA, Tag 0805]. The restriction of a blow-up to an open subscheme [Hau14, Corollary 5.2 (b)] is the case of an open immersion, the blow-up of a product [Hau14, Corollary 5.2 (e)] the case of a product projection. The flat case along Spec 𝒪_{X,x} ⟶ X gives the local structure of a blow-up at a point (Hironaka.Scheme.Smooth.LocalBlowUp), and along a flat morphism of bases it gives the induced morphism of blow-ups (Hironaka.Scheme.BlowUp.BlowUpMap).

The argument, from the universal property

The Stacks Project proves the lemma by computing the relative Proj: flatness makes g^*Iⁿ → 𝒪_{X₁} injective with image (I·𝒪_{X₁})ⁿ. The proof below reaches the same statement from the same hypotheses through the universal property [Hau14, Definition 4.4] alone, in the manner of Hauser's proof of [Hau14, Proposition 5.1] (the universal property of the blow-up against the universal property of the fibre product), so that it applies to any π with IsBlowUp I π.

Let P := X₁ ×_{X₂} B₂ with projections p₁ : P ⟶ X₁, p₂ : P ⟶ B₂, and write I₁ := I.comap g.

1. P ⟶ X₁ is admissible for I₁. I₁.comap p₁ = I.comap (p₁ ≫ g) = I.comap (p₂ ≫ π₂) = (I.comap π₂).comap p₂; I.comap π₂ is invertible (clause (i) for π₂) and p₂, the base change of the flat g, is flat, and the inverse image of an invertible ideal sheaf along a flat morphism is invertible (IsInvertible.comap_of_flat: a nonzerodivisor stays a nonzerodivisor under a flat ring map, the injectivity that flatness gives in [TSPA, Tag 0805], for n = 1). So p₁ lifts to τ : P ⟶ B₁ with τ ≫ π₁ = p₁.
2. π₁ ≫ g is admissible for I (I.comap (π₁ ≫ g) = I₁.comap π₁, clause (i) for π₁), so it lifts to φ : B₁ ⟶ B₂ with φ ≫ π₂ = π₁ ≫ g; this is the morphism of the square, and σ := (π₁, φ) : B₁ ⟶ P is the canonical comparison map.
3. σ and τ are inverse. σ ≫ τ and 𝟙 B₁ are two lifts of π₁ along π₁, which is admissible for I₁, so they agree (clause (ii)). τ ≫ φ and p₂ are two lifts along π₂ of the admissible p₁ ≫ g = p₂ ≫ π₂, so they agree; hence τ ≫ σ agrees with 𝟙 P on both projections. Therefore B₁ ≅ P over the two projections: the square is cartesian.

Nothing about B₁, B₂ beyond the two clauses is used; no Noetherian, separatedness or finiteness hypothesis enters ([TSPA, Tag 0805] has none).

Main declarations

• IdealSheafData.IsInvertible.comap_of_flat: the inverse image of an invertible ideal sheaf along a flat morphism is invertible.
• IsBlowUp.exists_isPullback_of_flat, IsBlowUp.exists_isPullback_of_etale, IsBlowUp.exists_isPullback_prod (with the pasted square B_{Z × a}(Z ×_S Y) = Z ×_S B_a Y).
• exists_restrictIso_of_isPullback: the pullback square of a blow-up along an open U ⊆ X read as Hauser prints it, an isomorphism B_{I|_U} U ≅ π⁻¹(U) carrying π_U to the restriction π ∣_ U — both are pullbacks of the same cospan.

Every morphism to Spec k, k a field, is flat (flat_of_field, in Hironaka/Scheme/Smooth/ExceptionalBaseChange.lean), which makes Hauser's product formula over a field an instance of flat base change.

theorem AlgebraicGeometry.Scheme.IdealSheafData.IsInvertible.comap_of_flat {X Y : Scheme} (f : Y ⟶ X) [Flat f] {J : X.IdealSheafData} (hJ : J.IsInvertible) : (J.comap f).IsInvertible

The inverse image of an invertible ideal sheaf along a flat morphism is invertible (flatness of g makes g^*𝓘ⁿ → 𝒪 injective [TSPA, Tag 0805], here for n = 1). On an affine open V ⊆ f⁻¹(U) with J(U) = (a), (J.comap f)(V) = (f♯a) (ideal_comap_of_le) and f♯a is a nonzerodivisor because f♯ : Γ(U) → Γ(V) is flat and multiplication by a is injective.

theorem AlgebraicGeometry.exists_restrictIso_of_isPullback {X B B' : Scheme} {π : B ⟶ X} (U : X.Opens) {π' : B' ⟶ ↑U} {φ : B' ⟶ B} (H : CategoryTheory.IsPullback φ π' π U.ι) : ∃ (e : B' ≅ ↑((TopologicalSpace.Opens.map π.base).obj U)), CategoryTheory.CategoryStruct.comp e.hom (π ∣_ U) = π'

The blow-up of an open U along U ∩ Z is the restriction of π to π⁻¹(U) [Hau14, Corollary 5.2 (b)]: a pullback square B' → B over U.ι : U → X gives an isomorphism B' ≅ π⁻¹(U) carrying π' : B' ⟶ U to Mathlib's restriction π ∣_ U, because π⁻¹(U) with π ∣_ U is a pullback of the same cospan (isPullback_morphismRestrict).

theorem AlgebraicGeometry.IsBlowUp.exists_isPullback_of_flat {X₁ X₂ B₁ B₂ : Scheme} {I : X₂.IdealSheafData} (g : X₁ ⟶ X₂) [Flat g] {π₂ : B₂ ⟶ X₂} (h₂ : IsBlowUp I π₂) {π₁ : B₁ ⟶ X₁} (h₁ : IsBlowUp (I.comap g) π₁) : ∃ (φ : B₁ ⟶ B₂), CategoryTheory.IsPullback φ π₁ π₂ g

Blowing up commutes with flat base change [TSPA, Tag 0805], proved from the universal property as described in the module docstring: for g : X₁ ⟶ X₂ flat and blow-ups π₂ : B₂ ⟶ X₂ along I and π₁ : B₁ ⟶ X₁ along I.comap g in the sense of IsBlowUp, there is φ : B₁ ⟶ B₂ over g with B₁ = X₁ ×_{X₂} B₂.

theorem AlgebraicGeometry.IsBlowUp.exists_isPullback_of_etale {X₁ X₂ B₁ B₂ : Scheme} {I : X₂.IdealSheafData} (g : X₁ ⟶ X₂) [Etale g] {π₂ : B₂ ⟶ X₂} (h₂ : IsBlowUp I π₂) {π₁ : B₁ ⟶ X₁} (h₁ : IsBlowUp (I.comap g) π₁) : ∃ (φ : B₁ ⟶ B₂), CategoryTheory.IsPullback φ π₁ π₂ g

The base-change square for an étale g [TSPA, Tag 0805] (étale morphisms are flat, Mathlib's Etale → Smooth → Flat).

theorem AlgebraicGeometry.IsBlowUp.exists_isPullback_prod {S Z Y BY B' : Scheme} (fZ : Z ⟶ S) [Flat fZ] (fY : Y ⟶ S) {a : Y.IdealSheafData} {πY : BY ⟶ Y} (hY : IsBlowUp a πY) {π' : B' ⟶ CategoryTheory.Limits.pullback fZ fY} (h' : IsBlowUp (a.comap (CategoryTheory.Limits.pullback.snd fZ fY)) π') : ∃ (φ : B' ⟶ BY), CategoryTheory.IsPullback φ π' πY (CategoryTheory.Limits.pullback.snd fZ fY) ∧ CategoryTheory.IsPullback (CategoryTheory.CategoryStruct.comp π' (CategoryTheory.Limits.pullback.fst fZ fY)) φ fZ (CategoryTheory.CategoryStruct.comp πY fY)

The blow-up of a product [Hau14, Corollary 5.2 (e)], over any base S with Z ⟶ S flat (Hauser's case is S = Spec k, where every morphism is flat): the blow-up of Z ×_S Y along Z × a = a.comap pr₂ is the flat base change of B_a Y ⟶ Y along the projection pr₂, and, pasting with the product square, it is Z ×_S B_a Y: B' = Z ×_S B_a Y over Z ⟶ S ⟵ B_a Y ⟶ Y ⟶ S.