Dimension 0: the base of the induction on the dimension

[Kol07, 70] starts the induction with the case dim X = 0, where I = 𝒪_X since I is nonzero on every irreducible component and "everything is resolved without blow-ups". A triple of dimension ≤ 0 (HasDimLE 0) has an étale structure morphism, its stalks are fields (AlgebraicGeometry.isField_stalk_of_smoothOfRelativeDimension_zero), so the stalk ideal of I — nonzero by [Kol07, Notation 64 (2)], the field Triple.isNonzeroEverywhere — is the unit ideal at every point: I = ⊤. The unit ideal has maximal order 0, and a smooth blow-up sequence of order m ≥ 1 (or ≥ m for a marked triple with mark ≥ 1) without empty blow-ups is then the empty sequence (Hironaka.BO.eq_nil_of_isOrderSeq_of_maxOrd_lt, AlgebraicGeometry.eq_nil_of_isOrderGeSeq_of_maxOrd_lt). Hence EVERY functor of the two types takes the value nil on a triple of dimension ≤ 0 — the base of the coherence induction (Hironaka.Resolution.Algebraic.Stage.Coherence): at stage n' = 0 both stage functors agree because both are empty. The lemmas hold unconditionally, over ANY field.

theorem AlgebraicGeometry.Triple.I_eq_top_of_hasDimLE_zero {k : Type u} [Field k] (T : Triple k) (h : T.HasDimLE 0) : T.I = ⊤

The base case of [Kol07, 70]: on a triple of dimension ≤ 0 the stalks are fields, so an ideal nonzero on every component ([Kol07, Notation 64 (2)]) is the unit ideal.

theorem Hironaka.OrderSeqAssignment.seq_eq_nil_of_hasDimLE_zero {k : Type u} [Field k] {m : ℕ} {Dom : AlgebraicGeometry.Triple k → Prop} (B : OrderSeqAssignment k m Dom) (T : AlgebraicGeometry.Triple k) (hT : Dom T) (h0 : T.HasDimLE 0) (hm : 1 ≤ m) : B.seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

The base case of [Kol07, 70]: on a triple of dimension ≤ 0 every blow-up sequence functor of order m ≥ 1 takes the value nil — "everything is resolved without blow-ups": the ideal is the unit ideal, of maximal order 0 < m, and a sequence of order m without empty blow-ups for it is empty.

theorem Hironaka.OrderGeSeqAssignment.seq_eq_nil_of_hasDimLE_zero {k : Type u} [Field k] {Dom : MarkedTriple k → Prop} (B : OrderGeSeqAssignment k Dom) (T : MarkedTriple k) (hT : Dom T) (h0 : T.HasDimLE 0) (hm : 1 ≤ T.m) : B.seq T hT = AlgebraicGeometry.Scheme.BlowUpSequence.nil T.X.left

The base case of [Kol07, 70] for marked functors: on a marked triple of dimension ≤ 0 with mark ≥ 1 every marked blow-up sequence functor takes the value nil (eq_nil_of_isOrderGeSeq_of_maxOrd_lt).