Generalities on a marked triple and one smooth blow-up

Four facts about a marked triple (X, I, m, E) [Kol07, Notation 64] and one smooth blow-up that involve no monomial part: the power of the exceptional ideal at the exceptional order divides the total transform (pow_exceptionalOrderAlong_dvd, the multiplicity of π^* I along the exceptional divisor in [Kol07, 58]); on a triple's scheme the product of nonvanishing ideal sheaves is nonvanishing (isNonzeroEverywhere_mul); a smooth blow-up of order ≥ m for (X, I, m, E) is a smooth blow-up sequence of order ≥ m of length one (isOrderGeSeq_single, [Kol07, Definition 65, (1′)–(2′)]); the exceptional divisor is the last member of the total transform (support_exceptionalDivisor_le). They are used by the marked order reduction functor (Hironaka/Resolution/Algebraic/MarkedOrderReduction/), whose namespace Hironaka.BMO they share.

theorem AlgebraicGeometry.pow_exceptionalOrderAlong_dvd {B X : Scheme} (π : B ⟶ X) (F : B.IdealSheafData) (J : X.IdealSheafData) : F ^ exceptionalOrderAlong π F J ∣ J.comap π

The power of the exceptional ideal at the exceptional order divides the total transform: the set {c | F^c ∣ π^* J} is either all of ℕ or bounded, and a bounded nonempty set of naturals contains its supremum.

theorem AlgebraicGeometry.isNonzeroEverywhere_mul {k : Type u} [Field k] (T' : Triple k) {I J : T'.X.left.IdealSheafData} (hI : I.IsNonzeroEverywhere) (hJ : J.IsNonzeroEverywhere) : (I * J).IsNonzeroEverywhere

On a triple's scheme the product of two nonvanishing ideal sheaves is nonvanishing (the stalks are domains).

theorem AlgebraicGeometry.isOrderGeSeq_single {k : Type u} [Field k] (T : Hironaka.MarkedTriple k) (Z : T.X.left.IdealSheafData) (hZ : T.IsOrderGeBlowUp Z) : (Scheme.BlowUpSequence.cons T.X.left Z (Scheme.BlowUpSequence.nil Z.blowUp)).IsOrderGeSeq (T.X.left ↘ Spec ↧k) T.I T.m T.E

Conditions (1′)–(2′) of [Kol07, Definition 65] as the one-step sequence: a smooth blow-up of order ≥ m for (X, I, m, E) is a smooth blow-up sequence of order ≥ m of length one.

theorem AlgebraicGeometry.support_exceptionalDivisor_le {k : Type u} [Field k] (T : Hironaka.MarkedTriple k) (Z : T.X.left.IdealSheafData) : Z.exceptionalDivisor.support ≤ (T.E.totalTransform Z).support

The exceptional divisor is the last member of the total transform [Kol07, Definition 65].