Documentation

Hironaka.Resolution.Algebraic.Kol07.Thm36.EraseEmptyIndex

The stage index of a sequence after deleting its empty blow-ups #

Kollár's convention on empty blow-ups [Kol07, 32] and the second clause of functoriality under smooth morphisms [Kol07, 34.1] ("deleting every blow-up h^*π_i whose center is empty", then reindexing) compare a sequence with the sequence obtained by deleting its empty blow-ups: the stage m of S with a nonempty centre becomes the stage eraseIdx S m of S.eraseEmpty, the number of nonempty centres of S before m. The embedded desingularization loop is transported along a smooth morphism h whose pulled-back run has empty centres (the centres missing the image of h), and the affine resolution functor truncates at a first-centre index, so the predicate CenterContains and the truncation take have to be carried across eraseEmpty:

Used by Hironaka.Resolution.Algebraic.Kol07.Thm36.FirstCenterEraseEmpty and the transport lemmas of the embedded desingularization (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedEraseEmpty).

source
noncomputable def Hironaka.Resolution.eraseIdx {X : AlgebraicGeometry.Scheme} :
X.BlowUpSequence → ℕ → ℕ

The reindexing of [Kol07, 34.1]: the stage of S.eraseEmpty corresponding to the stage m of S, namely the number of nonempty centres of S before m.

Equations
Instances For
    source
    theorem Hironaka.Resolution.eraseIdx_nil {X : AlgebraicGeometry.Scheme} (m : ℕ) :
    eraseIdx (AlgebraicGeometry.Scheme.BlowUpSequence.nil X) m = 0
    source
    theorem Hironaka.Resolution.eraseIdx_cons_zero {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) :
    eraseIdx (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) 0 = 0
    source
    theorem Hironaka.Resolution.eraseIdx_cons_succ_of_eq_top {X : AlgebraicGeometry.Scheme} {D : X.IdealSheafData} (rest : D.blowUp.BlowUpSequence) (hD : D = ⊤) (m : ℕ) :
    eraseIdx (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) (m + 1) = eraseIdx rest m

    A deleted (empty) blow-up does not advance the index.

    source
    theorem Hironaka.Resolution.eraseIdx_cons_succ_of_ne_top {X : AlgebraicGeometry.Scheme} {D : X.IdealSheafData} (rest : D.blowUp.BlowUpSequence) (hD : D ≠ ⊤) (m : ℕ) :
    eraseIdx (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) (m + 1) = eraseIdx rest m + 1

    A kept (nonempty) blow-up advances the index by one.

    source
    theorem Hironaka.Resolution.eraseIdx_mono {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {m m' : ℕ} :
    m ≤ m' → eraseIdx S m ≤ eraseIdx S m'

    The index is monotone in the stage.

    source
    theorem Hironaka.Resolution.eraseEmpty_take {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (m : ℕ) :
    S.eraseEmpty.take (eraseIdx S m) = (S.take m).eraseEmpty

    The reindexing on the truncations [Kol07, 34.1]: the erased sequence truncated at the index of m is the erased truncation at m.

    source
    theorem Hironaka.Resolution.centerContains_eraseEmpty_iff {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (c : X.IdealSheafData) (m : ℕ) (hm : m < S.length) :
    S.center ⟨m, hm⟩ ≠ ⊤ → (CenterContains S.eraseEmpty c (eraseIdx S m) ↔ CenterContains S c m)

    The predicate CenterContains across the deletion of empty blow-ups [Kol07, 34.1]: at a stage m of S with a nonempty centre, the centre of S.eraseEmpty at eraseIdx S m contains the strict transform of c if and only if the centre of S at m does. A deleted empty blow-up carries the strict transform along the trivial blow-up (strictTransform_top_left), an isomorphism along which the predicate transports (centerContains_pullback_iff_of_isIso).

    source
    theorem Hironaka.Resolution.exists_eraseIdx_eq {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (m' : ℕ) :
    m' < S.eraseEmpty.length → ∃ (m : ℕ) (hm : m < S.length), S.center ⟨m, hm⟩ ≠ ⊤ ∧ eraseIdx S m = m'

    Every stage of S.eraseEmpty is the index of a stage of S with a nonempty centre.

    source
    theorem Hironaka.Resolution.exists_eraseIdx_eq_of_lt {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {n m' : ℕ} (hm' : m' < S.eraseEmpty.length) (hlt : m' < eraseIdx S n) :
    ∃ (m : ℕ) (hm : m < S.length), S.center ⟨m, hm⟩ ≠ ⊤ ∧ eraseIdx S m = m' ∧ m < n

    A stage of S.eraseEmpty below the index of n is the index of a nonempty stage below n.