The strict transform in the flat case equals the total transform

If a scheme X over S is flat over S at all points lying over the centre Z, its strict transform under the blow-up of S along Z is the base change X ×_S S' [TSPA, Tag 080F]. Here Y = V(J) ⊆ X is a closed subscheme, π : B ⟶ X a morphism whose inverse image E = D.comap π of the centre is invertible (the blow-up and its exceptional ideal in the applications), and the hypothesis is the flatness of the stalk maps 𝒪_{X, ι y} → 𝒪_{Y, y} at the points y of Y over Z = V(D).

The strict transform Jˢ = (J* : E^∞) equals J* as soon as (J* : E) = J* (saturate_eq_self_of_colon_eq). That inclusion is local on B: on an affine open U' ⊆ B over an affine open U ⊆ X, with E(U') = (e), e a nonzerodivisor, and J*(U') = J(U)·Γ(U') (ideal_comap_of_le), it says that u e ∈ J(U)Γ(U') forces u ∈ J(U)Γ(U'). Membership in an ideal is checked at every maximal ideal Q of Γ(U') in the elementary form "some t ∉ Q has t u in the ideal" (Ideal.mem_of_forall_exists_mul_mem). If e ∉ Q, take t = e. If J(U)Γ(U') ⊄ Q, take t in J(U)Γ(U') ∖ Q. Otherwise the point b ∈ U' of Q lies in the exceptional divisor and in V(J*), so x = π b lies in Z ∩ V(J) and is the image of a point y of Y at which the closed immersion is flat. A flat surjective ring map out of a local ring is injective — its kernel is a pure ideal (Ideal.Pure, [TSPA, Tag 04PS]), and a pure ideal K of a local ring is zero: x ∈ K has x = x k for some k ∈ K ⊆ 𝔪, and 1 − k is a unit. Since the sections of J over U vanish on Y, their germs at x are killed by the stalk map, hence are zero: every j ∈ J(U) is annihilated by some s ∉ 𝔭_x (the stalk is the localization at 𝔭_x). Writing u e = ∑ cᵢ φ(jᵢ) with finitely many jᵢ ∈ J(U) and taking s the product of the corresponding annihilators, φ(s) u e = 0, so φ(s) u = 0 because e is a nonzerodivisor, and t = φ(s) ∉ Q does the job.

This is a different proof from the Stacks Project's (which treats an arbitrary X → S through the torsion of N ⊗_A A[I/a]): for a closed subscheme, flatness of the immersion at y forces the ideal to vanish at ι y, which is what makes the total transform already saturated there.

Main declarations

• AlgebraicGeometry.injective_of_flat_of_surjective: a flat surjective ring map from a local ring to a nontrivial ring is injective.
• IdealSheafData.germ_eq_zero_of_flat_stalkMap, exists_mul_eq_zero_of_flat_stalkMap: the sections of J over an affine open vanish at a point of V(J) where the closed immersion is flat.
• Ideal.mem_of_forall_exists_mul_mem: the elementary localization principle for membership.
• AlgebraicGeometry.colon_comap_le_comap_of_flat, strictTransformAlong_eq_comap_of_flat (for any π with invertible D.comap π).

theorem AlgebraicGeometry.injective_of_flat_of_surjective {R : Type u_1} {S : Type u_2} [CommRing R] [CommRing S] [IsLocalRing R] [Nontrivial S] (f : R →+* S) (hf : f.Flat) (hs : Function.Surjective ⇑f) : Function.Injective ⇑f

A flat surjective ring homomorphism out of a local ring into a nontrivial ring is injective: its kernel is a pure ideal [TSPA, Tag 04PS], and a pure ideal of a local ring is zero.

theorem Ideal.mem_of_forall_exists_mul_mem {R : Type u_1} [CommRing R] {I : Ideal R} {u : R} (h : ∀ (Q : Ideal R), Q.IsMaximal → ∃ t ∉ Q, t * u ∈ I) : u ∈ I

The elementary localization principle for membership in an ideal: u ∈ I as soon as every maximal ideal Q admits t ∉ Q with t u ∈ I (the ideal (I : u) is then contained in no maximal ideal, hence is the unit ideal).

theorem AlgebraicGeometry.Scheme.IdealSheafData.germ_eq_zero_of_flat_stalkMap {X : Scheme} (J : X.IdealSheafData) (y : ↥J.subscheme) (hflat : (CommRingCat.Hom.hom (Hom.stalkMap J.subschemeι y)).Flat) (U : ↑X.affineOpens) {x : ↥X} (hxy : J.subschemeι y = x) (hx : x ∈ ↑U) {j : ↑(X.presheaf.obj (Opposite.op ↑U))} (hj : j ∈ J.ideal U) : (CategoryTheory.ConcreteCategory.hom (X.presheaf.germ (↑U) x hx)) j = 0

At a point y of the closed subscheme V(J) where the closed immersion is flat, the germs of the sections of J vanish: the stalk map is flat and surjective out of a local ring, hence injective, and it kills the germs of J because the sections of J restrict to zero on V(J).

theorem AlgebraicGeometry.Scheme.IdealSheafData.exists_mul_eq_zero_of_flat_stalkMap {X : Scheme} (J : X.IdealSheafData) (U : ↑X.affineOpens) (q : PrimeSpectrum ↑(X.presheaf.obj (Opposite.op ↑U))) (y : ↥J.subscheme) (hy : J.subschemeι y = (IsAffineOpen.fromSpec ⋯) q) (hflat : (CommRingCat.Hom.hom (Hom.stalkMap J.subschemeι y)).Flat) {j : ↑(X.presheaf.obj (Opposite.op ↑U))} (hj : j ∈ J.ideal U) : ∃ s ∉ q.asIdeal, s * j = 0

The affine form: at the point fromSpec q of U, image of a point y of V(J) where the closed immersion is flat, every section j ∈ J(U) is annihilated by some s ∉ q.

theorem AlgebraicGeometry.colon_comap_le_comap_of_flat {B X : Scheme} (π : B ⟶ X) (D J : X.IdealSheafData) (hE : (D.comap π).IsInvertible) (hflat : ∀ (y : ↥J.subscheme), J.subschemeι y ∈ D.support → (CommRingCat.Hom.hom (Scheme.Hom.stalkMap J.subschemeι y)).Flat) : (J.comap π).colon (D.comap π) ≤ J.comap π

The local statement of [TSPA, Tag 080F]: for π : B ⟶ X with invertible E = D.comap π, if the closed immersion V(J) → X is flat at every point over Z = V(D), then (J* : E) ≤ J*.

theorem AlgebraicGeometry.strictTransformAlong_eq_comap_of_flat {B X : Scheme} (π : B ⟶ X) (D J : X.IdealSheafData) (hE : (D.comap π).IsInvertible) (hflat : ∀ (y : ↥J.subscheme), J.subschemeι y ∈ D.support → (CommRingCat.Hom.hom (Scheme.Hom.stalkMap J.subschemeι y)).Flat) : J.strictTransformAlong π (D.comap π) = J.comap π

The flat case of the strict transform [TSPA, Tag 080F]: if the closed immersion V(J) → X is flat at every point over the centre, the strict transform of J along π is its total transform.