Clauses (1)–(3) of Kollár's Theorem 36 for the resolution functor on the class #
The three geometric clauses of [Kol07, Theorem 36] for the resolution functor BR k X
(Hironaka.Resolution.Algebraic.Kol07.Thm36.BR) on every member X of the class
IsReducedEquidimensional k X (reduced, smooth locus over k of one relative dimension): the end
result is smooth over k (1), the composite Π : X_r → X is an isomorphism over the smooth locus
of X (2), and the preimage of the singular locus is the support of a simple normal crossing
family of divisors on X_r (3).
theorem36_BRAffine— on an AFFINE class member.BRAffine k Xis the affine resolutionBR_affine TA embof an admissible embedding of codimension≥ 2(exists_admissibleEmbedding_of_codim) with its globally empty blow-ups deleted (BRAffine_eq_eraseEmpty_BR_affine); the clauses hold forBR_affine TA emb(Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36Reduced: the step by which Kollár'sBRis "defined on (possibly reducible) affine schemes" in the proof of Theorem 36, the irreducible components ofXall absorbed at the one truncation index) and pass along the isomorphism of the last stages (Hironaka.Resolution.Algebraic.Kol07.Thm36.LastIsoTransport). On the empty scheme the clauses hold by locality over the empty cover (Hironaka.Resolution.Algebraic.Kol07.Thm36.ClauseLocality).theorem36_BR— on every class member, by the descent of [Kol07, Proposition 37]: the pullback ofBR k Xalong a member of the finite affine cover is the pullback of the affine value on the cover scheme∐ Uᵢalong the summand inclusion (BR_pullback_finiteAffineCover_f, fromBR_pullback_affineCoverDescofHironaka.Resolution.Algebraic.Kol07.Thm36.BRDescent), the affine clauses restrict along the summand inclusions, and the clauses are local on the base.BR_smooth_last_of_class,BR_isIso_over_smoothLocus_of_class,BR_exists_snc_support_of_class— the three clauses separately, for the functorBRFunctor k(whose sequence atXisBR k Xby definition).
The affine assembly: clauses (1)–(3) for BRAffine X, X an affine class member #
Clauses (1)–(3) of [Kol07, Theorem 36] for BRAffine k X on a possibly reducible affine class
member X: the clauses for the affine resolution of an admissible embedding of codimension ≥ 2
(smooth_composite_BR_affine_of_class, isIso_composite_restrict_smoothLocus_BR_affine_of_class,
exists_snc_preimage_singularLocus_BR_affine_of_class), transported along the isomorphism of last
stages of the deletion of the empty blow-ups (eraseEmptyLastIso); on the empty scheme by
locality over the empty cover.
Descent to BR along the finite affine cover, and the three clauses separately #
The descent of [Kol07, Proposition 37]: the pullback of BR k X along a member Uᵢ → X of
the finite affine cover is the pullback of the affine value on the cover scheme ∐ Uᵢ along the
summand inclusion (BR_pullback_affineCoverDesc with ι_comp_affineCoverDesc).
The smooth locus of X over k pulls back along a member of the finite affine cover to the
pullback along the summand inclusion of the smooth locus of the cover scheme
(Scheme.Hom.preimage_smoothLocus_eq twice).
Clauses (1)–(3) of [Kol07, Theorem 36] for BR k X on every class member: the affine clauses
on the cover scheme ∐ Uᵢ (theorem36_BRAffine) descend along the finite affine cover
(BR_pullback_finiteAffineCover_f), the clauses being local on the base and stable under
pullback along open immersions.
Clause (1) of [Kol07, Theorem 36] for the functor BRFunctor k on a class member: the end
result is smooth over k.
Clause (2) of [Kol07, Theorem 36] for the functor BRFunctor k on a class member: the
composite is an isomorphism over the smooth locus of X.
Clause (3) of [Kol07, Theorem 36] for the functor BRFunctor k on a class member: the
preimage of the singular locus is the support of a simple normal crossing family on the end
result.