Kollár's resolution functor on reduced equidimensional schemes #
The resolution functor BR of [Kol07, Theorem 36], the witness of
AlgebraicGeometry.exists_functorial_resolution
(Hironaka.Resolution.Algebraic.Kol07.Thm36.Theorem36), on the class IsReducedEquidimensional k X
of reduced schemes whose smooth locus over k is smooth of one relative dimension
(Hironaka.Scheme.Resolution.Defs); the irreducible components may meet. Kollár constructs
BR first on affine schemes and then glues by the descent of [Kol07, Proposition 37]; this file
follows him.
The construction #
- On an affine scheme
Xoverk(BRAffine): embedXby an admissible embeddingX ↪ A(AdmissibleEmbedding: a closed immersion overkinto a smooth affineAwith the ideal of the triple the ideal ofXand empty boundary), run the single principalization sequenceBP(A, I_X, ∅)and restrict it toX, truncated at the first centre containing the strict transform ofX— the embedding-free affine resolutionBR_affine' k XofHironaka.Resolution.Algebraic.Kol07.Thm36.Independence, independent of the admissible pair byBR_affine'_eq("BR(X)is independent of the choice of the embedding", Kol07, Theorem 36, proof) — and delete its globally empty steps (eraseEmpty, below). On a reducedXwhose smooth locus has one relative dimension, the first centre containing the strict transform ofXis the first centre containing the strict transform of EACH irreducible component (Hironaka.Resolution.Algebraic.Kol07.Thm36.EqualAbsorbingIndex), so this single truncation is the step by which Kollár'sBRis "defined on (possibly reducible) affine schemes"; no component is blown up along itself. - On any member (
BR): the descent of [Kol07, Proposition 37] ofBRAffine (∐ Uᵢ)along the smooth surjectiong : ∐ Uᵢ → Xfrom the finite affine cover (Hironaka.Scheme.BlowUpSequence.AffineCover;∐ Uᵢis affine and in the class),BRDescends, chosen byClassical.choose, with the globally empty steps deleted;nil Xotherwise (BR_eq_of_descends,BR_eq_nil_of_not_descends,BR_eq_nil_of_not_class; the descent holds on every member,Hironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent). BRFunctor k : ResolutionAssignment kpackagesBR k.
The deletion of the globally empty steps #
Kollár's convention [Kol07, 32] is that the outputs of the named blow-up sequence functors
contain no empty blow-up. His list omits BR, but his (34.1) at the identity morphism demands it:
clause (4a) of exists_functorial_resolution at Y := X, h := 𝟙 X reads BR X = (BR X).eraseEmpty. The affine resolution does not satisfy this by itself: a stage of the global run
whose centre misses the strict transform of X (a stratum of the exceptional divisors away from
the strict transform of X) restricts to the centre ⊤ on X, and BR_affine keeps such steps.
So both branches delete the globally empty steps. The deletion is compatible with the clauses of
the theorem: it commutes with pullback along flat surjective morphisms
(eraseEmpty_pullback_of_flat_surjective), it is idempotent (eraseEmpty_eraseEmpty), and (nil X).eraseEmpty = nil X.
The empty scheme is in the class; both definitions return the empty sequence on the nose
(BRAffine_eq_nil_of_isEmpty, BR_empty).
Blow-up sequences on an empty scheme #
On the empty scheme every ideal sheaf is ⊤, so every blow-up sequence deletes to the empty
sequence.
On an empty scheme two blow-up sequences of the same length are equal: every ideal sheaf on an
empty scheme is ⊤ and the blow-up of an empty scheme is empty.
The resolution of an affine scheme X over k ("we have now defined BR on (possibly
reducible) affine schemes", [Kol07, Theorem 36, proof]): the embedding-free affine resolution
BR_affine' k X — the global run BP(A, I_X, ∅) of an admissible embedding X ↪ A, restricted
to X and truncated at the first centre containing the strict transform of X — with its globally
empty steps deleted (the convention of [Kol07, 32] on the output, forced by (34.1) at the identity;
see the module docstring). The value does not depend on the admissible pair
(BRAffine_eq_eraseEmpty_BR_affine); without an admissible embedding (never on an affine scheme of
finite type over k, exists_admissibleEmbedding) it is nil X.
Equations
Instances For
BRAffine through any admissible pair: the affine resolution BR_affine TA emb with its
globally empty steps deleted (BR_affine'_eq).
BRAffine has no empty blow-up.
On an empty scheme the affine value is the empty sequence.
The descent along the finite affine cover [Kol07, Proposition 37]: a blow-up sequence on X
whose pullback along g : ∐ Uᵢ → X is the affine value on ∐ Uᵢ.
Equations
Instances For
Kollár's resolution functor on a reduced equidimensional scheme Kol07, Theorem 36;
Proposition 37: the descended sequence of BRDescends with its globally empty steps deleted (the
convention of [Kol07, 32] on the output, forced by clause (4a) at the identity; a no-op when
the descended sequence has no empty step, eraseEmpty_eraseEmpty); nil X off the class or when
the descent does not hold (the latter never on a member of the class,
Hironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent).
Equations
- One or more equations did not get rendered due to their size.
Instances For
On a member of the class for which the descent holds, BR is the chosen descended sequence
with its globally empty steps deleted.
On a member of the class without the cover descent, BR is the empty sequence (a branch never
taken, since the descent holds on every member of the class).
Off the class BR is the empty sequence.
BR has no empty blow-up (both branches of the definition).
On a member for which the descent holds, the pullback of BR along the finite affine cover is
the affine value on the cover scheme (the deletion of empty steps commutes with the pullback along
the flat surjection g, and BRAffine has no empty step).
The uniqueness in the descent: a sequence T on a member whose pullback along the finite
affine cover is the affine value on the cover scheme has BR k X = T.eraseEmpty (a blow-up
sequence is determined by its pullbacks to an open cover, eq_of_pullback_of_covers).
Kollár's resolution functor BR, packaged as a ResolutionFunctor k: the witness of
AlgebraicGeometry.exists_functorial_resolution.
Equations
- One or more equations did not get rendered due to their size.
Instances For
The empty scheme #
The finite affine cover scheme of an empty scheme is empty.
On an empty scheme, a member of the class, the resolution functor is the empty sequence, on the nose.