The base stage: dimension zero #

[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 has I = ⊤ (Triple.I_eq_top_of_hasDimLE_zero, Hironaka.Resolution.Algebraic.Stage.DimZero), so the functors BO_{0,m} and BMO_{0,m} are the empty sequence nil on their classes: clause (1) of Theorems 68 and 69 holds since max-ord 𝒪_X = 0 < m for a mark m ≥ 1, and functoriality (both bullets of [Kol07, 34.1]), change of fields Kol07, 34.2 and the indifference to empty boundary members are the identities nil = nil (pullback_nil, eraseEmpty_nil, both rfl). stage0 packages these data; it is the base of the tower of stages (Hironaka.Stage.tower, whose base is a parameter), and HironakaExamples.Stage.BaseCases shows that it is the ONLY stage-0 package.

source

noncomputable def Hironaka.Stage.boZeroFunctor (m : ℕ) (k : Type u) [Field k] :

OrderSeqAssignment k m (AlgebraicGeometry.Triple.BOClass 0 m)

The functor BO_{0,m}: the empty blow-up sequence on every triple of dimension ≤ 0 ("everything is resolved without blow-ups", [Kol07, 70]).

Equations

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

Instances For

source

noncomputable def Hironaka.Stage.boZero (m : ℕ) :

BOData 0 m

The data of BO_{0,m} ([Kol07, Theorem 68] at dimension 0, [Kol07, 70]): the nil functor on the triples of dimension ≤ 0; clause (1) because such a triple has I = 𝒪_X (Triple.I_eq_top_of_hasDimLE_zero) of maximal order 0 < m, and the two functoriality clauses because nil pulls back to nil.

Equations

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

Instances For

source

noncomputable def Hironaka.Stage.bmoZeroFunctor (m : ℕ) (k : Type u) [Field k] :

OrderGeSeqAssignment k (MarkedTriple.BMOClass 0 m)

The functor BMO_{0,m}: the empty blow-up sequence on every marked triple of dimension ≤ 0 ([Kol07, 70]).

Equations

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

Instances For

source

noncomputable def Hironaka.Stage.bmoZero (m : ℕ) :

BMOData 0 m

The data of BMO_{0,m} ([Kol07, Theorem 69] at dimension 0, [Kol07, 70]): the nil functor on the marked triples of dimension ≤ 0 and mark m; clause (1) because I = 𝒪_X there, the functoriality clauses and the indifference to empty boundary members because nil pulls back to nil and does not see the boundary.

Equations

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

Instances For

source

noncomputable def Hironaka.Stage.stage0 :

OrderReductionStage 0

The base stage stage0 : OrderReductionStage 0 ([Kol07, 70]): BO_{0,m} and BMO_{0,m} for every mark m, both the empty sequence; the base of the tower Hironaka.Stage.tower stage0 from which the functors of Theorems 68 and 69 are built (Hironaka.Resolution.Algebraic.Stage.Theorem68).

Equations