All components of a reduced equidimensional scheme are absorbed at the same index

Kollár defines BR on "(possibly reducible) affine schemes" as in the proof of Kol07, Corollary 22: embed X ↪ A, run BP(A, I_X, ∅) and truncate at the first centre containing the strict transform of X [Kol07, Theorem 36, proof]. For a reducible X this presupposes that the irreducible components are absorbed together: the first blow-up along a centre containing the strict transform of one component deletes that component. This module proves it for a reduced X whose smooth locus over k is smooth of ONE relative dimension (all components of one dimension), whether or not the components meet:

• componentIndex, the absorbing index of a component C in the run BP TA of an admissible embedding: the first centre containing the strict transform of the reduced closed subscheme of C, pushed to the ambient (firstCenterIndex);
• componentIndex_eq: any two components have the same absorbing index;
• firstCenterIndex_eq_componentIndex: the first centre containing the strict transform of the whole of X, the truncation index of BR_affine, is the common absorbing index.

The argument is Kollár's localisation [Kol07, 4.2; Theorem 27, proof] applied to two components. Suppose j := j(C') < j(C). The absorbing centre Z_j of C' has a point over every point of C' (exists_mem_strictTransformSeq_support_stageMap_eq: the strict transform of C' at stage j lies in Z_j and maps onto C', the stage map being proper and the image containing the generic point), in particular over a closed smooth point x₀ of C' (the generic point of C' is a smooth point, and the closed points of the Jacobson X meet every nonempty locally closed set). No restricted centre Z_i ∩ X̄_i with i ≤ j < j(C) has a point over the generic point of C (notMem_center_support_of_stageMap_eq_of_lt_firstCenterIndex), so none has one over a closed smooth point x₀' of C outside the closed set of points over which some restricted centre has a point. But two closed smooth points see the same restricted centres (restrictedCenterHasPointOver_iff_of_mem_smoothLocus: the two-point étale pair and the functoriality of BP under smooth surjections, [Kol07, Theorem 35 (4)]): contradiction. Nothing about how the components meet is used; the equidimensionality enters only through the étale pair, and the codimension of X in A plays no role (the common value may be the length of the run).

The identification. For any blow-up sequence S on A and a reduced closed subscheme X = V(I) ↪ A, the centre Z_i contains the strict transform of X iff it contains the strict transforms of all components of X (centerContains_iff_forall_component): one direction is the monotonicity of the strict transform, the other is that the support of the strict transform of a finite union is the union of the strict transforms' supports and that the strict transform of the reduced X is reduced (Hironaka.Resolution.Algebraic.Wlo05.EmbeddedPullbackTools). Hence, when all components have the absorbing index j, so has X (firstCenterIndex_eq_of_forall). Without the equality the first centre containing the strict transform of X would be the one at which the LAST component is absorbed, and the components absorbed earlier would be blown up along themselves.

noncomputable def Hironaka.Resolution.componentIndex (k : Type u) [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsNoetherian X] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : ℕ

The absorbing index of the irreducible component C of X in the run BP TA along the closed embedding emb: the first centre containing the strict transform of C (firstCenterIndex), taken for the reduced closed subscheme X.irreducibleComponentIdeal C hC of the component, pushed to the ambient.

Equations

• Hironaka.Resolution.componentIndex k X TA emb C hC = Hironaka.Resolution.firstCenterIndex (Hironaka.Sequence.BP TA) ((X.irreducibleComponentIdeal C hC).map emb)

theorem Hironaka.Resolution.componentIndex_def (k : Type u) [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsNoetherian X] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : componentIndex k X TA emb C hC = firstCenterIndex (Sequence.BP TA) ((X.irreducibleComponentIdeal C hC).map emb)

The defining equation of componentIndex.

The absorbing centre lies over the whole component

theorem Hironaka.Resolution.exists_mem_strictTransformSeq_support_stageMap_eq {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (I : A.IdealSheafData) [AlgebraicGeometry.IsIntegral I.subscheme] {η : ↥A} (hη : IsGenericPoint η ↑I.support) (i : Fin (S.length + 1)) (hi : ↑i ≤ firstCenterIndex S I) {x : ↥A} (hx : x ∈ I.support) : ∃ p ∈ (S.strictTransformSeq I i).support, (S.stageMap i) p = x

Before or at the first containing centre, the strict transform of an integral V(I) maps onto V(I): its generic point lies over the generic point η of V(I), and the image of the strict transform under the proper stage map is closed, so it contains the closure of η.

The theorem

theorem Hironaka.Resolution.componentIndex_le {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) (C C' : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) (hC' : C' ∈ irreducibleComponents ↥X) : componentIndex k X TA emb C hC ≤ componentIndex k X TA emb C' hC'

One inequality of componentIndex_eq, by contradiction: if C' is absorbed strictly before C, at index j, then the restricted centre Z_j ∩ X̄_j has a point over a closed smooth point of C' and none over a closed smooth point of C outside the closed set of points over which some restricted centre of index ≤ j has a point, while the two closed smooth points see the same restricted centres.

theorem Hironaka.Resolution.componentIndex_eq {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) (C C' : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) (hC' : C' ∈ irreducibleComponents ↥X) : componentIndex k X TA emb C hC = componentIndex k X TA emb C' hC'

All irreducible components of a reduced equidimensional scheme are absorbed at the same index. For a reduced X whose smooth locus over k is smooth of one relative dimension, embedded by an admissible embedding X ↪ A, any two irreducible components C, C' of X have the same absorbing index in the run BP(A, I_X, ∅), whether or not they meet (componentIndex_le both ways).

The identification of the first containing centre

theorem Hironaka.Resolution.coe_support_ker_eq_iUnion (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsNoetherian X] {A : AlgebraicGeometry.Scheme} (emb : X ⟶ A) [AlgebraicGeometry.IsClosedImmersion emb] : ↑(AlgebraicGeometry.Scheme.Hom.ker emb).support = ⋃ C ∈ Set.univ, ↑((X.irreducibleComponentIdeal ↑C ⋯).map emb).support

The support of the ideal of X in the ambient is the union of the supports of the pushed reduced ideals of its components.

theorem Hironaka.Resolution.centerContains_iff_forall_component (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (emb : X ⟶ A) [AlgebraicGeometry.IsClosedImmersion emb] (n : ℕ) (hn : n < S.length) : CenterContains S (AlgebraicGeometry.Scheme.Hom.ker emb) n ↔ ∀ (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X), CenterContains S ((X.irreducibleComponentIdeal C hC).map emb) n

A centre contains the strict transform of the reduced X iff it contains the strict transforms of all its components: monotonicity of the strict transform one way; the finite-union formula for the support of the strict transform and the reducedness of the strict transform of X the other.

theorem Hironaka.Resolution.firstCenterIndex_eq_of_forall (X : AlgebraicGeometry.Scheme) [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] {A : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian A] (S : A.BlowUpSequence) (emb : X ⟶ A) [AlgebraicGeometry.IsClosedImmersion emb] (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) (h : ∀ (C' : Set ↥X) (hC' : C' ∈ irreducibleComponents ↥X), firstCenterIndex S ((X.irreducibleComponentIdeal C' hC').map emb) = firstCenterIndex S ((X.irreducibleComponentIdeal C hC).map emb)) : firstCenterIndex S (AlgebraicGeometry.Scheme.Hom.ker emb) = firstCenterIndex S ((X.irreducibleComponentIdeal C hC).map emb)

If all components of the reduced X have the same first containing centre, it is the first containing centre of X.

theorem Hironaka.Resolution.firstCenterIndex_eq_componentIndex {k : Type u} [Field k] [CharZero k] (X : AlgebraicGeometry.Scheme) [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsNoetherian X] [AlgebraicGeometry.IsReduced X] {d : ℕ} [AlgebraicGeometry.SmoothOfRelativeDimension d (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)).ι (X ↘ AlgebraicGeometry.Spec ↧k))] (TA : AlgebraicGeometry.Triple k) (emb : X ⟶ TA.X.left) (hadm : AdmissibleEmbedding k X TA emb) (C : Set ↥X) (hC : C ∈ irreducibleComponents ↥X) : firstCenterIndex (Sequence.BP TA) TA.I = componentIndex k X TA emb C hC

The truncation index of BR_affine is the common absorbing index: on a reduced X whose smooth locus is smooth of one relative dimension, with an admissible embedding, the first centre of BP TA containing the strict transform of X is the absorbing index of any one component (componentIndex_eq, firstCenterIndex_eq_of_forall).