Clauses (1)–(3) of Theorem 36 for the affine resolution of a reduced equidimensional scheme

For the resolution BR_affine TA emb of a reduced affine scheme X ↪ A whose smooth locus over k is smooth of one relative dimension (Hironaka.Resolution.Algebraic.Kol07.Thm36.Affine: the restriction to X of the principalization sequence BP(A, I_X, ∅) truncated at the first centre containing the strict transform of X), the three geometric clauses of [Kol07, Theorem 36] — the step by which Kollár's BR is "defined on (possibly reducible) affine schemes" in the proof of the theorem. The irreducible components of X may meet. Throughout, X is nonempty (hne) and of codimension ≥ 2 in A at every generic point (hcodim, the choice of the embedding in the proof of [Kol07, Theorem 36]); the empty X is treated by the assembly.

By Hironaka.Resolution.Algebraic.Kol07.Thm36.EqualAbsorbingIndex, the truncation index j = firstCenterIndex (BP TA) TA.I is the absorbing index of every component C of X, and it is an index of the run: some centre has a point over the generic point of C, since Π^* I_X is invertible and I_X is the maximal ideal of the regular local ring of A at that point (componentIndex_lt_length, the argument of the proof of [Kol07, Corollary 22]). At stage j:

• clause (1) (smooth_composite_BR_affine_of_class): the strict transform C̄_j of each component is integral and is an irreducible component of the smooth centre Z_j, open in Z_j, because its generic point is the unique point of the stage over the generic point of C, which is a maximal point of X (isOpenImmersion_inclusion_component); the strict transform X̄_j of X is reduced with support the union of the C̄_j, so its inclusion into the reduced Z_j is a closed immersion with open range, hence an open immersion (isOpenImmersion_inclusion_firstCenterIndex), and X̄_j, the end result, is smooth over k;
• clause (2) (isIso_composite_restrict_smoothLocus_BR_affine_of_class): no restricted centre Z_i ∩ X̄_i, i < j, has a point over a smooth point of X (not_restrictedCenterHasPointOver_BP_of_mem_smoothLocus_of_class): none has over the generic point of a component (i < j is the absorbing index of that component), and two closed smooth points see the same restricted centres (not_restrictedCenterHasPointOver_of_mem_smoothLocus_of_exists);
• clause (3) (exists_snc_preimage_singularLocus_BR_affine_of_class): the restriction to X̄_j of the exceptional divisors of A_j → A is a simple normal crossing family with support Π⁻¹(Sing X) (exists_isSnc_comap_totalTransformSeq_take_of_forall, through every point of X̄_j the strict transform of the component through its image, which no earlier centre contains).

The clauses are assembled on the whole affine X and on the class in Hironaka.Resolution.Algebraic.Kol07.Thm36.Theorem36Assembly.

The generic points of the components in the ambient

theorem Hironaka.Resolution.mem_genericPoints_support_ker {X A : AlgebraicGeometry.Scheme} (f : X ⟶ A) [AlgebraicGeometry.IsClosedImmersion f] {C : Set ↥X} (hC : C ∈ irreducibleComponents ↥X) {η : ↥X} (hη : IsGenericPoint η C) : f η ∈ (AlgebraicGeometry.Scheme.Hom.ker f).support.genericPoints

The generic point of a component C of X, pushed along the closed immersion emb, is a maximal point of emb(X) = V(ker emb) (Closeds.genericPoints): a point of emb(X) generalising it is the image of a point of X generalising the generic point of C, which is that generic point (a closed embedding reflects specialisation).

theorem Hironaka.Resolution.le_map_irreducibleComponentIdeal {k : Type u} [Field k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsNoetherian X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : TA.I ≤ (X.irreducibleComponentIdeal C hC).map emb

The ideal of X lies in the pushed reduced ideal of each component.

The absorbing index is an index of the run

theorem Hironaka.Resolution.componentIndex_lt_length {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : componentIndex k X TA emb C hC < (Sequence.BP TA).length

Some centre of BP TA contains the strict transform of each component Kol07, Corollary 22, proof: I_X is the maximal ideal of the regular local ring of A at the generic point η_C of the component, of dimension ≥ 2 (hcodim), so it is not principal there, while Π^* I_X is invertible (clause (2) of [Kol07, Theorem 35]); hence some centre has a point over η_C (exists_mem_center_support_of_isInvertible_comap_composite), and the least such centre contains the strict transform of C (exists_centerContains_of_exists_mem_center_support).

Two general lemmas on inclusions of closed subschemes

theorem Hironaka.Resolution.isOpenImmersion_inclusion_of_mem_genericPoints {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsNoetherian A] (S : A.BlowUpSequence) (I : A.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] (j : Fin S.length) (hj : ↑j = firstCenterIndex S I) (hle : S.center j ≤ S.strictTransformSeq I j.castSucc) (hZ : AlgebraicGeometry.IsRegular (S.center j).subscheme) {K : TopologicalSpace.Closeds ↥A} (hcos : ∀ y ∈ (S.center j).support, (S.stageMap j.castSucc) y ∈ K) {η : ↥A} (hη : IsGenericPoint η ↑I.support) (hηK : η ∈ K.genericPoints) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)

The identification of Hironaka.Resolution.Algebraic.Kol07.Thm36.Identification with the centre lying over a closed set K in which the generic point η of V(I) is maximal (instead of over V(I) itself): at the first centre Z_j containing the strict transform of the integral V(I), if Z_j is regular, lies over K, and η ∈ K.genericPoints, then X̄_j is an irreducible component of Z_j, open in it. For the components of a reduced X, K = emb(X).

theorem Hironaka.Resolution.range_inclusion {A : AlgebraicGeometry.Scheme} {Z T : A.IdealSheafData} (hle : Z ≤ T) : Set.range ⇑(AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle) = ⇑Z.subschemeι ⁻¹' ↑T.support

The range of the inclusion V(T) ⟶ V(Z) of closed subschemes (Z ≤ T) is the preimage of V(T) under the inclusion of V(Z).

The absorbing index on the class

theorem Hironaka.Resolution.firstCenterIndex_lt_length_BP_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) : firstCenterIndex (Sequence.BP TA) TA.I < (Sequence.BP TA).length

The truncation index of BR_affine is an index of the run BP TA (X nonempty).

theorem Hironaka.Resolution.centerContains_firstCenterIndex_BP_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) : CenterContains (Sequence.BP TA) TA.I (firstCenterIndex (Sequence.BP TA) TA.I)

The centre at the truncation index contains the strict transform of X.

theorem Hironaka.Resolution.centerContains_component_firstCenterIndex {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : CenterContains (Sequence.BP TA) ((X.irreducibleComponentIdeal C hC).map emb) (firstCenterIndex (Sequence.BP TA) TA.I)

The centre at the truncation index contains the strict transform of every component.

Clause (1): the end result is smooth

theorem Hironaka.Resolution.isOpenImmersion_inclusion_component {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) (hj : firstCenterIndex (Sequence.BP TA) TA.I < (Sequence.BP TA).length) (hle : (Sequence.BP TA).center ⟨firstCenterIndex (Sequence.BP TA) TA.I, hj⟩ ≤ (Sequence.BP TA).strictTransformSeq ((X.irreducibleComponentIdeal C hC).map emb) ⟨firstCenterIndex (Sequence.BP TA) TA.I, ⋯⟩) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)

At the truncation index j, the strict transform of each component C of X is an irreducible component of the centre Z_j, open in it: Z_j is smooth, hence regular, and lies over emb(X) (the centres of BP(A, I_X, ∅) lie over V(I_X)), in which the generic point of C is maximal.

theorem Hironaka.Resolution.isOpenImmersion_inclusion_firstCenterIndex {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) (hj : firstCenterIndex (Sequence.BP TA) TA.I < (Sequence.BP TA).length) (hle : (Sequence.BP TA).center ⟨firstCenterIndex (Sequence.BP TA) TA.I, hj⟩ ≤ (Sequence.BP TA).strictTransformSeq TA.I ⟨firstCenterIndex (Sequence.BP TA) TA.I, ⋯⟩) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)

At the truncation index j, the strict transform X̄_j of X is an open subscheme of the centre Z_j: its support is the union of the supports of the components' strict transforms, each open in Z_j (isOpenImmersion_inclusion_component), and a closed immersion into the reduced Z_j with open range is an open immersion.

theorem Hironaka.Resolution.smooth_composite_BR_affine_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) (hcodim : ∀ η ∈ genericPoints ↥X, 2 ≤ ringKrullDim ↑(TA.X.left.presheaf.stalk (emb η))) : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp (BR_affine TA emb).composite (X ↘ AlgebraicGeometry.Spec ↧k))

Clause (1) of [Kol07, Theorem 36] for the affine resolution of a reduced equidimensional scheme: the end result of BR_affine TA emb is smooth over k. It is the strict transform X̄_j at the truncation index, an open subscheme of the smooth centre Z_j (isOpenImmersion_inclusion_firstCenterIndex, smooth_composite_pullback_take).

Clause (2): an isomorphism over the smooth locus

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_BP_genericPoint_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) {η : ↥X} (hη : IsGenericPoint η C) (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 η)

Before the truncation index no restricted centre of BP TA has a point over the generic point of a component of X: the truncation index is the absorbing index of the component (notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex).

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_BP_of_mem_smoothLocus_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) {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 truncation index has a point over a smooth point of X (not_restrictedCenterHasPointOver_of_mem_smoothLocus_of_exists, from the generic point of a component, with the functoriality of the principalization sequence under smooth surjections).

theorem Hironaka.Resolution.isIso_composite_restrict_smoothLocus_BR_affine_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) : 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 a reduced equidimensional 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.

Clause (3): the preimage of the singular locus

theorem Hironaka.Resolution.exists_snc_preimage_singularLocus_BR_affine_of_class {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)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (hne : Nonempty ↥X) (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 a reduced equidimensional scheme: Π⁻¹(Sing X) is the support of a simple normal crossing family on the end result, the restriction of the total exceptional divisor (exists_isSnc_comap_totalTransformSeq_take_of_forall: through every point of X̄_j passes the strict transform of the component through its image, an integral closed subscheme of X that no centre before j contains).