Documentation

Hironaka.Scheme.BlowUpSequence.Concat

Concatenation of blow-up sequences #

Blow-up sequences [Kol07, Definition 29] compose: a sequence S on X of length r ending at X_r, followed by a sequence T on X_r of length s, is a sequence on X of length r + s with composite Π_T ≫ Π_S (Kollár's Π_{ij} bookkeeping; the disjoining sequence "composed on the right" with the marked order reduction functor in [Kol07, 72] is the same operation). On the inductive type AlgebraicGeometry.Scheme.BlowUpSequence (nil, and cons X D rest with rest living on D.blowUp) the concatenation is the structural recursion below: the tail of cons X D rest is a sequence on blowUp X D whose last stage is definitionally (cons X D rest).last, so the second argument needs no transport.

Concatenation is used to refine a smooth blow-up sequence to one with irreducible centers (each center Z_i is replaced by the sequence blowing up its components one at a time, Hironaka/Resolution/Algebraic/Kol07/Componentwise.lean, and the remainder of the sequence, carried across the canonical isomorphism of the end results, is concatenated on the right), and to assemble the rounds of the order reduction and resolution algorithms into one sequence.

Main declarations #

source
noncomputable def AlgebraicGeometry.Scheme.BlowUpSequence.concat {X : Scheme} (S : X.BlowUpSequence) :
S.last.BlowUpSequence → X.BlowUpSequence

The concatenation of a blow-up sequence S on X with a blow-up sequence T on its last stage S.last: the sequence performing the blow-ups of S and then those of T [Kol07, Definition 29].

Equations
Instances For
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.BlowUpSequence.concat_nil {X : Scheme} (T : (nil X).last.BlowUpSequence) :
    (nil X).concat T = T
    source
    @[simp]
    theorem AlgebraicGeometry.Scheme.BlowUpSequence.concat_cons {X : Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (T : (cons X D rest).last.BlowUpSequence) :
    (cons X D rest).concat T = cons X D (rest.concat T)
    source
    theorem AlgebraicGeometry.Scheme.BlowUpSequence.length_concat {X : Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) :
    (S.concat T).length = S.length + T.length

    The length of a concatenation is the sum of the lengths (Kollár's r + s).