Clauses (2) and (3) of Theorem 36 for the affine resolution of an integral scheme

For the resolution BR_affine TA emb of an integral affine scheme X ↪ A (Hironaka.Resolution.Algebraic.Kol07.Thm36.Affine), clause (2) of [Kol07, Theorem 36], Π : X_j → X is an isomorphism over the smooth locus of X, and clause (3), Π⁻¹(Sing X) is the support of a simple normal crossing family on X_j, in the forms used by Hironaka's Main Theorem I (Hironaka.Resolution.Algebraic.Hir64.MainTheoremI); the versions for a reduced X whose smooth locus has one relative dimension, used by the resolution functor, are Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36Reduced:

• not_restrictedCenterHasPointOver_BP_genericPoint: before the first containing centre no restricted centre of BP TA has a point over the generic point of X (notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex);
• not_restrictedCenterHasPointOver_BP_of_mem_smoothLocus: Kollár's localisation argument [Kol07, 4.2] on the truncation, with the functoriality of the principalization sequence under smooth surjections [Kol07, Theorem 35 (4)]: no restricted centre has a point over any smooth point of X (not_restrictedCenterHasPointOver_of_mem_smoothLocus);
• isIso_composite_restrict_smoothLocus_BR_affine_of_integral: clause (2);
• exists_snc_preimage_singularLocus_BR_affine_of_integral: clause (3), by Hironaka.Resolution.Algebraic.Kol07.Thm36.SncPreimageSingular on BP TA at the first containing index, with the first containing centre and clause (1) from Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36.

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_BP_genericPoint {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.IsIntegral X] (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) (i : Fin ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).length) : ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)) TA.I i (emb (genericPoint ↥X))

Before the first containing centre no restricted centre of the truncation of BP TA has a point over the generic point of X [Kol07, Corollary 22, proof] (notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex through the truncation bridge restrictedCenterHasPointOver_take).

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_BP_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) {x : ↥X} (hx : x ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)) (i : Fin ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)).length) : ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((Sequence.BP TA).take (firstCenterIndex (Sequence.BP TA) TA.I)) TA.I i (emb x)

Kollár's localisation argument [Kol07, 4.2] on the truncation: no restricted centre of the truncation of BP TA at the first containing index has a point over a smooth point of X (not_restrictedCenterHasPointOver_of_mem_smoothLocus, with the functoriality of the principalization sequence under smooth surjections BP_pullback_of_surjective as the functoriality of the assignment T ↦ BP T).

theorem Hironaka.Resolution.isIso_composite_restrict_smoothLocus_BR_affine_of_integral {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) : CategoryTheory.IsIso ((BR_affine TA emb).composite ∣_ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k))

Clause (2) of [Kol07, Theorem 36] for the affine resolution of an integral scheme: Π : X_j → X is an isomorphism over the smooth locus of X. The restricted centres avoid X^{ns}, so isIso_composite_restrict_of_centers_disjoint applies to BR_affine TA emb.

theorem Hironaka.Resolution.exists_snc_preimage_singularLocus_BR_affine_of_integral {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) : ∃ (F : (BR_affine TA emb).last.DivisorFamily), F.IsSnc ∧ ↑F.support = ⇑(BR_affine TA emb).composite ⁻¹' (↑(AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)))ᶜ

Clause (3) of [Kol07, Theorem 36] for the affine resolution of an integral scheme, after the proof of [Kol07, Theorem 27]: Π⁻¹(Sing X) is the support of a simple normal crossing family, the restriction Ex_tot|_{X_j} of the total exceptional divisor. This is Hironaka.Resolution.Algebraic.Kol07.Thm36.SncPreimageSingular on BP TA at the first containing index, the hypotheses being the first containing centre and clause (1) of Theorem 36 (Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36), clause (1) of [Kol07, Theorem 35] at j, the identification X̄_j = Z_j^η (Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification, with the centres over V(I_X)), "no earlier centre contains X̄", and the mechanism of clause (2).