Transport of a protected closed subscheme along a blow-up sequence

In the isolation passage of the proof of [Wlo05, Theorem 4.7.1], once the strict transform of a component is isolated, the later blow-ups of the modified run leave it alone: each centre either misses it or is a stratum of the boundary transversal to it. This module carries a closed subscheme γ having simple normal crossings with the boundary, and contained in no member of it near any of its points, along a blow-up sequence whose every centre misses the strict transform of γ at its stage or is locally a stratum of the boundary at its stage (MissesOrStratum): at every stage the strict transform of γ has simple normal crossings with the total transform of the boundary, is contained in no member near any point, and is the pull-back of the ideal of γ along the stage map. The two cases are Hironaka.Resolution.Algebraic.Wlo05.OffCentreTransport (the centre misses γ) and the hypothesis StratumBlowUp (the stratum case; Hironaka.Resolution.Algebraic.Wlo05.EmbeddedHypotheses). Structural recursion on the sequence. Blow-up sequences of order ≥ m are those of [Kol07, Definition 66].

StratumBlowUp is not proved in this development, so protected_transport and smooth_strictTransformSeq_of_protected are CONDITIONAL lemmas; they are used by the conditional loop modules Hironaka.Resolution.Algebraic.Wlo05.EmbeddedState and Hironaka.Resolution.Algebraic.Wlo05.EmbeddedIsolatedState, not by the proof of the theorem, which reaches the same conclusions through CP4 and CP5 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP5).

def Hironaka.Resolution.MissesOrStratum {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (E : X.DivisorFamily) (γ : X.IdealSheafData) : Prop

The dichotomy of the isolation passage of the proof of [Wlo05, Theorem 4.7.1] for the centres of a sequence relative to a protected closed subscheme γ: every centre misses the strict transform of γ at its stage, or is locally a stratum of the boundary at its stage.

Equations

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

theorem Hironaka.Resolution.disjoint_strictTransformSeq_support_of_disjoint {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (γ γ' : X.IdealSheafData) (h : Disjoint γ.support γ'.support) (i : Fin (S.length + 1)) : Disjoint (S.strictTransformSeq γ i).support (S.strictTransformSeq γ' i).support

Disjoint closed subschemes have disjoint strict transforms at every stage (the strict transform maps into the closed subscheme below).

theorem Hironaka.Resolution.protected_transport {k : Type u} [Field k] [CharZero k] (hG : StratumBlowUp k) {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (f : X ⟶ AlgebraicGeometry.Spec ↧k) (E : X.DivisorFamily) (γ : X.IdealSheafData) : (∀ (i : Fin (S.length + 1)), AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.stageMap i) f)) → E.IsSnc → (∀ (i : Fin S.length), (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i)) → MissesOrStratum S E γ → E.HasSncWith γ → NotContainedInMembers E γ → ∀ (i : Fin (S.length + 1)), (S.totalTransformSeq E i).HasSncWith (S.strictTransformSeq γ i) ∧ NotContainedInMembers (S.totalTransformSeq E i) (S.strictTransformSeq γ i) ∧ γ.comap (S.stageMap i) = S.strictTransformSeq γ i

The protected transport, conditional on the hypothesis StratumBlowUp: along a sequence of smooth stages whose centres have simple normal crossings with the boundary and satisfy the dichotomy for γ, the strict transform of γ at every stage has simple normal crossings with the total transform of the boundary, is contained in no member of it near any point, and is the pull-back of the ideal of γ along the stage map (the isolation passage of the proof of [Wlo05, Theorem 4.7.1]).

theorem Hironaka.Resolution.smooth_strictTransformSeq_of_protected {k : Type u} [Field k] [CharZero k] (hG : StratumBlowUp k) {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (f : X ⟶ AlgebraicGeometry.Spec ↧k) (E : X.DivisorFamily) (γ : X.IdealSheafData) (hsm : ∀ (i : Fin (S.length + 1)), AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.stageMap i) f)) (hE : E.IsSnc) (hcen : ∀ (i : Fin S.length), (S.totalTransformSeq E i.castSucc).HasSncWith (S.center i)) (hdich : MissesOrStratum S E γ) (hγ : E.HasSncWith γ) (hno : NotContainedInMembers E γ) (i : Fin (S.length + 1)) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (S.strictTransformSeq γ i).subschemeι (CategoryTheory.CategoryStruct.comp (S.stageMap i) f))

The protected strict transform is smooth over k at every stage (a subvariety with simple normal crossings with E is smooth, [Kol07, Definition 24]; HasSncWith.smooth), conditional on StratumBlowUp.