Kollár's Example 106 for the order-reduction functor: at least four blow-ups of order two #
After the blow-up of the origin, the point q ∈ E₁ of the z-chart has order 2 for the
transform (I₁, 2) (HironakaExamples/OrderReduction/Example106BlowUp.lean); blowing it up, the
origin q' of the w₂-chart is again of order 2, and after that blow-up the origin q'' of the
w₃-chart is again of order 2 (the chart identities of
HironakaExamples/MaximalContact/Example106Stages.lean). For the order-reduction functor of Kol07,
Theorem 103 this means that the order-2 run of BO_{4,2}(𝔸⁴_ℚ, I, ∅) has at least four blow-ups
(four_le_length_of_axioms), whereas the text of [Kol07, Example 106] passes to the mark 1 after
the first: the sequence cannot end while a point of order 2 exists (clause (1) of Theorem 103),
and its centres are forced one stage at a time by the cosupport forcing of
HironakaExamples/Sequence/CosuppForcing.lean.
The mechanism is one stage step, run twice. On a ℚ-scheme Y with a centre Z and an
ideal I whose order-2 locus is {ι 0}, for an open chart ι : 𝔸⁴_ℚ ⟶ Y on which Z is the
reduced origin and I is V(P), the blow-up of Y at Z receives the model blow-up of the
origin of 𝔸⁴ as an open piece (stepMap: the identification of
HironakaExamples/BlowUp/Glue/SpecIso.lean and the map of blow-ups along ι, a cartesian square),
on which the weak transform is the controlled transform (σ_j P : x_j²) chart by chart
(weakTransform_comap_stepMap); off the piece the weak transform has the order of I at the image
(ord_weakTransform_of_notMem), which is < 2. So the order-2 locus of the new weak transform is
read on the four charts of the model, the same computation as at stage 1 with the chart ideals
K_z = (x³z − y², z(x⁴z + x − w³)) (stage 2) and K_zw = (x³zw² − y², z(x⁴zw⁴ + x − w²)) (stage 3)
in place of I, and it is a single closed point (the cosupport is closed, isClosed_setOf_le_ord),
at which the forcing pins the next centre. That centre is the reduced point (the centres of an order
sequence are smooth, read on the pulled-back sequence: comap_eq_specIdealSheaf_centerIdeal), so
its chart form is again the origin and the step repeats. At stage 3 only the existence of the
order-2 point q'' is needed (two_le_ord_weakTransform_stepMap with ord_zero_example106_zww):
the final maximal order < 2 then forces a fourth blow-up (one_le_length_of_le_ord).
Every order-2 locus is computed at every scheme point, through the derivative criterion
ord_p ≥ 2 ↔ D(K) ⊆ p ([Kol07, Lemma 74 (3)]) on each chart. The three lemmas
comap_markedTransform_eqToHom, exists_eqToHom_apply_eq and map_span_pair are the
Scheme.{0} and ℚ[x, y, z, w] instances of their general forms in
Hironaka/Scheme/BlowUpSequence/InducedData.lean, Hironaka/Scheme/BlowUp/BlowUpMap.lean and
Hironaka/Scheme/BlowUp/Composite/ChartIdeal.lean; mem_of_two_mul_mem is specific to ℚ. The
result is applied to the functor's own sequence in HironakaExamples/KollarExample106Run.lean.
The model computation for an arbitrary ideal #
The controlled transform of control 2 of V(P) on the model blow-up of the origin of 𝔸⁴
([Kol07, Definition 60]): the shape of modelW for an arbitrary ideal P.
Equations
- One or more equations did not get rendered due to their size.
Instances For
Kollár's chart ideal (σ_j P : x_j²) on the chart of x_j.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The controlled transform on the chart of x_j is the ideal sheaf of the chart ideal
(σ_j P : x_j²) ([Kol07, Definition 60] on the chart, for any P; comap_modelW_modelChart is
the case P = I).
The image of a two-generator ideal under a chart substitution: the ℚ[x, y, z, w] instance of
Ideal.map_span_pair.
The chart ideal of a two-generator ideal whose generators transform with the factor x_j²
([Kol07, Definition 60]; the chart identities of Example106Charts.lean).
The derivative criterion on the chart of x_j: ord ≥ 2 at a point of the chart iff its
prime contains D(σ_j P : x_j²).
If no prime of a chart other than j₀ contains D(σ_j P : x_j²), and on the chart j₀ only
the origin does, then the order-2 locus of the controlled transform of V(P) on the model
blow-up is the origin of the chart j₀, at every scheme point (two_le_ord_modelW_iff for any
P).
The stage step: the blow-up at a chart origin receives the model blow-up as an open piece #
Transport of the marked transform along an equality of centres (the eqToHom of
eqToHom_comp_blowUpπ): the Scheme.{0} instance of
AlgebraicGeometry.comap_markedTransform_eqToHom.
The model blow-up of the origin of 𝔸⁴ as an open piece of the blow-up of Y at a centre ZY
that is the origin on the chart ι ([Kol07, 30.1], the pull-back of a blow-up along an open
immersion): blowUpMap ι ZY preceded by the transport of the centre and by blowUpSpecIso.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The open piece is an open immersion (isOpenImmersion_blowUpMap).
The open piece lies over the chart: stepMap ≫ π = π_model ≫ ι.
Points of a blow-up transport along an equality of centres: the Scheme.{0} instance of
AlgebraicGeometry.exists_eqToHom_apply_eq.
Every point of blowUp Y ZY over the chart lies on the open piece (the cartesian square of
blowUpMap, exists_blowUpMap_eq).
On the open piece the weak transform of IY is the model's controlled transform of V(P)
([Kol07, 58] against [Kol07, Definition 60]; weakTransform_eq_markedTransform_of_smooth and the
flat pull-back of colon ideals).
If the order-2 locus of IY is the chart origin ι 0, the centre is supported there, and
the chart hypotheses on V(P) hold (no prime of a chart other than j₀ contains the derivative of
its chart ideal, and on the chart j₀ only the origin does), then the order-2 locus of the weak
transform is the single point stepMap (chart j₀ 0), at every scheme point: on the open piece by
the model computation, off it by ord_weakTransform_of_notMem (the point lies off the exceptional
divisor and its image has order < 2).
The order-2 point of the new weak transform is a closed point: the closed cosupport
{ord ≥ 2} (isClosed_setOf_le_ord) is that single point.
The next centre of the order sequence is forced (clause (1) of [Kol07, Theorem 103] through the
cosupport forcing exists_eq_cons_of_ord_le_iff): it is supported exactly at the order-2 point
stepMap (chart j₀ 0).
A centre of an order sequence supported at the chart origin ι 0 is, on the chart, the reduced
origin (x, y, z, w) (centerIdeal): the centres are smooth ([Kol07, Definition 65 (1)]), hence
regular, hence reduced, hence the vanishing ideal of their support, read on the sequence pulled
back along the chart ([Kol07, 30.1]).
The origin of the chart j₀ on the open piece has ord ≥ 2 for the new weak transform as soon
as D(σ_{j₀} P : x_{j₀}²) ⊆ (x, y, z, w): the third stage.
Clause (1) of [Kol07, Theorem 103] at the end of a sequence: if a point of order ≥ m remains
while the final maximal order is < m, the sequence is not empty.
Stages 2 and 3: the chart ideals K_z and K_zw and their order-2 loci #
Kollár's I₁ on the z-chart: K_z = (x³z − y², z(x⁴z + x − w³)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The transform I₂ on the w₂-chart of the blow-up of q:
K_zw = (x³zw² − y², z(x⁴zw⁴ + x − w²)).
Equations
- One or more equations did not get rendered due to their size.
Instances For
The x₂-chart: (σ_x K_z : x²) = (x²z − y², z(x⁴z + 1 − w³x²)).
The y₂-chart: (σ_y K_z : y²) = (x³y²z − 1, z(x⁴y⁴z + x − w³y²)).
The z₂-chart: (σ_z K_z : z²) = (x³z² − y², x⁴z⁴ + x − w³z²).
The w₂-chart: (σ_w K_z : w²) = K_zw.
The w₃-chart: (σ_w K_zw : w²) = (x³zw⁴ − y², z(x⁴zw⁸ + x − w)).
2a ∈ p ⇒ a ∈ p in ℚ[x, y, z, w], 2 being a unit.
The x₂-chart of the blow-up of q has no point of order 2, at every prime:
∂_z(x²z − y²) = x² puts x in a prime containing D(K), and then
∂_z(z(x⁴z + 1 − w³x²)) = 2x⁴z + 1 − w³x² puts 1 in it.
The y₂-chart has no point of order 2: x³y²z − 1 ∈ D(K) and ∂_z(x³y²z − 1) = x³y² ∈ D(K),
so 1 ∈ D(K).
The z₂-chart has no point of order 2: ∂_z(x³z² − y²) = 2x³z gives x ∈ p or z ∈ p, and
∂_x(x⁴z⁴ + x − w³z²) = 4x³z⁴ + 1 then gives 1 ∈ p in either case.
On the w₂-chart a prime contains D(K_zw) iff it is the origin q': ∂_y(x³zw² − y²) = −2y,
∂_z(x³zw² − y²) = x³w², ∂_x(z(x⁴zw⁴ + x − w²)) = 4x³z²w⁴ + z and
∂_z(z(x⁴zw⁴ + x − w²)) = 2x⁴zw⁴ + x − w² put y, x, z, w in the prime (in the case w ∈ p of the
second derivative, x ∈ p follows from the fourth); conversely K_zw ⊆ 𝔪²
(ord_zero_example106_zw) gives D(K_zw) ⊆ 𝔪.
Off the w₂-chart, no prime of the blow-up of q has ord I₂ ≥ 2.
On the w₂-chart the order-2 locus of I₂ is the origin q', at every scheme point.
On the w₃-chart the origin q'' has ord I₃ ≥ 2 (ord_zero_example106_zww).
The order-2 run of BO_{4,2} has at least four blow-ups #
The z-chart of the blow-up of 𝔸⁴_ℚ at the origin; Kollár's q is its origin.
Equations
- One or more equations did not get rendered due to their size.
Instances For
On the z-chart the weak transform I₁ is V(K_z).
For any smooth blow-up sequence for (𝔸⁴_ℚ, I, E) of order 2 with no empty centre and final
maximal order < 2 (the three properties of the values of BO_{4,2}) that begins with the
blow-up of the origin, the tail has at least three blow-ups: the centres Z₁ ∋ q and Z₂ ∋ q' are
forced, and I₃ still has the point q'' of order 2. Stated for a centre J equal to
centerIdeal ℚ 4 4 so that 𝔪₀ may be passed.
Kollár's Example 106, continued: every smooth blow-up sequence for (𝔸⁴_ℚ, I, E) of order
2 with no empty centre and final maximal order < 2 has at least four blow-ups; the origin, q
and q' are forced as centres and q'' remains of order 2. Where [Kol07, Example 106] passes to
the mark 1 after the first blow-up ("the order has dropped to 1"), the order-2 run of BO_{4,2}
continues for at least three more blow-ups.