The shape of the total transform at a point of the exceptional divisor

Hauser's chart computation (the proof of [Hau14, Proposition 5.3]; [Hau14, Proposition 5.4 (7)]) reads the total transform of an snc divisor at a point x' of the exceptional divisor F of a smooth blow-up in coordinates y at x' for which F = (y_j): the total transform of a component containing the centre is (y_c · y_j) — or (y_j) for the component whose coordinate is the chart coordinate — and that of a transversal component is (y_c); a component not through x' has total transform (1). Its strict transform is the saturation ⋃_k (T : F^k), which divides out the exceptional factor: (y_c y_j) : y_j^∞ = (y_c), (y_j) : y_j^∞ = (1).

This module isolates that shape as a predicate on a local ring, TotalTransformData F T — a regular system of parameters z with F = (z_j) and each T i of one of the four shapes, the parameter indices of the components through the point being distinct and different from j — proves that the predicate transports along ring isomorphisms (how the chart computation reaches the stalk 𝒪_{B,x'}, Hironaka.Scheme.Snc.TotalTransformOnCentre), and computes the saturations in a regular local ring: the strict transform of a component through x' is the prime (z_a), that of a component missing x' (or of the component with c = j, [Hau14, Definition 6.2]) is (1). The assembly into Kollár's conditions (1)–(3) for the total transform (exists_snc_data_totalTransform_of_mem_support of Hironaka.Scheme.Snc.TotalTransformSnc) then only reads off the indices.

Why the saturations hold. (z_a) is prime for a member of a regular system of parameters (the quotient is regular, hence a domain), and z_j ∉ (z_a) for a ≠ j (distinct members are independent modulo 𝔪²). Hence z_a z_j ∣ r z_j^k forces z_a ∣ r, so (z_a z_j) : z_j^k ⊆ (z_a) for every k, with equality of the union at k = 1; (z_a) : z_j^k = (z_a) since (z_a) is a prime not containing z_j; and (z_j) : z_j = (1).

Sources: [Hau14, Proposition 5.3] (the proof); [Hau14, Proposition 5.4 (7); Definition 6.2]; [Kol07, Definition 24].

def AlgebraicGeometry.TotalTransformData {S : Type u} [CommRing S] [IsLocalRing S] {ι : Type v} (F : Ideal S) (T : ι → Ideal S) : Prop

The shape of the total transform at a point x' of the exceptional divisor (the proof of [Hau14, Proposition 5.3]): the stalk is a regular local ring with a regular system of parameters z, the exceptional divisor has stalk (z_j), and the total transform T i of each component is (z_{a i} · z_j) (a component containing the centre, through x'), (z_{a i}) (a transversal component through x'), (z_j) (the component of the chart coordinate) or (1) (a component missing x'); the indices a i of the components through x' are different from j and distinct (the index of a component missing x' is irrelevant and may be taken to be j).

Equations

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

theorem AlgebraicGeometry.map_maximalIdeal_ringEquiv {S : Type u} [CommRing S] [IsLocalRing S] {S' : Type w} [CommRing S'] [IsLocalRing S'] (e : S ≃+* S') : Ideal.map e.symm (IsLocalRing.maximalIdeal S') = IsLocalRing.maximalIdeal S

The maximal ideal transports along a ring isomorphism of local rings.

theorem AlgebraicGeometry.TotalTransformData.of_ringEquiv {S : Type u} [CommRing S] [IsLocalRing S] {ι : Type v} {S' : Type w} [CommRing S'] [IsLocalRing S'] (e : S ≃+* S') {F : Ideal S} {T : ι → Ideal S} {F' : Ideal S'} {T' : ι → Ideal S'} (hF : Ideal.map e F = F') (hT : ∀ (i : ι), Ideal.map e (T i) = T' i) (h : TotalTransformData F' T') : TotalTransformData F T

The total-transform shape transports along a ring isomorphism e : S ≃ S' carrying the ideals F, T i to F', T' i.

theorem AlgebraicGeometry.notMem_span_singleton_of_ne {R : Type u} [CommRing R] [IsRegularLocalRing R] {m : ℕ} {z : Fin m → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R) (hn : ↑m = ringKrullDim R) {a j : Fin m} (haj : a ≠ j) : z j ∉ Ideal.span {z a}

z_j ∉ (z_a) for distinct members of a regular system of parameters.

theorem AlgebraicGeometry.iSup_colon_pow_span_singleton_mul {R : Type u} [CommRing R] [IsRegularLocalRing R] {m : ℕ} {z : Fin m → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R) (hn : ↑m = ringKrullDim R) {a j : Fin m} (haj : a ≠ j) : ⨆ (k : ℕ), Submodule.colon (Ideal.span {z a * z j}) ↑(Ideal.span {z j} ^ k) = Ideal.span {z a}

[Hau14, Proposition 5.4 (7)]: (z_a z_j) : z_j^∞ = (z_a) for a ≠ j — the saturation divides out the exceptional factor.

theorem AlgebraicGeometry.iSup_colon_pow_span_singleton_of_ne {R : Type u} [CommRing R] [IsRegularLocalRing R] {m : ℕ} {z : Fin m → R} (hz : Ideal.span (Set.range z) = IsLocalRing.maximalIdeal R) (hn : ↑m = ringKrullDim R) {a j : Fin m} (haj : a ≠ j) : ⨆ (k : ℕ), Submodule.colon (Ideal.span {z a}) ↑(Ideal.span {z j} ^ k) = Ideal.span {z a}

The proof of [Hau14, Proposition 5.3]: (z_a) : z_j^∞ = (z_a) for a ≠ j — a transversal component is unchanged by the saturation.

theorem AlgebraicGeometry.iSup_colon_pow_span_singleton_self {R : Type u} [CommRing R] (g : R) : ⨆ (k : ℕ), Submodule.colon (Ideal.span {g}) ↑(Ideal.span {g} ^ k) = ⊤

(z_j) : z_j^∞ = (1): the component of the chart coordinate dies ([Hau14, Definition 6.2]).

theorem AlgebraicGeometry.iSup_colon_pow_top {R : Type u} [CommRing R] (J : Ideal R) : ⨆ (k : ℕ), Submodule.colon ⊤ ↑(J ^ k) = ⊤

The saturation of the unit ideal is the unit ideal.

theorem AlgebraicGeometry.TotalTransformData.iSup_colon_eq {S : Type u} [CommRing S] [IsLocalRing S] {ι : Type v} {F : Ideal S} {T : ι → Ideal S} (h : TotalTransformData F T) : IsRegularLocalRing S ∧ ∃ (m : ℕ) (z : Fin m → S), (Ideal.span (Set.range z) = IsLocalRing.maximalIdeal S ∧ ↑m = ringKrullDim S) ∧ ∃ (j : Fin m) (a : ι → Fin m), F = Ideal.span {z j} ∧ (∀ (i i' : ι), a i ≠ j → a i' ≠ j → a i = a i' → i = i') ∧ ∀ (i : ι), a i ≠ j ∧ ⨆ (k : ℕ), Submodule.colon (T i) ↑(F ^ k) = Ideal.span {z (a i)} ∨ ⨆ (k : ℕ), Submodule.colon (T i) ↑(F ^ k) = ⊤

The strict transforms read off the total-transform shape: the saturation ⋃ₖ (T i : F^k) is (z_{a i}) for a component through x' (its index a i ≠ j) and (1) otherwise.