The total transform under a trivial blow-up

[Kol07, Definition 65]: "If π is a trivial blow-up, then π⁻¹_{tot}(E) = E + Z"; [Kol07, Warning 20 (2)]: its exceptional divisor is F = Z. A trivial blow-up has an invertible centre Z (a Cartier divisor) and π : B_Z X ⟶ X is an isomorphism (the universal property of the blow-up applied to the identity), so the strict transform of a component D of E is the inverse image along π of the saturation D.saturate Z computed on X (strictTransformAlong_of_isIso), and everything reduces to stalks.

Why the lemmas hold. At a point x ∈ Z the snc data ([Kol07, Definition 24 (4)]) give a regular system of parameters z of 𝒪_{X,x} with Z_x = (z_l : l ∈ s) and, for a component D through x, D_x = (z_c). Since Z_x is principal, generated by a nonzerodivisor, s is a single index {j}: two distinct parameters z_j, z_{j'} cannot both be multiples of one generator g ∈ 𝔪 — if z_j = g b with b a unit then z_{j'} ∈ (z_j), and if b ∈ 𝔪 then z_j ∈ 𝔪², both impossible for a regular system of parameters (exists_eq_singleton_of_span_image_eq_span_singleton). If c ≠ j the ideal (z_c) is prime (the quotient is regular, hence a domain) and z_j ∉ (z_c), so (z_c) : (z_j)^i = (z_c): the component is unchanged by the saturation. If c = j then D_x = Z_x and (z_j) : (z_j) = (1): the component dies near x. On its support the saturation therefore has the stalks of D (stalkIdeal_saturate_eq_of_mem_support), so its subscheme is regular when V(D) is (isRegular_subscheme_saturate), and for a component transversal to Z at every point the saturation is D itself (saturate_eq_self_of_snc_transversal).

The assembly into Kollár's conditions (1)–(3) for DivisorFamily.totalTransform is Hironaka.Scheme.Snc.TrivialSncData and totalTransform_isSnc_of_isInvertible of Hironaka.Scheme.Snc.TotalTransformSmoothBlowUp; as in Hironaka.Scheme.Snc.Family the snc data are explicit hypotheses here.

Main declarations

• Ideal.colon_pow_eq_self_of_isPrime — (p : J^i) = p for a prime p and J ⊄ p.
• AlgebraicGeometry.isPrime_span_singleton_of_parameters, colon_pow_span_image_eq_of_notMem, exists_eq_singleton_of_span_image_eq_span_singleton — the algebra in a regular local ring.
• AlgebraicGeometry.saturate_eq_self_of_forall_stalk, stalkIdeal_saturate_eq_of_mem_support, saturate_eq_self_of_snc_transversal, isRegular_subscheme_saturate, strictTransformAlong_eq_comap_of_saturate_eq — the sheaf-level statements.

theorem Ideal.colon_coe_self {R : Type u_1} [CommRing R] (I : Ideal R) : Submodule.colon I ↑I = ⊤

(I : I) = ⊤ for an ideal I of a commutative ring.

theorem Ideal.colon_pow_eq_self_of_isPrime {R : Type u_1} [CommRing R] {p J : Ideal R} (hp : p.IsPrime) (hJ : ¬J ≤ p) (i : ℕ) : Submodule.colon p ↑(J ^ i) = p

In any commutative ring, a prime ideal is unchanged by the colon with a power of an ideal not contained in it.

Algebra in a regular local ring

theorem AlgebraicGeometry.isPrime_span_singleton_of_parameters {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) (c : Fin n) : (Ideal.span {z c}).IsPrime

A single member of a regular system of parameters generates a prime ideal (the quotient is a regular local ring, hence a domain; isRegularLocalRing_quotient_span_image_finset of Hironaka.Scheme.Snc.ParameterSubset).

theorem AlgebraicGeometry.colon_pow_span_image_eq_of_notMem {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {s : Finset (Fin n)} (hs : s.Nonempty) {c : Fin n} (hc : c ∉ s) (i : ℕ) : Submodule.colon (Ideal.span {z c}) ↑(Ideal.span (z '' ↑s) ^ i) = Ideal.span {z c}

(z_c) : (z_l : l ∈ s)^i = (z_c) for c ∉ s and s nonempty.

theorem AlgebraicGeometry.exists_eq_singleton_of_span_image_eq_span_singleton {R : Type u} [CommRing R] [IsRegularLocalRing R] {n : ℕ} {z : Fin n → R} (hz : IsLocalRing.maximalIdeal R = Ideal.span (Set.range z)) (hn : ↑n = ringKrullDim R) {s : Finset (Fin n)} {g : R} (hg : g ∈ nonZeroDivisors R) (h : Ideal.span (z '' ↑s) = Ideal.span {g}) : ∃ (j : Fin n), s = {j}

If the ideal (z_l : l ∈ s) of a subset of the parameters is principal, generated by a nonzerodivisor, then s is a single index: two parameters cannot both be multiples of one generator g ∈ 𝔪 (a unit multiplier puts one in the ideal of the other, a non-unit multiplier puts one in 𝔪²), and s = ∅ would make g = 0.

The saturation along the centre of a trivial blow-up

theorem AlgebraicGeometry.saturate_eq_self_of_forall_stalk {X : Scheme} (D Z : X.IdealSheafData) (hZ : Z.IsInvertible) (h : ∀ x ∈ D.support, x ∈ Z.support → ∀ (i : ℕ), Submodule.colon (D.stalkIdeal x) ↑(Z.stalkIdeal x ^ i) ≤ D.stalkIdeal x) : D.saturate Z = D

If at every point of D ∩ Z the colon of the stalks is contained in the stalk of D, the saturation of D along the invertible Z is D.

def AlgebraicGeometry.SncDataAt {X : Scheme} (D Z : X.IdealSheafData) (x : ↥X) : Prop

The snc data of the centre Z and of a component D at a point: a regular system of parameters z with D_x = (z_c) and Z_x = (z_l : l ∈ s).

Equations

• One or more equations did not get rendered due to their size.

theorem AlgebraicGeometry.stalkIdeal_saturate_eq_of_mem_support {X : Scheme} (hreg : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) (D Z : X.IdealSheafData) (hZ : Z.IsInvertible) (hdata : ∀ x ∈ D.support, x ∈ Z.support → SncDataAt D Z x) {w : ↥X} (hw : w ∈ (D.saturate Z).support) : (D.saturate Z).stalkIdeal w = D.stalkIdeal w

On the support of the saturation, the saturation of D along the invertible centre Z has the stalks of D: at a point of Z on D with D_x = (z_c), Z_x = (z_j), either c ≠ j and the colon computation gives (z_c), or c = j, the stalk of the saturation is (1) and the point is not on the support.

theorem AlgebraicGeometry.saturate_eq_self_of_snc_transversal {X : Scheme} (hreg : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) (D Z : X.IdealSheafData) (hZ : Z.IsInvertible) (hdata : ∀ x ∈ D.support, x ∈ Z.support → ∃ (n : ℕ) (z : Fin n → ↑(X.presheaf.stalk x)) (c : Fin n) (s : Finset (Fin n)), IsLocalRing.maximalIdeal ↑(X.presheaf.stalk x) = Ideal.span (Set.range z) ∧ ↑n = ringKrullDim ↑(X.presheaf.stalk x) ∧ D.stalkIdeal x = Ideal.span {z c} ∧ Z.stalkIdeal x = Ideal.span (z '' ↑s) ∧ c ∉ s) : D.saturate Z = D

For a component D transversal to the invertible centre Z at every point (c ∉ s in the snc data), the saturation of D along Z is D.

theorem AlgebraicGeometry.isRegular_subscheme_saturate {X : Scheme} (hreg : ∀ (x : ↥X), IsRegularLocalRing ↑(X.presheaf.stalk x)) (D Z : X.IdealSheafData) (hZ : Z.IsInvertible) (hdata : ∀ x ∈ D.support, x ∈ Z.support → SncDataAt D Z x) (hD : IsRegular D.subscheme) : IsRegular (D.saturate Z).subscheme

The subscheme of the saturation of D along the invertible centre Z is regular when V(D) is: on its support the saturation has the stalks of D.

theorem AlgebraicGeometry.strictTransformAlong_eq_comap_of_saturate_eq {B X : Scheme} (π : B ⟶ X) [CategoryTheory.IsIso π] (Z D : X.IdealSheafData) (h : D.saturate Z = D) : D.strictTransformAlong π (Z.comap π) = D.comap π

For an isomorphism π (a trivial blow-up) and a closed subscheme D whose saturation along the centre is D, the strict transform of D is D carried along π.