Extension of a blow-up sequence across the complement of an open subscheme

In the proof of Corollary 1 of Main Theorem II [Hir64, p. 144], a finite succession of monoidal transformations on the open subscheme X̄ = X ∖ S whose centers D̄(i) are mapped into the closed subset T − S of X is extended to a finite succession f_i : X(i+1) → X(i) on X itself, with centers D(i) and open immersions u_i : X̄(i) → X(i) such that "u_i(D̄(i)) = D(i) and u_i ∘ f̄_i = f_i ∘ u_{i+1}". This module proves that extension in general:

• The closedness ground: a subset of U closed in U whose image under the open immersion u : U ⟶ X lies in a closed C ⊆ u(U) has closed image in X (isClosed_image_of_isOpenImmersion); its closure stays inside C ⊆ u(U), where u is an embedding.
• The extended center: for a center D on U with closed image, the ideal sheaf D.map u = ker (D.subschemeι ≫ u) of X (Mathlib's push-forward; the composite is a closed immersion, isClosedImmersion_subschemeι_comp) has support u(D) (support_map_of_isClosed) and restricts to D on U (comap_map_of_isClosed).
• The extension extendOfOpen u S' C h, by recursion on S': the first center is extended, the next open immersion is the base change blowUpMap u (D.map u) of the blow-up (an open immersion with image π⁻¹(u(U)), [TSPA, Tag 0805]; the blow-up maps form a pullback square, isPullback_blowUpMap) transported along (D.map u).comap u = D, and the tail is extended over the preimage of C. Its pull-back along u is S' (pullback_extendOfOpen: Hironaka's u_i(D̄(i)) = D(i) and u_i ∘ f̄_i = f_i ∘ u_{i+1}, the defining squares of the pull-back) and its centers lie over C (stageMap_extendOfOpen_mem).
• exists_extend_of_isOpenImmersion is the existential form.

The closedness ground

theorem Hironaka.Sequence.isClosed_image_of_isOpenImmersion {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] {A : Set ↥U} (hA : IsClosed A) {C : Set ↥X} (hC : IsClosed C) (hCU : C ⊆ Set.range ⇑u) (hAC : ⇑u '' A ⊆ C) : IsClosed (⇑u '' A)

A subset A closed in U whose image under the open immersion u lies in a closed C ⊆ u(U) has closed image: the closure of u(A) lies in C, hence in u(U), where u is an embedding and A is closed.

The extended center

theorem Hironaka.Sequence.isClosedImmersion_subschemeι_comp {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (h : IsClosed (⇑u '' ↑D.support)) : AlgebraicGeometry.IsClosedImmersion (CategoryTheory.CategoryStruct.comp D.subschemeι u)

The closed subscheme D of U with closed image in X is a closed subscheme of X: the composite D ⟶ U ⟶ X is a preimmersion with closed range.

theorem Hironaka.Sequence.support_map_of_isClosed {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (h : IsClosed (⇑u '' ↑D.support)) : ↑(D.map u).support = ⇑u '' ↑D.support

The support of the extended center is the image of the support.

theorem Hironaka.Sequence.comap_map_of_isClosed {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (h : IsClosed (⇑u '' ↑D.support)) : (D.map u).comap u = D

The extended center restricts to the center, (D.map u).comap u = D: Mathlib's ker_ideal_of_isPullback_of_isOpenImmersion on the square with the identity, which is cartesian because u is a monomorphism.

The extension

structure Hironaka.Sequence.ExtendsOver {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) (S' : U.BlowUpSequence) (C : Set ↥X) : Prop

The data under which a sequence S' on U extends across the complement of the open immersion u : U ⟶ X: a closed C ⊆ u(U) over which every center lies (Hironaka's T − S).

• isClosed : IsClosed C

  C is closed in X.

• subset_range : C ⊆ Set.range ⇑u

  C lies in the image of u.

• center_mem (i : Fin S'.length) (y : ↥(S'.stage i.castSucc)) : y ∈ (S'.center i).support → u ((S'.stageMap i.castSucc) y) ∈ C

  Every center maps into C.

theorem Hironaka.Sequence.ExtendsOver.image_subset {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : ⇑u '' ↑D.support ⊆ C

The first center maps into C.

theorem Hironaka.Sequence.ExtendsOver.isClosed_image {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : IsClosed (⇑u '' ↑D.support)

The first center has closed image.

theorem Hironaka.Sequence.ExtendsOver.comap_map {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : (D.map u).comap u = D

noncomputable def Hironaka.Sequence.extendStep {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : D.blowUp ⟶ (D.map u).blowUp

Hironaka's next open immersion u_{i+1}: the base change of u to the blow-ups, transported along (D.map u).comap u = D.

Equations

• Hironaka.Sequence.extendStep u D rest C h = CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (AlgebraicGeometry.Scheme.Hom.blowUpMap u (D.map u))

theorem Hironaka.Sequence.isPullback_extendStep {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : CategoryTheory.IsPullback (extendStep u D rest C h) D.blowUpπ (D.map u).blowUpπ u

The square of extendStep over u is cartesian: the eqToHom square pasted with the base-change square of the blow-up (isPullback_blowUpMap).

theorem Hironaka.Sequence.isOpenImmersion_extendStep {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : AlgebraicGeometry.IsOpenImmersion (extendStep u D rest C h)

theorem Hironaka.Sequence.extendStep_π {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : CategoryTheory.CategoryStruct.comp (extendStep u D rest C h) (D.map u).blowUpπ = CategoryTheory.CategoryStruct.comp D.blowUpπ u

theorem Hironaka.Sequence.range_extendStep {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : Set.range ⇑(extendStep u D rest C h) = ⇑(D.map u).blowUpπ ⁻¹' Set.range ⇑u

theorem Hironaka.Sequence.ExtendsOver.tailStep {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : ExtendsOver (extendStep u D rest C h) rest (⇑(D.map u).blowUpπ ⁻¹' C)

The tail extends over the preimage of C.

noncomputable def Hironaka.Sequence.extendOfOpen {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (S' : U.BlowUpSequence) (C : Set ↥X) : ExtendsOver u S' C → X.BlowUpSequence

The extension of a sequence on U across the complement of the open immersion u [Hir64, Corollary 1 of Main Theorem II, p. 144], by recursion: the first center extended by D.map u, the next open immersion extendStep, the tail extended over the preimage of C.

Equations

• One or more equations did not get rendered due to their size.
• Hironaka.Sequence.extendOfOpen x✝³ (AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝⁵) x✝¹ x✝ = AlgebraicGeometry.Scheme.BlowUpSequence.nil x✝⁴

theorem Hironaka.Sequence.extendOfOpen_nil {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.nil U) C) : extendOfOpen u (AlgebraicGeometry.Scheme.BlowUpSequence.nil U) C h = AlgebraicGeometry.Scheme.BlowUpSequence.nil X

theorem Hironaka.Sequence.extendOfOpen_cons {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (D : U.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C) : extendOfOpen u (AlgebraicGeometry.Scheme.BlowUpSequence.cons U D rest) C h = AlgebraicGeometry.Scheme.BlowUpSequence.cons X (D.map u) (extendOfOpen (extendStep u D rest C h) rest (⇑(D.map u).blowUpπ ⁻¹' C) ⋯)

theorem Hironaka.Sequence.length_extendOfOpen {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (S' : U.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u S' C) : (extendOfOpen u S' C h).length = S'.length

theorem Hironaka.Sequence.pullback_eqToHom_pullback_eqToHom_symm {X X' : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (e : X' = X) : (S.pullback (CategoryTheory.eqToHom e)).pullback (CategoryTheory.eqToHom ⋯) = S

Pulling back along eqToHom and its inverse is the identity.

theorem Hironaka.Sequence.pullback_extendOfOpen {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (S' : U.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u S' C) : (extendOfOpen u S' C h).pullback u = S'

The pull-back of the extension along u is the sequence (Hironaka's "u_i(D̄(i)) = D(i) and u_i ∘ f̄_i = f_i ∘ u_{i+1}", [Hir64, p. 144]): the extended center restricts to the center, and the pull-back's next stage map is extendStep up to the transport.

theorem Hironaka.Sequence.stageMap_extendOfOpen_mem {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (S' : U.BlowUpSequence) (C : Set ↥X) (h : ExtendsOver u S' C) (i : Fin (extendOfOpen u S' C h).length) (x : ↥((extendOfOpen u S' C h).stage i.castSucc)) : x ∈ ((extendOfOpen u S' C h).center i).support → ((extendOfOpen u S' C h).stageMap i.castSucc) x ∈ C

The centers of the extension lie over C.

The existential form

theorem Hironaka.Sequence.exists_extend_of_isOpenImmersion {U X : AlgebraicGeometry.Scheme} (u : U ⟶ X) [AlgebraicGeometry.IsOpenImmersion u] (S' : U.BlowUpSequence) (C : Set ↥X) (hC : IsClosed C) (hCU : C ⊆ Set.range ⇑u) (hcent : ∀ (i : Fin S'.length), ∀ y ∈ (S'.center i).support, u ((S'.stageMap i.castSucc) y) ∈ C) : ∃ (S : X.BlowUpSequence), S.pullback u = S' ∧ ∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, (S.stageMap i.castSucc) x ∈ C

A sequence on an open subscheme whose centers lie over a closed subset of the image extends across the complement [Hir64, Corollary 1 of Main Theorem II, p. 144]: the existential form of extendOfOpen, pullback_extendOfOpen and stageMap_extendOfOpen_mem.