Remark 33 on the affine model: the exceptional divisors #
[Kol07, Remark 33]: under the isomorphism e : X_2 ≅ X_2' of
HironakaExamples/Sequence/Remark33Iso.lean, the exceptional divisors are interchanged,
E_0' ↔ E_1 and E_1' ↔ E_0, where on X_2 = B_{C'} B_p 𝔸³ the divisors are E_1 = π_1⁻¹(C') and
the birational transform of E_0 = π_0⁻¹(p), and on X_2' = B_D B_C 𝔸³ they are E_1' = σ_1⁻¹(D)
and the birational transform of E_0' = σ_0⁻¹(C). The main result is exists_iso_last_exceptional.
Only the compatibility e ≫ Σ = Π is used. Write F := π_1⁻¹ E_0 = Π⁻¹(p) and
E_1 = π_1⁻¹ C' on X_2. Since D = σ_0⁻¹(p), the pullback of E_1' = σ_1⁻¹ D along e is
Π⁻¹(p) = F, and the pullback of the total transform σ_1⁻¹ σ_0⁻¹ C is
Π⁻¹(C) = π_1⁻¹(E_0 · C') = F · E_1 (the key identity curve_comap_eq). So the two assertions are
F.saturate E_1 = F: the total transform ofE_0under the blow-up ofC'is already its birational transform (C' ⊄ E_0), and(F · E_1).saturate F = E_1: the birational transform ofE_0' = σ_0⁻¹ CisE_1.
Both follow from the colon identities (F : E_1) = F and (E_1 : F) = E_1 (the two divisors
share no component) together with (F · E_1 : F) = E_1 for the invertible F, and the one-step
saturation lemma saturate_eq_self_of_colon_eq. The colon identities are checked on a cover of
X_2: over the x- and y-charts of X_1 the ideal C' is the unit ideal, so the second
blow-up is an isomorphism there and E_1 = ⊤; over the z-chart, C' = V(x, y) and E_0 = V(z)
once more, so the second blow-up is B_{V(x,y)} 𝔸³, whose two charts carry E_1 = (x_j) and
F = (z), two distinct coordinate hyperplanes, with (x_j) : (z) = (x_j) and (z) : (x_j) = (z)
because both are prime ideals of k[x, y, z] not containing the other's generator. The cover of
X_2 by the blow-ups of the restrictions C'|_{U_j} comes from the pullback square
isPullback_blowUpMap along the open immersions U_j → X_1.
Invertibility of F is free from the isomorphism: F is the pullback along e of the
exceptional divisor σ_1⁻¹ D of X_2'.
The general lemmas (inequalities on covers by open immersions, colons along open immersions,
blow-ups of restrictions to opens) are in the library module
Hironaka/Scheme/BlowUpSequence/Remark33Exceptional.lean.
Two coordinate hyperplanes of 𝔸³ share no component #
(x_a) is a prime ideal of k[x, y, z].
x_b ∉ (x_a) for a ≠ b.
Two distinct coordinate hyperplanes share no component: (x_a) : (x_b) = (x_a).
The chart substitution of the x_j-chart of B_{V(x,y)} 𝔸³ (j < 2): x_i ↦ x_i x_j for
i < 2, i ≠ j; z ↦ z.
Equations
Instances For
In the chart of x_j (j < 2) of B_{V(x,y)} 𝔸³, the ideal (x, y) becomes (x_j): the
exceptional ideal.
The plane z = 0 is untouched by the charts of B_{V(x,y)} 𝔸³.
In the z-chart of B_p 𝔸³, the ideal (x, y) is (z) · (x, y) and its (z)-colon is
(x, y) again.
In the x- and y-charts of B_p 𝔸³ the ideal (x, y) is the exceptional ideal itself,
whose colon by itself is the unit ideal.
On B_{V(x,y)} 𝔸³: the exceptional divisor and the plane z = 0 share no component #
The plane z = 0 as an ideal sheaf on Spec k[x, y, z]: over the z-chart of B_p 𝔸³ it is
the exceptional divisor E_0.
Equations
Instances For
The charts of B_{V(x,y)} 𝔸³ through a chosen isomorphism with the model blow-up.
Equations
Instances For
On B_J 𝔸³ with J = V(x, y) and A = V(z): the total transforms of A and J share no
component, in the form of both colon identities. Stated for J and A given by equations so
that it applies to the restrictions of the second blow-up's data.
The trivial case: over a chart where the center is the unit ideal, both colon identities hold for free.
On X_2 = B_{C'} B_p 𝔸³: F = π_1⁻¹ E_0 and E_1 = π_1⁻¹ C' share no component #
The exceptional divisor E_0 of the point blow-up, as an ideal sheaf on blowUp (Zs k).
Equations
Instances For
The birational transform C' of the z-axis under the point blow-up.
Equations
Instances For
The total transform F = π_1⁻¹ E_0 on X_2 = B_{C'} X_1.
Equations
Instances For
The exceptional divisor E_1 = π_1⁻¹ C' of the second blow-up.
Equations
Instances For
The restriction of C' to the chart of x_j, as the chart ideal ((x, y)·𝒪 : E_0).
The total transform of E_0 under the blow-up of C' is its birational transform:
F.saturate E_1 = F.
The birational transform of F · E_1 along F is E_1: (F · E_1).saturate F = E_1
((F · E_1 : F) = E_1 for the invertible F).
F is invertible: it is the pullback along the isomorphism e of the exceptional divisor of
X_2' = B_D B_C 𝔸³.
Under any isomorphism e : X_2 ≅ X_2' over 𝔸³ (stated for the coordinate subspaces Zs
and Ys), the birational transform of E_0' = σ_0⁻¹ C pulls back to E_1, and E_1' = σ_1⁻¹ D
pulls back to the birational transform of E_0.
The matching of the exceptional divisors for centers p, C given by equations, in the
shape the recursive definitions of BlowUpSequence produce (the identity arms of step at
index 0).
[Kol07, Remark 33]: the isomorphism X_2 ≅ X_2' over 𝔸³ matches the exceptional divisors,
E_0' ↔ E_1 and E_1' ↔ E_0.