Warning 63 on the model of Remark 33

On 𝔸³_k with the origin p = V(x, y, z) and the z-axis C = V(x, y), Kollár compares the marked transforms of (I_C, 1) along the two sequences of [Kol07, Remark 33]: Π (blow up p, then the strict transform of C) and Σ (blow up C, then D = σ_0^{-1}(p)), and finds Π_*^{-1}(I_C, 1) ≠ Σ_*^{-1}(I_C, 1) although Π = Σ [Kol07, Warning 63]. With the marked transform defined as the colon ideal π_*^{-1}(J, m) = (π^* J : F^m), the computation along Σ is immediate: σ_0^* I_C is the exceptional divisor E_0' itself, so (σ_0)_*^{-1}(I_C, 1) = (E_0' : E_0') = 𝒪, and the transform of (𝒪, 1) under any blow-up is (𝒪 : F) = 𝒪. Kollár's printed value 𝒪(E_0' + 2E_1') · Σ^* I_C = 𝒪(E_1') is a fractional ideal: Definition 60 is applied with ord_D 𝒪 = 0 < 1, outside its domain m ≤ ord_Z I, which is exactly why Σ is not a sequence of order ≥ 1 for (𝔸³, I_C, 1, ∅) while Π is (not_isOrderGeSeq_seqCurvePoint in HironakaExamples/Sequence/Remark33Warning63.lean). The two processes with the same end result are told apart by the marked ideals they induce.

The model sequences are defined in HironakaExamples/Sequence/Remark33Model.lean.

The two general facts used, markedTransform_self and markedTransform_top, are in the library module Hironaka/Resolution/Algebraic/Kol07/Warning63.lean.

theorem Hironaka.Sequence.markedTransformSeq_seqCurvePoint_one (k : Type u) [Field k] : (Remark33.seqCurvePoint k).markedTransformSeq (Remark33.curve k) 1 ⟨1, ⋯⟩ = ⊤

The first step of Σ: (σ_0)_*^{-1}(I_C, 1) = 𝒪, since σ_0^* I_C = E_0' [Kol07, Warning 63].

theorem Hironaka.Sequence.markedTransformSeq_seqCurvePoint (k : Type u) [Field k] : (Remark33.seqCurvePoint k).markedTransformSeq (Remark33.curve k) 1 (Fin.last 2) = ⊤

The end of Σ: Σ_*^{-1}(I_C, 1) = 𝒪, the transform of (𝒪, 1) [Kol07, Warning 63].