Documentation

Hironaka.Resolution.Algebraic.Wlo05.EmbeddedGenericLift

The generic point of a strict transform before the first containing centre #

The hypothesis of Włodarczyk's Claim in the proof of [Wlo05, Theorem 4.7.1] — η a generic point of supp I on no member of the boundary at which I = I_{closure η} — transports along any stage i of a blow-up sequence before the first centre containing the strict transform of c = I_{closure η} (the proof of [Kol07, Corollary 22]): the strict transform at stage i is the reduced ideal of the closure of a point η' over η, η' is a generic point of the support of the marked transform of I, lies on no member of the total transform of the boundary, and the marked transform agrees with the strict transform at η'. This is the invariant GenericLift carried through the proof of CP1 (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedChainRelative): the hypotheses of CP1For for the triple induced at stage i with the member c̃_i, read off the corresponding hypotheses at stage 0. The round-by-round reading of the run of BMO_1 (Step 1 of the proof of [Kol07, Theorem 107]) applies it at the end of each round that never contains c̃. Used throughout the CP1 modules (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedCP1For, EmbeddedCP1Cover, EmbeddedCP1Step21, EmbeddedCP1Step22, …).

source
structure Hironaka.Resolution.GenericLift {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) (η : ↥X) (i : Fin (S.length + 1)) (η' : ↥(S.stage i)) :
Prop

The lift of the hypothesis of Włodarczyk's Claim to a stage — η' at stage i lies over η, the strict transform of c := vanishingIdeal (closure {η}) at stage i is vanishingIdeal (closure {η'}), η' is a generic point of the support of the marked transform of I (mark m), lies on no member of the total transform of E, the marked transform agrees with vanishingIdeal (closure {η'}) at η', η' lies over no earlier centre, and it is the only point of stage i over η.

Instances For
    source
    theorem Hironaka.Resolution.exists_genericLift {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (I : X.IdealSheafData) (E : X.DivisorFamily) (m : ℕ) {η : ↥X} (hη : η ∈ I.support.genericPoints) (hηE : ∀ (j : E.ι), η ∉ (E.component j).support) (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (i : Fin (S.length + 1)) (hi : ∀ l < ↑i, ¬CenterContains S (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) l) :
    ∃ (η' : ↥(S.stage i)), GenericLift S I E m η i η'

    If no centre before stage i contains the strict transform of c := vanishingIdeal (closure {η}), the lift exists (the proof of [Kol07, Corollary 22]: the strict transform of an integral scheme has a generic point over the original one before its first containing centre).

    source
    theorem Hironaka.Resolution.GenericLift.isGenericPoint_strictTransformSeq {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {η : ↥X} {i : Fin (S.length + 1)} {η' : ↥(S.stage i)} (h : GenericLift S I E m η i η') :
    IsGenericPoint η' ↑(S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) i).support

    The lifted point is a generic point of the strict transform's support.

    source
    theorem Hironaka.Resolution.GenericLift.mem_support {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {η : ↥X} {i : Fin (S.length + 1)} {η' : ↥(S.stage i)} (h : GenericLift S I E m η i η') :
    η' ∈ (S.strictTransformSeq (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})) i).support

    The lifted point lies on the strict transform.

    source
    theorem Hironaka.Resolution.GenericLift.stalkIdeal_eq_maximalIdeal {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {η : ↥X} {i : Fin (S.length + 1)} {η' : ↥(S.stage i)} (h : GenericLift S I E m η i η') (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) :
    (S.markedTransformSeq I m i).stalkIdeal η' = IsLocalRing.maximalIdeal ↑((S.stage i).presheaf.stalk η')

    The marked transform's stalk at the lifted point is the maximal ideal.

    source
    theorem Hironaka.Resolution.GenericLift.ord_eq_one {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {η : ↥X} {i : Fin (S.length + 1)} {η' : ↥(S.stage i)} [AlgebraicGeometry.IsLocallyNoetherian (S.stage i)] (h : GenericLift S I E m η i η') (hIc : I.stalkIdeal η = (AlgebraicGeometry.Scheme.IdealSheafData.vanishingIdeal (TopologicalSpace.Closeds.closure {η})).stalkIdeal η) (hI0 : I.stalkIdeal η ≠ ⊥) :
    (S.markedTransformSeq I m i).ord η' = 1

    The marked transform has order 1 at the lifted point when I is nonzero at η.

    source
    theorem Hironaka.Resolution.GenericLift.stalkIdeal_monomialPart_eq_top {X : AlgebraicGeometry.Scheme} {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} {η : ↥X} {i : Fin (S.length + 1)} {η' : ↥(S.stage i)} [AlgebraicGeometry.IsLocallyNoetherian X] [TopologicalSpace.NoetherianSpace ↥(S.stage i)] (h : GenericLift S I E m η i η') (hηE : ∀ (j : E.ι), η ∉ (E.component j).support) (K : (S.stage i).IdealSheafData) :
    (BMO.monomialPart K (S.totalTransformSeq E i)).stalkIdeal η' = ⊤

    Any ideal sheaf's monomial part with respect to the total transform of E is the unit ideal at the lifted point.