Kollár's Example 28.1: local blow-up sequences that do not glue

[Kol07, Example 28.1]: X a smooth threefold, C₁, C₂ irreducible curves meeting at two points p₁, p₂, Cᵢ smooth away from pᵢ where it has a cusp transversal to the other curve; on U₁ = X ∖ {p₁} one blows up C₁ first, on U₂ = X ∖ {p₂} C₂ first; over U₁ ∩ U₂, where the two curves are disjoint, both local sequences blow up the same two curves, in opposite orders, and no rule says which to blow up first. This file places local models on X = 𝔸³_k: p₁ = (0, 0, 0), p₂ = (1, 0, 0), C₁ = V(z, y² − x³) (a cuspidal curve near p₁), C₂ = V(y, z² − (x − 1)³) (near p₂). On 𝔸³ these two curves are disjoint (z = y = 0 forces x = 0 and x = 1): the file does not model Kollár's global configuration (curves meeting at p₁, p₂ with transversal cusps, the end results gluing to a locally but not globally projective Y); the disjoint model suffices for the failure of the gluing condition (37.1) of [Kol07, Proposition 37] (the first centres of the local sequences agree on the overlaps), which is Kollár's own diagnosis. The examples instantiate the mechanism of HironakaExamples/Sequence/Prop37Constraints.lean: the first centres C₁|_{U₁}, C₂|_{U₂} of the two local sequences differ on the overlap U₁ ×_X U₂ (the point q = (4, 8, 0) of U₁ ∩ U₂ lies on C₁ and not on C₂), so, whatever the continuations, no blow-up sequence on X restricts to both (not_exists_pullback_eq_of_center_ne), and (37.1) is the condition violated. The examples show that these two first centres do not glue; that the rule "blow up the smooth curve first" selects them (smoothness of C₁ on U₁, the cusp of C₂ at p₂) is not proved here.

@[reducible, inline]

abbrev Hironaka.Sequence.Examples.Example28.Poly (k : Type) [Field k] : Type

The coordinate ring k[x, y, z], with x = X 0, y = X 1, z = X 2.

Equations

• Hironaka.Sequence.Examples.Example28.Poly k = MvPolynomial (Fin 3) k

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.A3 (k : Type) [Field k] : AlgebraicGeometry.Scheme

The affine space 𝔸³_k.

Equations

• Hironaka.Sequence.Examples.Example28.A3 k = AlgebraicGeometry.Spec ↧(Hironaka.Sequence.Examples.Example28.Poly k)

noncomputable def Hironaka.Sequence.Examples.Example28.vanishing (k : Type) [Field k] (I : Ideal (Poly k)) : (A3 k).IdealSheafData

The ideal sheaf of the closed subscheme V(I) ⊆ 𝔸³_k.

Equations

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

noncomputable def Hironaka.Sequence.Examples.Example28.idealC₁ (k : Type) [Field k] : Ideal (Poly k)

C₁ = V(z, y² − x³): the cuspidal model near p₁ = (0, 0, 0) (its singularity at p₁ and smoothness elsewhere are not proved here).

Equations

• Hironaka.Sequence.Examples.Example28.idealC₁ k = Ideal.span {MvPolynomial.X 2, MvPolynomial.X 1 ^ 2 - MvPolynomial.X 0 ^ 3}

noncomputable def Hironaka.Sequence.Examples.Example28.idealC₂ (k : Type) [Field k] : Ideal (Poly k)

C₂ = V(y, z² − (x − 1)³): the cuspidal model near p₂ = (1, 0, 0) (its singularity at p₂ and smoothness elsewhere are not proved here).

Equations

• Hironaka.Sequence.Examples.Example28.idealC₂ k = Ideal.span {MvPolynomial.X 1, MvPolynomial.X 2 ^ 2 - (MvPolynomial.X 0 - 1) ^ 3}

theorem Hironaka.Sequence.Examples.Example28.eval_surjective (k : Type) [Field k] (v : Fin 3 → k) : Function.Surjective ⇑(MvPolynomial.eval v)

noncomputable def Hironaka.Sequence.Examples.Example28.pt (k : Type) [Field k] (v : Fin 3 → k) : ↥(A3 k)

The k-point of 𝔸³_k with coordinates v: the maximal ideal ker (eval v).

Equations

• Hironaka.Sequence.Examples.Example28.pt k v = { asIdeal := RingHom.ker (MvPolynomial.eval v), isPrime := ⋯ }

theorem Hironaka.Sequence.Examples.Example28.isMaximal_pt (k : Type) [Field k] (v : Fin 3 → k) : (pt k v).asIdeal.IsMaximal

theorem Hironaka.Sequence.Examples.Example28.mem_pt_iff (k : Type) [Field k] (v : Fin 3 → k) (f : Poly k) : f ∈ (pt k v).asIdeal ↔ (MvPolynomial.eval v) f = 0

theorem Hironaka.Sequence.Examples.Example28.mem_support_vanishing_iff (k : Type) [Field k] (I : Ideal (Poly k)) (x : ↥(A3 k)) : x ∈ (vanishing k I).support ↔ I ≤ x.asIdeal

A point of 𝔸³_k lies on V(I) iff I is contained in its prime ideal.

def Hironaka.Sequence.Examples.Example28.openCompl (k : Type) [Field k] (p : ↥(A3 k)) (hp : p.asIdeal.IsMaximal) : (A3 k).Opens

The open subscheme X ∖ {p} for a closed point p.

Equations

• Hironaka.Sequence.Examples.Example28.openCompl k p hp = { carrier := {p}ᶜ, is_open' := ⋯ }

theorem Hironaka.Sequence.Examples.Example28.mem_openCompl_iff (k : Type) [Field k] (p : ↥(A3 k)) (hp : p.asIdeal.IsMaximal) (x : ↥(A3 k)) : x ∈ openCompl k p hp ↔ x ≠ p

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.p₁ (k : Type) [Field k] : ↥(A3 k)

p₁ = (0, 0, 0).

Equations

• Hironaka.Sequence.Examples.Example28.p₁ k = Hironaka.Sequence.Examples.Example28.pt k ![0, 0, 0]

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.p₂ (k : Type) [Field k] : ↥(A3 k)

p₂ = (1, 0, 0).

Equations

• Hironaka.Sequence.Examples.Example28.p₂ k = Hironaka.Sequence.Examples.Example28.pt k ![1, 0, 0]

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.q (k : Type) [Field k] : ↥(A3 k)

The witness point q = (4, 8, 0): on C₁ (8² = 4³), not on C₂ (y = 8 ≠ 0).

Equations

• Hironaka.Sequence.Examples.Example28.q k = Hironaka.Sequence.Examples.Example28.pt k ![4, 8, 0]

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.U₁ (k : Type) [Field k] : (A3 k).Opens

U₁ = X ∖ {p₁}.

Equations

• Hironaka.Sequence.Examples.Example28.U₁ k = Hironaka.Sequence.Examples.Example28.openCompl k (Hironaka.Sequence.Examples.Example28.p₁ k) ⋯

@[reducible, inline]

noncomputable abbrev Hironaka.Sequence.Examples.Example28.U₂ (k : Type) [Field k] : (A3 k).Opens

U₂ = X ∖ {p₂}.

Equations

• Hironaka.Sequence.Examples.Example28.U₂ k = Hironaka.Sequence.Examples.Example28.openCompl k (Hironaka.Sequence.Examples.Example28.p₂ k) ⋯

theorem Hironaka.Sequence.Examples.Example28.pt_ne_of_eval_ne (k : Type) [Field k] {v w : Fin 3 → k} (f : Poly k) (hv : (MvPolynomial.eval v) f = 0) (hw : (MvPolynomial.eval w) f ≠ 0) : pt k v ≠ pt k w

Two k-points with different coordinates are different points (a polynomial separates them).

theorem Hironaka.Sequence.Examples.Example28.q_ne_p₁ (k : Type) [Field k] [CharZero k] : q k ≠ p₁ k

theorem Hironaka.Sequence.Examples.Example28.q_ne_p₂ (k : Type) [Field k] [CharZero k] : q k ≠ p₂ k

theorem Hironaka.Sequence.Examples.Example28.q_mem_C₁ (k : Type) [Field k] : q k ∈ (vanishing k (idealC₁ k)).support

q ∈ C₁.

theorem Hironaka.Sequence.Examples.Example28.q_not_mem_C₂ (k : Type) [Field k] [CharZero k] : q k ∉ (vanishing k (idealC₂ k)).support

q ∉ C₂.

theorem Hironaka.Sequence.Examples.Example28.center_ne (k : Type) [Field k] [CharZero k] : ((vanishing k (idealC₁ k)).comap (U₁ k).ι).comap (CategoryTheory.Limits.pullback.fst (U₁ k).ι (U₂ k).ι) ≠ ((vanishing k (idealC₂ k)).comap (U₂ k).ι).comap (CategoryTheory.Limits.pullback.snd (U₁ k).ι (U₂ k).ι)

The first centres of the two local sequences differ on the overlap U₁ ×_X U₂: the point q lies on C₁ and not on C₂.

noncomputable def Hironaka.Sequence.Examples.Example28.piece (k : Type) [Field k] : Bool → AlgebraicGeometry.Scheme

The two-piece cover {U₁, U₂} of 𝔸³_k, indexed by Bool.

Equations

• Hironaka.Sequence.Examples.Example28.piece k true = ↑(Hironaka.Sequence.Examples.Example28.U₁ k)
• Hironaka.Sequence.Examples.Example28.piece k false = ↑(Hironaka.Sequence.Examples.Example28.U₂ k)

noncomputable def Hironaka.Sequence.Examples.Example28.incl (k : Type) [Field k] (b : Bool) : piece k b ⟶ A3 k

The inclusions of the pieces.

Equations

• Hironaka.Sequence.Examples.Example28.incl k true = (Hironaka.Sequence.Examples.Example28.U₁ k).ι
• Hironaka.Sequence.Examples.Example28.incl k false = (Hironaka.Sequence.Examples.Example28.U₂ k).ι

instance Hironaka.Sequence.Examples.Example28.instIsOpenImmersionIncl (k : Type) [Field k] (b : Bool) : AlgebraicGeometry.IsOpenImmersion (incl k b)

noncomputable def Hironaka.Sequence.Examples.Example28.localSeq (k : Type) [Field k] (r₁ : ((vanishing k (idealC₁ k)).comap (U₁ k).ι).blowUp.BlowUpSequence) (r₂ : ((vanishing k (idealC₂ k)).comap (U₂ k).ι).blowUp.BlowUpSequence) (b : Bool) : (piece k b).BlowUpSequence

The two local sequences with the first centres the rule "blow up the smooth curve first" is meant to select: C₁|_{U₁} on U₁, C₂|_{U₂} on U₂, with arbitrary continuations r₁, r₂ (the selection itself is not proved here).

Equations

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