The state of the loop and its end result

Włodarczyk proves the clauses of [Wlo05, Theorem 4.7.1] (the strict transforms of the components smooth and disjoint, the full transform of I_Y its monomial part times I_Ỹ) by an invariant carried along the passes of the modified run. Here the invariant is a predicate on the state (X, I, E, C, Γ) of the loop BED (Hironaka.Resolution.Algebraic.Wlo05.Embedded) — the members C still to be absorbed and the protected components Γ already isolated:

• EmbeddedStateData: the invariant InvCE for the members (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses); each protected component has simple normal crossings with the boundary and is contained in no member near any point; the protected components are pairwise disjoint and disjoint from the members; and the nonmonomial part of the marked ideal is trivial along them;
• EmbeddedEndData and EmbeddedEnd: what holds at the end of the loop on that state — the final marked transform of I is the product of the final strict transforms of the members (I_r = I_Ỹ, the content of σ^*(I_Y) = M(σ^*(I_Y)) · I_Ỹ in [Wlo05, Theorem 4.7.1] once the monomial factor of [Kol07, 72] is supplied), each protected component's ideal pulls back to its strict transform, every final strict transform has simple normal crossings with the final boundary, and they are pairwise disjoint.

The definitions are used by the proof of the theorem (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCPBridge, Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEndBridge). The theorems of this module — the dichotomy for a run of BMO_1 from the hypothesis CentersInNonmonomialSupportOrStratum, the protected transport along the run from StratumBlowUp, and the base case of the loop embeddedEnd_bmoOneRun (a run of BMO_1 with no member left: the protected transport along the whole run, and I_r = 𝒪 at the end of the run by [Kol07, Theorem 69 (1)]) — are CONDITIONAL on those two unproved hypotheses and are not used by the proof of the theorem.

structure Hironaka.Resolution.EmbeddedStateData {Y : AlgebraicGeometry.Scheme} (I : Y.IdealSheafData) (E : Y.DivisorFamily) (C Γ : Finset Y.IdealSheafData) : Prop

The state of the loop (I, E, C, Γ) (the invariant of the proof of [Wlo05, Theorem 4.7.1]): the members C satisfy InvCE; every protected component γ ∈ Γ has simple normal crossings with the boundary and is contained in no member near any of its points; the protected components are pairwise disjoint and disjoint from the members; and the nonmonomial part of I is trivial along them.

• invCE : InvCE I E C
• snc (γ : Y.IdealSheafData) : γ ∈ Γ → E.HasSncWith γ
• notContained (γ : Y.IdealSheafData) : γ ∈ Γ → NotContainedInMembers E γ
• pairwise : (↑Γ).Pairwise fun (a b : Y.IdealSheafData) => Disjoint a.support b.support
• disjointCΓ (c : Y.IdealSheafData) : c ∈ C → ∀ γ ∈ Γ, Disjoint c.support γ.support
• nonmonomial (γ : Y.IdealSheafData) : γ ∈ Γ → Disjoint (BMO.nonmonomialPart I E).support γ.support

structure Hironaka.Resolution.EmbeddedEndData {Y Yend : AlgebraicGeometry.Scheme} (Eend : Yend.DivisorFamily) (Iend : Yend.IdealSheafData) (zEnd cEnd : Y.IdealSheafData → Yend.IdealSheafData) (C Γ : Finset Y.IdealSheafData) : Prop

The conclusions of [Wlo05, Theorem 4.7.1] at the end of the loop on a state, on the end data — the final boundary Eend, the final marked transform Iend, the final strict transform zEnd z of a closed subscheme z, and the pull-back cEnd z of its ideal along the composite: Iend is the product of the members' final strict transforms, each protected component pulls back to its strict transform, the final strict transforms of members and protected components have simple normal crossings with the final boundary, and they are pairwise disjoint.

• marked_eq : Iend = ∏ c ∈ C, zEnd c
• comap_eq (γ : Y.IdealSheafData) : γ ∈ Γ → cEnd γ = zEnd γ
• snc (z : Y.IdealSheafData) : z ∈ C ∪ Γ → Eend.HasSncWith (zEnd z)
• pairwise : (↑(C ∪ Γ)).Pairwise fun (a b : Y.IdealSheafData) => Disjoint (zEnd a).support (zEnd b).support

def Hironaka.Resolution.EmbeddedEnd {k : Type u} [Field k] (T : MarkedTriple k) (C Γ : Finset T.X.left.IdealSheafData) (S : T.X.left.BlowUpSequence) : Prop

EmbeddedEndData at the end of a blow-up sequence S on the marked triple T.

Equations

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

theorem Hironaka.Resolution.EmbeddedStateData.of_heq {Y Y' : AlgebraicGeometry.Scheme} (h : Y = Y') {I : Y.IdealSheafData} {I' : Y'.IdealSheafData} {E : Y.DivisorFamily} {E' : Y'.DivisorFamily} {C Γ : Finset Y.IdealSheafData} {C' Γ' : Finset Y'.IdealSheafData} (hI : I ≍ I') (hE : E ≍ E') (hC : C ≍ C') (hΓ : Γ ≍ Γ') (hs : EmbeddedStateData I' E' C' Γ') : EmbeddedStateData I E C Γ

The state transports across a cast of the ambient scheme.

theorem Hironaka.Resolution.EmbeddedEndData.of_heq {Y Yend Yend' : AlgebraicGeometry.Scheme} (h : Yend = Yend') {Eend : Yend.DivisorFamily} {Eend' : Yend'.DivisorFamily} {Iend : Yend.IdealSheafData} {Iend' : Yend'.IdealSheafData} {zEnd cEnd : Y.IdealSheafData → Yend.IdealSheafData} {zEnd' cEnd' : Y.IdealSheafData → Yend'.IdealSheafData} (hE : Eend ≍ Eend') (hI : Iend ≍ Iend') (hz : zEnd ≍ zEnd') (hc : cEnd ≍ cEnd') {C Γ : Finset Y.IdealSheafData} (hs : EmbeddedEndData Eend' Iend' zEnd' cEnd' C Γ) : EmbeddedEndData Eend Iend zEnd cEnd C Γ

The end data transport across a cast of the end scheme.

theorem Hironaka.Resolution.missesOrStratum_bmoOneRun {k : Type u} [Field k] [CharZero k] (hL : CentersInNonmonomialSupportOrStratum k) (T : MarkedTriple k) (hm : T.m = 1) {γ : T.X.left.IdealSheafData} (hγ : Disjoint (BMO.nonmonomialPart T.I T.E).support γ.support) : MissesOrStratum (bmoOneRun T hm) T.E γ

The dichotomy of the isolation passage for a run of BMO_1, from the hypothesis CentersInNonmonomialSupportOrStratum: a closed subscheme along which the nonmonomial part of the marked ideal is trivial is missed by every centre lying in the nonmonomial support, the other centres being strata.

theorem Hironaka.Resolution.EmbeddedStateData.protected_transport_bmoOneRun {k : Type u} [Field k] [CharZero k] (hG : StratumBlowUp k) (hL : CentersInNonmonomialSupportOrStratum k) {T : MarkedTriple k} {hm : T.m = 1} {C Γ : Finset T.X.left.IdealSheafData} (hs : EmbeddedStateData T.I T.E C Γ) {γ : T.X.left.IdealSheafData} (hγ : γ ∈ Γ) (i : Fin ((bmoOneRun T hm).length + 1)) : ((bmoOneRun T hm).totalTransformSeq T.E i).HasSncWith ((bmoOneRun T hm).strictTransformSeq γ i) ∧ NotContainedInMembers ((bmoOneRun T hm).totalTransformSeq T.E i) ((bmoOneRun T hm).strictTransformSeq γ i) ∧ γ.comap ((bmoOneRun T hm).stageMap i) = (bmoOneRun T hm).strictTransformSeq γ i

The protected transport along a run of BMO_1 on a state (conditional on StratumBlowUp and CentersInNonmonomialSupportOrStratum): the strict transform of every protected component has simple normal crossings with the boundary at every stage, is contained in no member, and is the pull-back of the ideal of the component.

theorem Hironaka.Resolution.embeddedEnd_bmoOneRun {k : Type u} [Field k] [CharZero k] (hG : StratumBlowUp k) (hL : CentersInNonmonomialSupportOrStratum k) (T : MarkedTriple k) (hm : T.m = 1) (Γ : Finset T.X.left.IdealSheafData) (hs : EmbeddedStateData T.I T.E ∅ Γ) : EmbeddedEnd T ∅ Γ (bmoOneRun T hm)

The base case of the loop (conditional on StratumBlowUp and CentersInNonmonomialSupportOrStratum): on a state with no member left, the run of BMO_1 ends with the unit marked ideal ([Kol07, Theorem 69 (1)] at the mark 1), and the protected components pull back to their strict transforms, which have simple normal crossings with the final boundary and are pairwise disjoint.