The strict transform at the first containing centre is a component of the centre

In the proof of [Kol07, Corollary 22], at the first blow-up whose centre Z_j contains the strict transform X̄_j of X, the image π_0 ⋯ π_{j−1}(Z_j) lies in X̄, so η_X is the generic point of Z_j: the resolution of X is the component of the smooth centre through the generic point. This file proves that identification in general form, as a lemma about closed subschemes:

• on any scheme B with a Noetherian underlying space, for closed subschemes V(T) ⊆ V(Z) (Z ≤ T) with V(T) integral, V(Z) regular (every stalk a regular local ring), and the generic point η' of V(T) maximal in V(Z) (no point of V(Z) generalises it), the inclusion V(T) ⟶ V(Z) is an open immersion: V(T) is the irreducible component of V(Z) through η', and the irreducible components of a regular Noetherian scheme are open (they are pairwise disjoint, a regular local ring having a single minimal prime);
• along a blow-up sequence on a Noetherian scheme A, at the first centre Z_j containing the strict transform X̄_j of an integral V(I), the hypotheses hold when Z_j is regular and lies over V(I): η_j is the unique point over η (Hironaka.Resolution.Algebraic.Kol07.Thm36.FirstCenter), so a point of Z_j generalising η_j maps to a point of V(I) generalising η, which is η, hence it is η_j (isOpenImmersion_inclusion_of_firstCenterIndex).

The smoothness of the end result of the affine resolution then follows, since an open subscheme of a smooth scheme is smooth (smooth_subschemeι_comp_of_isOpenImmersion_inclusion; see Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineEndResult).

Conventions

IsRegular means that every stalk is a regular local ring (Hironaka.RegularSmooth); Closeds.genericPoints is the set of points of a closed subset maximal for specialisation; IdealSheafData.inclusion hle : T.subscheme ⟶ Z.subscheme is Mathlib's inclusion of closed subschemes for hle : Z ≤ T.

Irreducible components of a Noetherian space with pairwise disjoint components are open

theorem Hironaka.Resolution.isOpen_irreducibleComponent_of_inter_nonempty_imp_eq {α : Type u_1} [TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] (h : ∀ C₁ ∈ irreducibleComponents α, ∀ C₂ ∈ irreducibleComponents α, (C₁ ∩ C₂).Nonempty → C₁ = C₂) (x : α) : IsOpen (irreducibleComponent x)

In a Noetherian space whose irreducible components are pairwise disjoint, every irreducible component is open: its complement is the finite union of the other (closed) components.

Regular closed subschemes: disjoint components, reducedness

theorem Hironaka.Resolution.mem_genericPoints_support_of_isGenericPoint_of_mem_irreducibleComponents {B : AlgebraicGeometry.Scheme} (Z : B.IdealSheafData) {C : Set ↥Z.subscheme} (hC : C ∈ irreducibleComponents ↥Z.subscheme) {ξ : ↥Z.subscheme} (hξ : IsGenericPoint ξ C) : Z.subschemeι ξ ∈ Z.support.genericPoints

The image in B of the generic point of an irreducible component of the closed subscheme V(Z) is a maximal point of its support (Closeds.genericPoints).

theorem Hironaka.Resolution.eq_of_mem_irreducibleComponents_of_isRegular {B : AlgebraicGeometry.Scheme} (Z : B.IdealSheafData) (hZ : AlgebraicGeometry.IsRegular Z.subscheme) {C₁ C₂ : Set ↥Z.subscheme} (h₁ : C₁ ∈ irreducibleComponents ↥Z.subscheme) (h₂ : C₂ ∈ irreducibleComponents ↥Z.subscheme) (hne : (C₁ ∩ C₂).Nonempty) : C₁ = C₂

Two irreducible components of a regular closed subscheme meeting at a point coincide: their generic points are maximal points of the support specialising to a common point, hence equal (Hironaka.Sequence.eq_of_specializes_of_isRegular).

theorem Hironaka.Resolution.isReduced_of_isRegular {B : AlgebraicGeometry.Scheme} (hB : AlgebraicGeometry.IsRegular B) : AlgebraicGeometry.IsReduced B

A regular scheme is reduced (regular local rings are domains).

theorem Hironaka.Resolution.noetherianSpace_subscheme {B : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥B] (Z : B.IdealSheafData) : TopologicalSpace.NoetherianSpace ↥Z.subscheme

The underlying space of a closed subscheme of a Noetherian space is Noetherian.

theorem Hironaka.Resolution.isOpen_irreducibleComponent_of_isRegular {B : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥B] (Z : B.IdealSheafData) (hZ : AlgebraicGeometry.IsRegular Z.subscheme) (z : ↥Z.subscheme) : IsOpen (irreducibleComponent z)

Every irreducible component of a regular closed subscheme of a Noetherian scheme is open.

The identification

theorem Hironaka.Resolution.isOpenImmersion_of_isClosedImmersion_of_isOpen_range {B W : AlgebraicGeometry.Scheme} (ι : W ⟶ B) [AlgebraicGeometry.IsClosedImmersion ι] [AlgebraicGeometry.IsReduced B] (hopen : IsOpen (Set.range ⇑ι)) : AlgebraicGeometry.IsOpenImmersion ι

A closed immersion into a reduced scheme whose range is open is an open immersion: restricted over its range it is a surjective closed immersion onto a reduced scheme, hence an isomorphism (isIso_of_isClosedImmersion_of_surjective).

theorem Hironaka.Resolution.isOpenImmersion_inclusion_of_isGenericPoint {B : AlgebraicGeometry.Scheme} [TopologicalSpace.NoetherianSpace ↥B] (Z T : B.IdealSheafData) (hle : Z ≤ T) (hZ : AlgebraicGeometry.IsRegular Z.subscheme) {η' : ↥B} (hη' : IsGenericPoint η' ↑T.support) (hmax : η' ∈ Z.support.genericPoints) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)

The identification in general form [Kol07, Corollary 22, proof]: for closed subschemes V(T) ⊆ V(Z) of a Noetherian scheme with V(Z) regular and the generic point η' of V(T) a maximal point of V(Z), the inclusion V(T) ⟶ V(Z) is an open immersion: V(T) is the irreducible component of V(Z) through η'.

theorem Hironaka.Resolution.smooth_subschemeι_comp_of_isOpenImmersion_inclusion {B : AlgebraicGeometry.Scheme} {Z T : B.IdealSheafData} (hle : Z ≤ T) [AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)] {Y : AlgebraicGeometry.Scheme} (g : B ⟶ Y) [AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι g)] : AlgebraicGeometry.Smooth (CategoryTheory.CategoryStruct.comp T.subschemeι g)

An open subscheme of a smooth scheme is smooth: if the inclusion V(T) ⟶ V(Z) is an open immersion and V(Z) is smooth over Y, so is V(T) ("Z_j is smooth since we blow it up", [Kol07, Corollary 22, proof]; the component X̄_j of Z_j inherits the smoothness).

Noetherian stages

theorem Hironaka.Resolution.isNoetherian_stage_mk {A : AlgebraicGeometry.Scheme} (hA : AlgebraicGeometry.IsNoetherian A) (S : A.BlowUpSequence) (n : ℕ) (hn : n < S.length + 1) : AlgebraicGeometry.IsNoetherian (S.stage ⟨n, hn⟩)

The stages of a blow-up sequence on a Noetherian scheme are Noetherian (blowUp.isNoetherian).

theorem Hironaka.Resolution.isNoetherian_stage {A : AlgebraicGeometry.Scheme} [hA : AlgebraicGeometry.IsNoetherian A] (S : A.BlowUpSequence) (i : Fin (S.length + 1)) : AlgebraicGeometry.IsNoetherian (S.stage i)

isNoetherian_stage_mk in the Fin form.

At the first containing centre

theorem Hironaka.Resolution.isOpenImmersion_inclusion_of_firstCenterIndex {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) (hcos : ∀ y ∈ (S.center j).support, (S.stageMap j.castSucc) y ∈ I.support) : AlgebraicGeometry.IsOpenImmersion (AlgebraicGeometry.Scheme.IdealSheafData.inclusion hle)

"η_X is the generic point of Z_j" [Kol07, Corollary 22, proof]: along a blow-up sequence on a Noetherian scheme, at the first centre Z_j containing the strict transform X̄_j of an integral closed subscheme V(I), if Z_j is regular and lies over V(I), then X̄_j is an irreducible component of Z_j: the inclusion V(X̄_j) ⟶ V(Z_j) is an open immersion. The generic point η_j of X̄_j is the unique point of the stage over the generic point η of V(I) (Hironaka.Resolution.Algebraic.Kol07.Thm36.FirstCenter), so a point of Z_j generalising η_j maps to a point of V(I) generalising η, which is η; hence it is η_j, and isOpenImmersion_inclusion_of_isGenericPoint applies.