Transport along an open immersion whose range contains the centers

The proof of Corollary 1 of Main Theorem II [Hir64, pp. 143–144] runs Main Theorem II on the open subscheme X̄ = X ∖ S and extends the succession across S by open immersions u_i : X̄(i) → X(i) with u_i(D̄(i)) = D(i). The extension S on X has S.pullback u = S̄ (Hironaka/Resolution/Algebraic/Hir64/ExtendOpen.lean), and every center of S lies in the range of the stage lift u_i (CentersInRange). This module transports along such an open immersion what the corollary needs:

• the closed subschemes of the centers: for a closed Z ⊆ X whose support lies in the range of the open immersion φ, the induced map V(φ⁻¹ Z) → V(Z) is an isomorphism (an open immersion, as the base change of φ, and surjective), so regularity, irreducibility and smoothness over the base transfer from φ⁻¹ Z to Z;
• smoothness of the sequence (isSmooth_of_isSmooth_pullback);
• the weak transforms (weakTransformSeq_pullback_mk_of_isOpenImmersion): the induced ideals of S.pullback u are the inverse images of the induced ideals of S under the stage lifts, as for the flat transport of Hironaka/Scheme/BlowUpSequence/WeakTransformFlat.lean, the order along each center of S being read off the pulled-back center through the range condition (the weak transform is the marked transform with the constant order as mark on both sides, and marked transforms commute with flat pull-back). The pull-back of a sequence is that of [Kol07, 30.1].

The closed subscheme of a center in the range of an open immersion

theorem AlgebraicGeometry.isOpenImmersion_subschemeMap_comap {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) [IsOpenImmersion φ] : IsOpenImmersion ((Z.comap φ).subschemeMap Z φ ⋯)

V(φ⁻¹ Z) → V(Z) is an open immersion, the base change of φ.

theorem AlgebraicGeometry.surjective_subschemeMap_comap {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) (hZ : ↑Z.support ⊆ Set.range ⇑φ) : Function.Surjective ⇑((Z.comap φ).subschemeMap Z φ ⋯)

V(φ⁻¹ Z) → V(Z) is surjective when |Z| lies in the range of φ.

theorem AlgebraicGeometry.isIso_subschemeMap_comap_of_subset {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) [IsOpenImmersion φ] (hZ : ↑Z.support ⊆ Set.range ⇑φ) : CategoryTheory.IsIso ((Z.comap φ).subschemeMap Z φ ⋯)

V(φ⁻¹ Z) → V(Z) is an isomorphism when |Z| lies in the range of the open immersion φ (a surjective open immersion); this is Hironaka's u_i(D̄(i)) = D(i).

theorem AlgebraicGeometry.isRegular_subscheme_of_comap {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) [IsOpenImmersion φ] (hZ : ↑Z.support ⊆ Set.range ⇑φ) (h : IsRegular (Z.comap φ).subscheme) : IsRegular Z.subscheme

Regularity of V(Z) from regularity of V(φ⁻¹ Z) (the stalks correspond under the isomorphism).

theorem AlgebraicGeometry.irreducibleSpace_subscheme_of_comap {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) [IsOpenImmersion φ] (hZ : ↑Z.support ⊆ Set.range ⇑φ) (h : IrreducibleSpace ↥(Z.comap φ).subscheme) : IrreducibleSpace ↥Z.subscheme

Irreducibility of V(Z) from irreducibility of V(φ⁻¹ Z).

theorem AlgebraicGeometry.smooth_subschemeι_comp_of_comap {X Y : Scheme} (φ : Y ⟶ X) (Z : X.IdealSheafData) [IsOpenImmersion φ] {W : Scheme} (g : X ⟶ W) (hZ : ↑Z.support ⊆ Set.range ⇑φ) (h : Smooth (CategoryTheory.CategoryStruct.comp (Z.comap φ).subschemeι (CategoryTheory.CategoryStruct.comp φ g))) : Smooth (CategoryTheory.CategoryStruct.comp Z.subschemeι g)

Smoothness of V(Z) → W from smoothness of V(φ⁻¹ Z) → Y → X → W.

Centers in the range of the stage lifts

theorem AlgebraicGeometry.forall_center_of_pullback {X Y : Scheme} (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) (P : {W : Scheme} → W.IdealSheafData → Prop) (hP : ∀ {W W' : Scheme} (φ : W' ⟶ W) [IsOpenImmersion φ] (Z : W.IdealSheafData), ↑Z.support ⊆ Set.range ⇑φ → P (Z.comap φ) → P Z) (hC : S.CentersInRange u) (h : ∀ (i : Fin (S.pullback u).length), P ((S.pullback u).center i)) (i : Fin S.length) : P (S.center i)

A predicate on closed subschemes that transfers from φ⁻¹ Z to Z along open immersions whose range contains |Z| holds on the centers of S once it holds on the centers of S.pullback u, provided the centers of S lie in the ranges of the stage lifts.

theorem AlgebraicGeometry.forall_isRegular_center_of_pullback {X Y : Scheme} (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) (hC : S.CentersInRange u) (h : ∀ (i : Fin (S.pullback u).length), IsRegular ((S.pullback u).center i).subscheme) (i : Fin S.length) : IsRegular (S.center i).subscheme

Regular centers transfer from S.pullback u to S.

theorem AlgebraicGeometry.forall_irreducibleSpace_center_of_pullback {X Y : Scheme} (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) (hC : S.CentersInRange u) (h : ∀ (i : Fin (S.pullback u).length), IrreducibleSpace ↥((S.pullback u).center i).subscheme) (i : Fin S.length) : IrreducibleSpace ↥(S.center i).subscheme

Irreducible centers transfer from S.pullback u to S.

theorem AlgebraicGeometry.isSmooth_of_isSmooth_pullback {X Y : Scheme} (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) {k : Type u} [Field k] (f : X ⟶ Spec ↧k) (hC : S.CentersInRange u) (h : (S.pullback u).IsSmooth (CategoryTheory.CategoryStruct.comp u f)) : S.IsSmooth f

A sequence whose pull-back along u is smooth over k is smooth over k when its centers lie in the ranges of the stage lifts: each center's closed subscheme is isomorphic to that of the pulled-back center.

The weak transforms along the stage lifts

theorem AlgebraicGeometry.weakTransformSeq_pullback_mk_of_isOpenImmersion {X Y : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) (hC : S.CentersInRange u) (hsm : S.IsSmooth f) (I : X.IdealSheafData) (hpt : ∀ (j : ℕ) (hj : j < S.length), ∃ (c : ℕ), ∀ y ∈ ((S.pullback u).center (S.pullbackCenterIdx u ⟨j, hj⟩)).support, ((S.pullback u).weakTransformSeq (I.comap u) (S.pullbackStageIdx u ⟨j, ⋯⟩)).ord y = ↑c) (j : ℕ) (hj : j < S.length + 1) : (S.pullback u).weakTransformSeq (I.comap u) (S.pullbackStageIdx u ⟨j, hj⟩) = (S.weakTransformSeq I ⟨j, hj⟩).comap (S.pullbackStageHom u ⟨j, hj⟩)

Along an open immersion u whose stage lifts contain the centers of the smooth sequence S, if every induced ideal of S.pullback u has constant order on the corresponding center, the induced ideals of S.pullback u are the inverse images of the induced ideals of S under the stage lifts (the flat transport of Hironaka/Scheme/BlowUpSequence/WeakTransformFlat.lean, with the order along each center read off the pulled-back center).

theorem AlgebraicGeometry.weakTransformSeq_pullback_of_isOpenImmersion {X Y : Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ Spec ↧k) (n : ℕ) [SmoothOfRelativeDimension n f] (u : Y ⟶ X) [IsOpenImmersion u] (S : X.BlowUpSequence) (hC : S.CentersInRange u) (hsm : S.IsSmooth f) (I : X.IdealSheafData) (hpt : ∀ (j : ℕ) (hj : j < S.length), ∃ (c : ℕ), ∀ y ∈ ((S.pullback u).center (S.pullbackCenterIdx u ⟨j, hj⟩)).support, ((S.pullback u).weakTransformSeq (I.comap u) (S.pullbackStageIdx u ⟨j, ⋯⟩)).ord y = ↑c) (i : Fin (S.length + 1)) : (S.pullback u).weakTransformSeq (I.comap u) (S.pullbackStageIdx u i) = (S.weakTransformSeq I i).comap (S.pullbackStageHom u i)

The Fin-indexed form of weakTransformSeq_pullback_mk_of_isOpenImmersion.