The principal case of the weak transform

For principal ideals the weak and strict transforms coincide [Hau14, Remark 6.9]. Here I^g is the weak transform (I* : E^N) with N the exceptional order, the largest N with E^N ∣ I* [Hir64, Ch. 0, §5, p. 142], and Iˢ = ⋃ᵢ (I* : Eⁱ) the strict transform, for I* = I.comap π the total transform of a locally principal I and E the (invertible) ideal of the exceptional divisor F = V(E). Hauser's setting is a regular ambient scheme with a regular centre, so that F is regular and irreducible; weakTransformAlong_eq_strictTransformAlong_of_locally_principal' states the result under exactly these hypotheses, and weakTransformAlong_eq_strictTransformAlong_of_locally_principal under the one the proof uses, the integrality of F. The auxiliary lemmas (the integrality of a regular irreducible closed subscheme, the primality of its ideal on a chart, and I ≤ E ^ c → E ^ c ∣ I for invertible E) are used for the components of normal crossings divisors (Hironaka.Resolution.Algebraic.Snc.ComponentStalks), the order along the exceptional divisor (Hironaka.Scheme.IdealSheaf.Order.Exceptional) and hypersurfaces of maximal contact (Hironaka.Resolution.Algebraic.MaximalContact.AgreeOnBlowUp).

The argument

Write N for the exceptional order. Since (I* : Eⁱ) increases with i and (I* : Eⁱ) ⊆ Iˢ for every i, everything reduces to the single inequality (I* : E^(N+1)) ⊆ (I* : E^N): it gives (I* : E^(N+i)) = (I* : E^N) for all i by colon_colon, hence Iˢ = (I* : E^N).

On an affine chart U' of the blow-up over an affine U of X with I(U) = (f) and E(U') = (e), e a nonzerodivisor (E is invertible), the total transform is (f*) with f* = π♯ f (ideal_comap_of_le), and the inequality reads: u e^(N+1) ∈ (f*) ⇒ u e^N ∈ (f*).

• If U' misses F, then E(U') = Γ(U'), e is a unit and there is nothing to prove.
• If U' meets F and the exceptional order is attained (E^N ∣ I*, E^(N+1) ∤ I*), then f* = e^N g with e ∤ g and the ring form of the strict transform, f* = h^k f^s [Hau14, Definition 6.2], applies once e is prime in Γ(U'): from u e^(N+1) = v e^N g cancel e^N, so e ∣ v g, e ∣ v, v = e w, u = w g and u e^N = w f*.
• If every power of E divides I* (so N = 0, the supremum in ℕ of an unbounded set being 0), then f* is divisible by every power of e; on the Noetherian ring Γ(U') the chain (f*) : eⁱ stabilizes and yields (1 - a e) f* = 0 for some a, whence (f* : e) = (f*).

Two facts carry the hypotheses of the statement:

1. e is prime. F = V(E) is irreducible and its stalks are regular local rings, hence domains, so F is reduced and therefore integral. Then Γ(F ∩ U') is a domain and E(U') = ker (Γ(U') → Γ(F ∩ U')) (Mathlib ker_subschemeι_app) is a prime ideal.
2. Constancy of the exceptional order along F. If e^(N+1) ∣ f* on one chart meeting F, then E^(N+1) ∣ I* everywhere: any other chart U'' meeting F meets it in a nonempty open of the irreducible F, and on a common smaller chart V the divisibility says that the restriction of g (from f* = e^N g on U'') lies in E(V), i.e. vanishes on F ∩ V; on the integral F a section vanishing on a nonempty open vanishes (map_injective_of_isIntegral), so g ∈ E(U'') and e^(N+1) ∣ f* on U''. Charts missing F divide trivially.

Fact (2) says that the order of f* along F is its order at the generic point of F; the argument above reads this on sections (the generic point is not named). The regularity of the ambient scheme, part of Hauser's setting, is not among the hypotheses of the theorems here; the regularity of F enters only through the reducedness of F.

Conventions

The transforms are strictTransformAlong π E I, controlledTransformAlong π E I c, exceptionalOrderAlong π E I = sSup {c | E ^ c ∣ I.comap π} (0 when unbounded), and weakTransformAlong π E I, the controlled transform with the exceptional order as control. Invertibility is IsInvertible (locally a nonzerodivisor generator). Integrality of a scheme is Mathlib's IsIntegral.

Ring lemmas

theorem AlgebraicGeometry.mem_nonZeroDivisors_of_span_singleton_eq {A : Type u_1} [CommRing A] {a b : A} (ha : a ∈ nonZeroDivisors A) (h : Ideal.span {a} = Ideal.span {b}) : b ∈ nonZeroDivisors A

Two generators of one principal ideal: if one is a nonzerodivisor, so is the other.

theorem AlgebraicGeometry.mul_pow_mem_span_of_mul_pow_succ_mem {A : Type u_1} [CommRing A] {e f : A} (he : e ∈ nonZeroDivisors A) (hp : Prime e) {N : ℕ} (hN : e ^ N ∣ f) (hN' : ¬e ^ (N + 1) ∣ f) {u : A} (hu : u * e ^ (N + 1) ∈ Ideal.span {f}) : u * e ^ N ∈ Ideal.span {f}

The ring form of the strict transform of a principal ideal [Hau14, Definition 6.2] at a chart meeting the divisor: for a prime nonzerodivisor e and f = eᴺ g with e ∤ g, (f : eᴺ⁺¹) ⊆ (f : eᴺ).

theorem AlgebraicGeometry.mem_span_of_mul_mem_of_forall_pow_dvd {A : Type u_1} [CommRing A] [IsNoetherianRing A] {e f : A} (he : e ∈ nonZeroDivisors A) (hf : ∀ (i : ℕ), e ^ i ∣ f) {u : A} (hu : u * e ∈ Ideal.span {f}) : u ∈ Ideal.span {f}

Chain form of Krull's intersection theorem, as needed for an unbounded exceptional order: in a Noetherian ring, if the nonzerodivisor e has every power dividing f, then (f : e) = (f).

Sections of an ideal sheaf whose closed subscheme is integral

theorem AlgebraicGeometry.Scheme.IdealSheafData.isIntegral_subscheme_of_isRegularLocalRing_stalk {X : Scheme} (E : X.IdealSheafData) [IrreducibleSpace ↥E.subscheme] (h : ∀ (z : ↥E.subscheme), IsRegularLocalRing ↑(E.subscheme.presheaf.stalk z)) : IsIntegral E.subscheme

The closed subscheme V(E) is integral when it is irreducible and its stalks are regular local rings (regular local rings are domains, so V(E) is reduced).

theorem AlgebraicGeometry.Scheme.IdealSheafData.ideal_eq_top_of_forall_notMem {X : Scheme} (E : X.IdealSheafData) (U : ↑X.affineOpens) (h : ∀ (z : ↥E.subscheme), E.subschemeι z ∉ ↑U) : E.ideal U = ⊤

An affine open missing V(E) has E(U) = Γ(U).

theorem AlgebraicGeometry.Scheme.IdealSheafData.isPrime_ideal_of_isIntegral_subscheme {X : Scheme} (E : X.IdealSheafData) [IsIntegral E.subscheme] (U : ↑X.affineOpens) {z : ↥E.subscheme} (hz : E.subschemeι z ∈ ↑U) : (E.ideal U).IsPrime

On an affine open meeting the integral closed subscheme V(E), the ideal E(U) is prime: it is the kernel of Γ(U) → Γ(V(E) ∩ U) and the target is a domain.

theorem AlgebraicGeometry.Scheme.IdealSheafData.mem_ideal_of_map_mem_of_isIntegral_subscheme {X : Scheme} (E : X.IdealSheafData) [IsIntegral E.subscheme] {U V : ↑X.affineOpens} (h : V ≤ U) {z : ↥E.subscheme} (hz : E.subschemeι z ∈ ↑V) {g : ↑(X.presheaf.obj (Opposite.op ↑U))} (hg : (CommRingCat.Hom.hom (X.presheaf.map (CategoryTheory.homOfLE h).op)) g ∈ E.ideal V) : g ∈ E.ideal U

On the integral closed subscheme V(E), a section vanishing on a nonempty open vanishes: if the restriction of g ∈ Γ(U) to an affine V ≤ U meeting V(E) lies in E(V), then g ∈ E(U).

Divisibility by powers of an invertible ideal sheaf

theorem AlgebraicGeometry.le_pow_of_pow_dvd {B : Scheme} {I E : B.IdealSheafData} {c : ℕ} (h : E ^ c ∣ I) : I ≤ E ^ c

E ^ c ∣ I implies I ≤ E ^ c.

theorem AlgebraicGeometry.pow_dvd_of_le_pow_of_isInvertible {B : Scheme} {I E : B.IdealSheafData} (hE : E.IsInvertible) {c : ℕ} (h : I ≤ E ^ c) : E ^ c ∣ I

For an invertible E, I ≤ E ^ c implies E ^ c ∣ I (with quotient (I : E ^ c)).

theorem AlgebraicGeometry.ideal_le_pow_of_le {B : Scheme} {I K : B.IdealSheafData} {U V : ↑B.affineOpens} (h : V ≤ U) {c : ℕ} (hU : I.ideal U ≤ K.ideal U ^ c) : I.ideal V ≤ K.ideal V ^ c

Divisibility on a chart restricts to smaller affine opens.

theorem AlgebraicGeometry.exists_chart_of_locally_principal {B X : Scheme} (π : B ⟶ X) (E : B.IdealSheafData) (J : X.IdealSheafData) (hE : E.IsInvertible) (hJ : ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}) (b : ↥B) : ∃ (U : ↑X.affineOpens) (U' : ↑B.affineOpens) (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f} ∧ b ∈ ↑U' ∧ ↑U' ≤ (TopologicalSpace.Opens.map π.base).obj ↑U ∧ ∃ e ∈ nonZeroDivisors ↑(B.presheaf.obj (Opposite.op ↑U')), E.ideal U' = Ideal.span {e}

The charts used below: an affine open U of X around π b on which the locally principal J is principal, and an affine open U' ∋ b of B inside π⁻¹U on which the invertible E is generated by a nonzerodivisor.

theorem AlgebraicGeometry.locally_principal_of_forall_principal {X : Scheme} (J : X.IdealSheafData) (hJ : ∀ (U : ↑X.affineOpens), ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}) (x : ↥X) : ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}

Principality on every affine open gives principality on an affine neighbourhood of every point, the hypothesis of weakTransformAlong_eq_strictTransformAlong_of_locally_principal.

Constancy of the exceptional order along an integral exceptional divisor

theorem AlgebraicGeometry.ideal_comap_le_pow_succ_of_le {B X : Scheme} (π : B ⟶ X) (E : B.IdealSheafData) (J : X.IdealSheafData) [IsIntegral E.subscheme] (U : ↑X.affineOpens) (U' : ↑B.affineOpens) (hle : ↑U' ≤ (TopologicalSpace.Opens.map π.base).obj ↑U) {e : ↑(B.presheaf.obj (Opposite.op ↑U'))} (hEe : E.ideal U' = Ideal.span {e}) {f : ↑(X.presheaf.obj (Opposite.op ↑U))} (hf : J.ideal U = Ideal.span {f}) {N : ℕ} (hN : (J.comap π).ideal U' ≤ E.ideal U' ^ N) (V : ↑B.affineOpens) (hV : V ≤ U') {z : ↥E.subscheme} (hz : E.subschemeι z ∈ ↑V) (heV : ∃ e' ∈ nonZeroDivisors ↑(B.presheaf.obj (Opposite.op ↑V)), E.ideal V = Ideal.span {e'}) (h : (J.comap π).ideal V ≤ E.ideal V ^ (N + 1)) : (J.comap π).ideal U' ≤ E.ideal U' ^ (N + 1)

Constancy of the exceptional order, chart to chart: on a chart U' of B over an affine U of X with J(U) = (f), E(U') = (e), e a nonzerodivisor and eᴺ ∣ π♯ f, if the total transform is divisible by E ^ (N + 1) on a smaller affine V meeting V(E), then it is divisible by E ^ (N + 1) on U'.

theorem AlgebraicGeometry.comap_le_pow_succ_of_chart {B X : Scheme} (π : B ⟶ X) (E : B.IdealSheafData) (J : X.IdealSheafData) [IsIntegral E.subscheme] (hE : E.IsInvertible) (hJ : ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}) {N : ℕ} (hN : J.comap π ≤ E ^ N) (U₀ : ↑B.affineOpens) {z₀ : ↥E.subscheme} (hz₀ : E.subschemeι z₀ ∈ ↑U₀) (h₀ : (J.comap π).ideal U₀ ≤ E.ideal U₀ ^ (N + 1)) : J.comap π ≤ E ^ (N + 1)

Constancy of the exceptional order along an integral divisor: for J locally principal, E invertible with V(E) integral and J* ≤ E ^ N, if E ^ (N + 1) divides the total transform on one affine open meeting V(E), it divides it everywhere.

The principal case

theorem AlgebraicGeometry.weakTransformAlong_eq_strictTransformAlong_of_locally_principal {B X : Scheme} (π : B ⟶ X) (E : B.IdealSheafData) (J : X.IdealSheafData) [IsIntegral E.subscheme] [IsLocallyNoetherian B] (hE : E.IsInvertible) (hJ : ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}) : J.weakTransformAlong π E = J.strictTransformAlong π E

For principal ideals the weak and strict transforms coincide [Hau14, Remark 6.9]: along π : B ⟶ X with B locally Noetherian, E an invertible ideal sheaf on B whose closed subscheme is integral and J locally principal on X (principal on an affine neighbourhood of every point), the weak transform of J is its strict transform.

theorem AlgebraicGeometry.weakTransformAlong_eq_strictTransformAlong_of_locally_principal' {B X : Scheme} (π : B ⟶ X) (E : B.IdealSheafData) (J : X.IdealSheafData) [IsLocallyNoetherian B] (hE : E.IsInvertible) (hF : ∀ (z : ↥E.subscheme), IsRegularLocalRing ↑(E.subscheme.presheaf.stalk z)) [IrreducibleSpace ↥E.subscheme] (hJ : ∀ (x : ↥X), ∃ (U : ↑X.affineOpens), x ∈ ↑U ∧ ∃ (f : ↑(X.presheaf.obj (Opposite.op ↑U))), J.ideal U = Ideal.span {f}) : J.weakTransformAlong π E = J.strictTransformAlong π E

The principal case of the weak transform in Hauser's setting [Hau14, Remark 6.9]: the exceptional divisor V(E) regular (stalks regular local rings) and irreducible.