The strict transform is a blow-up

The strict transform X' of a closed subscheme X ⊆ S under the blow-up of S along Z is the blow-up of X in the closed subscheme f⁻¹Z of X [TSPA, Tag 080E]; [Hau14, Corollary 5.2 (a)]. The Stacks Project proves it by the Proj computation on charts; here it is proved from the universal property alone [Hau14, Definition 4.4], for any pair of blow-ups in the sense of IsBlowUp (Hironaka.Scheme.BlowUp.UniversalProperty), so that no chart of the construction is unfolded. The argument, for π : B ⟶ X a blow-up of X along D, ι : Y ⟶ X the closed subscheme of J, π' : B' ⟶ Y a blow-up of Y along D.comap ι, E := D.comap π the exceptional ideal, Jˢ the strict transform (the E-power torsion saturation of J* = J.comap π):

1. π' ≫ ι is admissible for D (its inverse image of D is the exceptional ideal of B'), so it lifts to φ : B' ⟶ B over X.
2. φ lands in V(Jˢ): J*.comap φ = ⊥ because J.comap ι = ⊥, and the saturation pulls back into the saturation of ⊥ by the invertible exceptional ideal of B' (comap_saturate_le), which is ⊥ (saturate_bot_of_isInvertible). Hence φ = φ' ≫ ιˢ with ιˢ : V(Jˢ) ⟶ B.
3. ιˢ ≫ π factors through ι as g : V(Jˢ) ⟶ Y (J.comap (ιˢ ≫ π) ≤ Jˢ.comap ιˢ = ⊥), and g is admissible for D.comap ι: its inverse image is the restriction E.comap ιˢ of the exceptional ideal to the saturated closed subscheme, which is invertible because a local generator of E stays a nonzerodivisor modulo an E-saturated ideal (isInvertible_comap_subschemeι_of_colon_eq). So g lifts to ψ : V(Jˢ) ⟶ B' over Y.
4. φ' ≫ ψ = 𝟙 by uniqueness of lifts of π' (both are lifts), and ψ ≫ φ' = 𝟙 by uniqueness of lifts of the admissible ιˢ ≫ π into B (ψ ≫ φ and ιˢ both lift it; ιˢ is a monomorphism).

Generic lemmas on ideal sheaves used along the way

• comap_mul, comap_pow: the inverse image ideal sheaf is multiplicative (the affine formula for inverse images on a cover).
• comap_iSup: comap preserves suprema (it is a lower adjoint).
• comap_colon_le, comap_saturate_le: colons and saturations pull back into colons and saturations.
• colon_pow_bot_of_isInvertible, saturate_bot_of_isInvertible: an invertible ideal sheaf has no torsion.
• colon_saturate_of_fg: the saturation is saturated, (I : K^∞) : K = (I : K^∞), for K finitely generated on affine opens (in particular invertible).
• comap_subschemeι_eq_bot: I.comap I.subschemeι = ⊥.
• isInvertible_comap_subschemeι_of_colon_eq: for E invertible and S with (S : E) = S, E.comap S.subschemeι is invertible.

Conventions

IsBlowUp I π is the predicate of Hironaka.Scheme.BlowUp.UniversalProperty: π admissible and every admissible morphism lifts uniquely. Closed subschemes are Mathlib's IdealSheafData.subscheme with subschemeι; factorizations through them are IsClosedImmersion.lift (kernel containment). The strict transform is strictTransformAlong π E J.

The inverse image ideal sheaf and products, colons, saturations

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_affineOpens_le_preimage {X Y : Scheme} (f : Y ⟶ X) (y : ↥Y) : ∃ (U : ↑X.affineOpens) (V : ↑Y.affineOpens), y ∈ ↑V ∧ ↑V ≤ (TopologicalSpace.Opens.map f.base).obj ↑U

Every point of Y has an affine neighbourhood mapping into an affine open of X.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_mul {X Y : Scheme} (I K : X.IdealSheafData) (f : Y ⟶ X) : (I * K).comap f = I.comap f * K.comap f

The inverse image ideal sheaf is multiplicative ([TSPA, Tag 080A]: the ideal of the exceptional divisor of a composite of blow-ups is the product of the two inverse images), by the affine formula ideal_comap_of_le on a cover.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_pow {X Y : Scheme} (K : X.IdealSheafData) (f : Y ⟶ X) (n : ℕ) : (K ^ n).comap f = K.comap f ^ n

The power form: f⁻¹(K^n)·𝒪_Y = (f⁻¹K·𝒪_Y)^n.

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_iSup {X Y : Scheme} {ι : Sort u_1} (I : ι → X.IdealSheafData) (f : Y ⟶ X) : (⨆ (i : ι), I i).comap f = ⨆ (i : ι), (I i).comap f

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_colon_le {X Y : Scheme} (I K : X.IdealSheafData) (f : Y ⟶ X) : (I.colon K).comap f ≤ (I.comap f).colon (K.comap f)

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_saturate_le {X Y : Scheme} (I K : X.IdealSheafData) (f : Y ⟶ X) : (I.saturate K).comap f ≤ (I.comap f).saturate (K.comap f)

theorem AlgebraicGeometry.Scheme.IdealSheafData.colon_pow_bot_of_isInvertible {X : Scheme} {E : X.IdealSheafData} (hE : E.IsInvertible) (i : ℕ) : ⊥.colon (E ^ i) = ⊥

An invertible ideal sheaf has no torsion: (⊥ : E ^ i) = ⊥.

theorem AlgebraicGeometry.Scheme.IdealSheafData.saturate_bot_of_isInvertible {X : Scheme} {E : X.IdealSheafData} (hE : E.IsInvertible) : ⊥.saturate E = ⊥

theorem AlgebraicGeometry.Scheme.IdealSheafData.colon_saturate_of_fg {X : Scheme} (I K : X.IdealSheafData) (hK : ∀ (U : ↑X.affineOpens), (K.ideal U).FG) : (I.saturate K).colon K = I.saturate K

For K finitely generated on every affine open, ((I : K^∞) : K) = (I : K^∞): the saturation is saturated.

Closed subschemes: the kernel of the inclusion and the restriction of an invertible ideal

theorem AlgebraicGeometry.Scheme.IdealSheafData.comap_subschemeι_eq_bot {X : Scheme} (I : X.IdealSheafData) : I.comap I.subschemeι = ⊥

I.comap I.subschemeι = ⊥: the ideal of a closed subscheme pulls back to zero on it.

theorem AlgebraicGeometry.Scheme.IdealSheafData.isInvertible_comap_subschemeι_of_colon_eq {X : Scheme} {E S : X.IdealSheafData} (hE : E.IsInvertible) (hS : S.colon E = S) : (E.comap S.subschemeι).IsInvertible

The restriction of an invertible ideal sheaf E to the closed subscheme of an E-saturated ideal sheaf S ((S : E) = S) is invertible: on an affine open where E = (e) with e a nonzerodivisor, e stays a nonzerodivisor modulo S(U), because u e ∈ S(U) forces u ∈ (S(U) : e) = S(U).

The strict transform is the blow-up of the closed subscheme

theorem AlgebraicGeometry.exists_iso_strictTransform_subscheme {X B B' : Scheme} {D J : X.IdealSheafData} {π : B ⟶ X} {π' : B' ⟶ J.subscheme} (hπ : IsBlowUp D π) (hπ' : IsBlowUp (D.comap J.subschemeι) π') : ∃ (e : B' ≅ (J.strictTransformAlong π (D.comap π)).subscheme), CategoryTheory.CategoryStruct.comp e.hom (CategoryTheory.CategoryStruct.comp (J.strictTransformAlong π (D.comap π)).subschemeι π) = CategoryTheory.CategoryStruct.comp π' J.subschemeι

The strict transform is a blow-up [TSPA, Tag 080E]; [Hau14, Corollary 5.2 (a)]: for any blow-up π : B ⟶ X of X along D and any blow-up π' : B' ⟶ V(J) of the closed subscheme V(J) along D.comap ι (in the sense of IsBlowUp), B' is isomorphic to the strict transform V(Jˢ) ⊆ B, compatibly with the maps to X. Proof by the universal property alone (see the module docstring): the lift φ of π' ≫ ι lands in V(Jˢ); the lift ψ of V(Jˢ) → V(J), admissible because the exceptional ideal restricts to an invertible ideal on the saturated subscheme, is its inverse by uniqueness of lifts.