The nonmonomial round: the weak transform of N(I) is the nonmonomial part

Step 1 of the proof of [Kol07, Theorem 107] (item 111, Step 1) applies order reduction to the nonmonomial part N(I); Kollár notes that the two birational transforms (Π₁)⁻¹_* N(I) and (Π₁)⁻¹_*(I, m) differ only in their monomial part, by an ideal sheaf of exceptional divisors of Π₁, whence N((Π₁)⁻¹_*(I, m)) = (Π₁)⁻¹_* N(I). Hironaka.Resolution.Algebraic.MarkedOrderReduction.Step1NonmonomialPart has the one-step identity nonmonomialPart_markedTransform_eq_weakTransform and the end identity with N on both sides. The proof of the statement CP3 of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative) along Step 1 needs the identity at every stage, with the weak transform itself on the left. This requires in addition that the weak transform of N(I) has the unit ideal as monomial part, i.e. order 0 along every member of the induced families: along the strict transforms of the old members because a member of order 0 is off the centre and the blow-up is an isomorphism there, and along the exceptional divisors because the pulled-back order at a generic point of the exceptional divisor is the order at the generic point of the component of the centre ([Kol07, Definition 47], the multiplicity of the pullback along the exceptional divisor; the weak transform of [Kol07, 58]), which is exactly d for a sequence of order d (IsOrderSeq); both facts are in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Exceptional. This module holds the recursion (ord_weakTransformSeq_eq_zero_of_mem_genericPoints), the vanishing of the monomial part (nonmonomialPart_eq_self_of_forall_ord_eq_zero, from [Kol07, Definition–Lemma 110]) and the identity in its triple form (weakTransformSeq_eq_nonmonomialPart_markedTransformSeq). Used in Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP3Step1.

theorem Hironaka.Resolution.nonmonomialPart_eq_self_of_forall_ord_eq_zero {X : AlgebraicGeometry.Scheme} (E : X.DivisorFamily) (J : X.IdealSheafData) (hJE : ∀ (j : E.ι), ∀ ξ ∈ (E.component j).support.genericPoints, J.ord ξ = 0) : BMO.nonmonomialPart J E = J

An ideal of order 0 along every member of E has the unit ideal as monomial part and is its own nonmonomial part ([Kol07, Definition–Lemma 110]).

theorem Hironaka.Resolution.ord_weakTransformSeq_eq_zero_of_mem_genericPoints_aux {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {J : X.IdealSheafData} {E : X.DivisorFamily} {d : ℕ} : S.IsOrderSeq f J E d → (∀ (j : E.ι), ∀ ξ ∈ (E.component j).support.genericPoints, J.ord ξ = 0) → ∀ (i : Fin (S.length + 1)) (j : (S.totalTransformSeq E i).ι) {ε : ↥(S.stage i)}, ε ∈ ((S.totalTransformSeq E i).component j).support.genericPoints → (S.weakTransformSeq J i).ord ε = 0

The recursion: along a sequence of order d for J with J of order 0 along every member, the weak transforms have order 0 along every member of the induced families. By structural recursion on the sequence, the Noetherian instance carried explicitly (through isNoetherian_of_field on the blow-up); at a stage i + 1 a member is a strict transform of a member of the previous stage (ord_weakTransform_eq_zero_of_mem_genericPoints_strictTransform) or the exceptional divisor of the previous blow-up (ord_weakTransform_eq_zero_of_mem_genericPoints_exceptionalDivisor, the order along the centre being exactly d by IsOrderSeq).

theorem Hironaka.Resolution.ord_weakTransformSeq_eq_zero_of_mem_genericPoints {k : Type u} [Field k] [CharZero k] {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian X] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {J : X.IdealSheafData} {E : X.DivisorFamily} {d : ℕ} (hS : S.IsOrderSeq f J E d) (hJE : ∀ (j : E.ι), ∀ ξ ∈ (E.component j).support.genericPoints, J.ord ξ = 0) (i : Fin (S.length + 1)) (j : (S.totalTransformSeq E i).ι) {ε : ↥(S.stage i)} (hε : ε ∈ ((S.totalTransformSeq E i).component j).support.genericPoints) : (S.weakTransformSeq J i).ord ε = 0

The Fin form of the recursion ord_weakTransformSeq_eq_zero_of_mem_genericPoints_aux.

theorem Hironaka.Resolution.weakTransformSeq_eq_nonmonomialPart_markedTransformSeq_aux {k : Type u} [Field k] [CharZero k] (l : ℕ) (T : MarkedTriple k) (S : T.X.left.BlowUpSequence) : S.length = l → ∀ {d : ℕ}, S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (BMO.nonmonomialPart T.I T.E) T.E d → S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I T.m T.E → ∀ (i : Fin (S.length + 1)), S.weakTransformSeq (BMO.nonmonomialPart T.I T.E) i = BMO.nonmonomialPart (S.markedTransformSeq T.I T.m i) (S.totalTransformSeq T.E i)

The recursion behind weakTransformSeq_eq_nonmonomialPart_markedTransformSeq, by induction on the length, the marked triple advancing through blowUpTriple: one step is nonmonomialPart_markedTransform_eq_weakTransform together with the vanishing of the monomial part at the generic points of the induced family (through ord_nonmonomialPart_eq_zero), the structure map of the blown-up triple being blowUpπ ≫ (T.X.left ↘ Spec k).

theorem Hironaka.Resolution.weakTransformSeq_eq_nonmonomialPart_markedTransformSeq {k : Type u} [Field k] [CharZero k] (T : MarkedTriple k) (hm : T.m = 1) {S : T.X.left.BlowUpSequence} {d : ℕ} (hS : S.IsOrderSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) (BMO.nonmonomialPart T.I T.E) T.E d) (hI : S.IsOrderGeSeq (T.X.left ↘ AlgebraicGeometry.Spec ↧k) T.I 1 T.E) (i : Fin (S.length + 1)) : S.weakTransformSeq (BMO.nonmonomialPart T.I T.E) i = BMO.nonmonomialPart (S.markedTransformSeq T.I 1 i) (S.totalTransformSeq T.E i)

Along a round of order d for N(I) the birational transform of N(I) is the nonmonomial part of the marked transform of I at every stage ([Kol07, 111, Step 1]: N((Π₁)⁻¹_*(I, m)) = (Π₁)⁻¹_* N(I)), in the triple form.