The birational transform of a smooth hypersurface through the centre

Kollár's proof of [Kol07, Theorem 80 (1)] passes from 𝒪_{X_i}(−H_i) ⊂ J_i to 𝒪_{X_{i+1}}(−H_{i+1}) ⊂ J_{i+1} in one clause ("since … H_0 is smooth, we see that …"). The step it hides is [Wlo05, Lemma 2.7.4 (2)–(3)]: if the smooth centre Z lies in the smooth hypersurface H = (u = 0), then in a chart with exceptional coordinate y the function u' = u/y is again a parameter, V(u') is the strict transform of H, and u' is the controlled transform of u with control 1. Coordinate-free:

• the exceptional multiplicity of π^* H is one at every point of the exceptional divisor (stalkIdeal_comap_not_le_exceptionalDivisor_sq; the multiplicity of [Kol07, 58.1] pointwise): at a point q of B_Z X over z ∈ Z, the chart bridge (exists_stalk_equiv_localization_chart_of_smooth) identifies 𝒪_{B,q} with a localization of the chart ring 𝒪_{X,z}[y_i/y_ρ] at a prime 𝔮 over 𝔪_z, the exceptional divisor becoming (y_ρ); the equation h of H has order one and lies in the centre, so h = y_ρ · h' with h' its controlled transform, and h' cannot lie in (y_ρ) there: modulo 𝔪_z the chart ring is the polynomial ring κ(z)[Y] (exists_quotient_map_maximalIdeal_ringEquiv), in which h' is the leading form of h, a nonzero polynomial (exists_transformElem_eq_chartPresentation), while (y_ρ) maps to zero. This is the argument of the local form of [Kol07, Lemma 61] (ordElem_algebraMap_transformElem_le) with the inequality replaced by a non-membership.
• the strict transform of H is the marked transform (π)⁻¹_*(𝒪(−H), 1) (strictTransform_eq_markedTransform_one): the strict transform is the saturation of π^* H by the exceptional divisor F, the marked transform ([Kol07, 60.1]) its colon by F; stalkwise π^* H = (y u') with y the equation of F, prime because F is a smooth divisor of B_Z X (isSmoothDivisor_exceptionalDivisor_of_smooth), and u' ∉ (y) by the previous point, so every colon (y u' : y^i) is contained in (y u' : y) (colon_pow_le_colon_of_prime).
• the strict transform of H is again a smooth hypersurface (isSmoothDivisor_strictTransform_of_le): the morphism of blow-ups blowUpMap H.subschemeι Z : B_{Z ∩ H} H ⟶ B_Z X is a closed immersion with kernel the strict transform of H (the restriction of [Kol07, Definition 30.2]), so V(H_1) ≅ B_{Z ∩ H} H; the centre Z ∩ H is Z itself (Z ⊆ H), smooth; H is smooth of relative dimension n − 1, so B_Z H is smooth of relative dimension n − 1 inside B_Z X, smooth of relative dimension n, which is what "smooth divisor" means. The route avoids adapted coordinates for the flag Z ⊆ H. The degenerate relative dimension n = 0 (an étale X) has no smooth hypersurface but ⊤: at a point of V(H) a generator in 𝔪 ∖ 𝔪² would need 𝔪 ≠ 0, while the stalk of an étale scheme over a field has Krull dimension 0 and is a field; the strict transform of ⊤ is ⊤, a smooth divisor.

When Z is a component of H (a codimension-one centre; the blow-up is an isomorphism, [Kol07, Warning 20]) the statements hold as well: the transform drops that component, on both sides.

These results carry the hypersurface of maximal contact along a blow-up sequence (Hironaka/Resolution/Algebraic/MaximalContact/Sequence.lean) and are used again in the globalization (Hironaka/Resolution/Algebraic/Kol07/MaximalContactGlobalization.lean), in the embedded resolution (Hironaka/Resolution/) and in boundary clearing (Hironaka/Resolution/Algebraic/BoundaryClearing/Restriction.lean).

theorem Hironaka.Local.algebraMap_transformElem_notMem_map_span_x {R : Type u_1} [CommRing R] [IsRegularLocalRing R] {n : ℕ} (x : Fin n → R) (hx : IsLocalRing.maximalIdeal R = Ideal.span (Set.range x)) (hn : ↑n = ringKrullDim R) (r : Fin n) (𝔮 : Ideal ↥(IsLocalRing.chartRing x r)) [𝔮.IsPrime] (h𝔮 : IsLocalRing.maximalIdeal R ≤ Ideal.comap (algebraMap R ↥(IsLocalRing.chartRing x r)) 𝔮) {m : ℕ} {f : R} (hf : f ∈ IsLocalRing.chartCenter x r ^ m) (hord : IsLocalRing.ordElem f = ↑m) : (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime 𝔮)) (IsLocalRing.transformElem x r f hf) ∉ Ideal.map (algebraMap (↥(IsLocalRing.chartRing x r)) (Localization.AtPrime 𝔮)) (Ideal.span {(algebraMap R ↥(IsLocalRing.chartRing x r)) (x r)})

The multiplicity of [Kol07, 58.1] at a point of the exceptional divisor of the chart: for f ∈ P^m of order exactly m, the controlled transform f / x_r^m does not lie in the exceptional ideal (x_r) at any prime 𝔮 of the chart ring over 𝔪: modulo 𝔪 R' the chart ring is κ[Y], in which f / x_r^m is the nonzero leading form of f while x_r vanishes; the argument of ordElem_algebraMap_transformElem_le.

theorem Hironaka.Local.colon_pow_le_colon_of_prime {S : Type u_1} [CommRing S] {y u' : S} (hy : y ∈ nonZeroDivisors S) (hprime : Prime y) (hu' : ¬y ∣ u') (i : ℕ) : Submodule.colon (Ideal.span {u' * y}) ↑(Ideal.span {y} ^ i) ≤ Submodule.colon (Ideal.span {u' * y}) ↑(Ideal.span {y})

In a commutative ring, for a prime nonzerodivisor y and u' not divisible by y, every colon (u' y : y^i) lies in (u' y : y): the saturation of the principal ideal (u' y) by (y) stabilizes at the first step.

theorem AlgebraicGeometry.IsSmoothDivisor.ord_eq_one {X : Scheme} {H : X.IdealSheafData} (hH : IsSmoothDivisor H) {x : ↥X} (hx : x ∈ H.support) : H.ord x = 1

A smooth hypersurface has order exactly one at every point of its support: its stalk there is generated by an element of 𝔪 ∖ 𝔪² (ordElem_eq_one_iff).

theorem AlgebraicGeometry.IsSmoothDivisor.ordAlongEq_one_of_le {X : Scheme} {H Z : X.IdealSheafData} (hH : IsSmoothDivisor H) (hZH : H ≤ Z) : H.OrdAlongEq Z.support ↑1

A smooth hypersurface containing the centre Z (H ≤ Z as ideal sheaves) has order exactly 1 along Z: at every generic point of Z, which lies on H.

theorem Hironaka.Snc.isSmoothDivisor_top {X : AlgebraicGeometry.Scheme} : AlgebraicGeometry.IsSmoothDivisor ⊤

The unit ideal sheaf is a smooth divisor (the empty hypersurface): its closed subscheme has no points.

theorem AlgebraicGeometry.IsSmoothDivisor.locally_principal {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] {H : X.IdealSheafData} (hH : IsSmoothDivisor H) (x : ↥X) : ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (s : ↑(X.presheaf.obj (Opposite.op ↑U))), H.ideal U = Ideal.span {s}

The ideal sheaf of a smooth hypersurface is locally principal: on an affine neighbourhood of every point it is generated by one section (at a point of V(H) the stalk generator spreads to a basic open, exists_basicOpen_ideal_eq_span; off V(H) the ideal is the unit ideal).

theorem AlgebraicGeometry.IsSmoothDivisor.eq_top_of_smoothOfRelativeDimension_zero {X : Scheme} {k : Type u} [Field k] (f : X ⟶ Spec ↧k) [CharZero k] [SmoothOfRelativeDimension 0 f] {H : X.IdealSheafData} (hH : IsSmoothDivisor H) : H = ⊤

In relative dimension 0 (an étale X) the only smooth hypersurface is the empty one: at a point of V(H) a generator in 𝔪 ∖ 𝔪² would need 𝔪 ≠ 0, but the stalk has Krull dimension 0 and is a field.

theorem Hironaka.Sequence.isSmoothDivisor_exceptionalDivisor_of_smooth {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) [CharZero k] (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] : AlgebraicGeometry.IsSmoothDivisor Z.exceptionalDivisor

The exceptional divisor of the blow-up of a smooth scheme along a smooth centre of any shape is a smooth divisor of the blow-up (isSmoothDivisor_totalTransformFamily for the empty divisor family).

theorem Hironaka.Sequence.stalkIdeal_comap_not_le_exceptionalDivisor_sq {k : Type u} [Field k] {X : AlgebraicGeometry.Scheme} (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)] {H : X.IdealSheafData} (hH : AlgebraicGeometry.IsSmoothDivisor H) (hZH : H ≤ Z) (q : ↥Z.blowUp) (hq : Z.blowUpπ q ∈ Z.support) : ¬(H.comap Z.blowUpπ).stalkIdeal q ≤ Z.exceptionalDivisor.stalkIdeal q ^ 2

The multiplicity of [Kol07, 58.1] at every point of the exceptional divisor: for a smooth hypersurface H containing the smooth centre Z, the pull-back π^* H is not contained in F² at any point q of B_Z X over the centre; the exceptional multiplicity of π^* H is exactly one. Through the chart bridge at q (exists_stalk_equiv_localization_chart_of_smooth), this is algebraMap_transformElem_notMem_map_span_x for the equation h of H at π q, which has order one and lies in the centre.

theorem AlgebraicGeometry.Scheme.IdealSheafData.strictTransform_eq_markedTransform_one {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) (hZ : Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)) (H : X.IdealSheafData) (hH : IsSmoothDivisor H) (hZH : H ≤ Z) : H.strictTransform Z = H.markedTransform Z 1

[Wlo05, Lemma 2.7.4 (3)], the step hidden in the proof of [Kol07, Theorem 80 (1)]: for a smooth centre Z contained in a smooth hypersurface H, the strict transform of H under the blow-up of Z is the marked transform (π)⁻¹_*(𝒪(−H), 1): stalkwise π^* H = (u' y) with y the (prime) equation of the exceptional divisor and u' ∉ (y) (stalkIdeal_comap_not_le_exceptionalDivisor_sq), so the saturation by (y) is the colon by (y) (colon_pow_le_colon_of_prime).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isSmoothDivisor_strictTransform_of_le {k : Type u} [Field k] {X : Scheme} (f : X ⟶ Spec ↧k) [CharZero k] (n : ℕ) [SmoothOfRelativeDimension n f] (Z : X.IdealSheafData) (hZ : Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι f)) (H : X.IdealSheafData) (hH : IsSmoothDivisor H) (hZH : H ≤ Z) : IsSmoothDivisor (H.strictTransform Z)

[Wlo05, Lemma 2.7.4 (2)], "u' = u/y is a parameter": the strict transform of a smooth hypersurface containing the smooth centre is a smooth hypersurface of B_Z X: V(H_1) ≅ B_Z H through the closed immersion blowUpMap H.subschemeι Z, smooth of relative dimension n − 1.