Assignments of successions of blow-ups

The data of the functors that the proofs of Kollár's Theorem 36 and of Włodarczyk's Theorem 1.0.2 construct (Hironaka.Resolution.BRFunctor, Hironaka.Resolution.EDFunctor): a succession of blow-ups for every input, with no conditions. The statements of the theorems use AlgebraicGeometry.BlowUpSequenceFunctor (Hironaka.Scheme.Resolution.Defs); these unbundled forms are the ones the constructions are written in.

structure AlgebraicGeometry.ResolutionAssignment (k : Type u) [Field k] : Type (u + 1)

A resolution functor on all algebraic k-schemes [Kol07, Theorem 36]: an assignment of a succession of monoidal transformations BR(X) to every scheme of finite type over Spec k (separated, as every scheme of this library). The resolution functor Hironaka.Resolution.BRFunctor is one; the statement of the theorem uses AlgebraicGeometry.BlowUpSequenceFunctor.

• seq (X : Scheme) [X.Over (Spec ↧k)] [FiniteType (X ↘ Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] : X.BlowUpSequence

  The succession BR(X).

structure AlgebraicGeometry.EmbeddedDesingularizationAssignment (k : Type u) [Field k] : Type (u + 1)

An embedded desingularization assignment [Wlo05, Theorem 1.0.2]: a succession of monoidal transformations of the smooth ambient X for every closed subscheme Y ⊆ X (given by its ideal sheaf). The embedded desingularization functor Hironaka.Resolution.EDFunctor is one; the statement of the theorem, AlgebraicGeometry.exists_functorial_embeddedDesingularization, uses AlgebraicGeometry.BlowUpSequenceFunctor on embedded pairs.

• seq (X : Scheme) [X.Over (Spec ↧k)] [FiniteType (X ↘ Spec ↧k)] [IsSeparated (X ↘ Spec ↧k)] [Smooth (X ↘ Spec ↧k)] : X.IdealSheafData → X.BlowUpSequence

  The succession assigned to Y ⊆ X.