Points of the centers under pull-back and under the deletion of empty blow-ups

The set of points of the base over which some center of a blow-up sequence has a point is unchanged by the deletion of the empty blow-ups (the empty blow-up convention of [Kol07, 32]: empty blow-ups "are then ignored"), and it moves along a flat pull-back as restrictedCenterHasPointOver_pullback_iff of Hironaka/Scheme/BlowUpSequence/RestrictedCenters.lean says. These are the facts about the centers that the resolution of an affine scheme needs when its sequence is compared with the sequence of an open piece.

The predicate is RestrictedCenterHasPointOver S J i x at the zero ideal J = ⊥: the strict transform of ⊥ is ⊥ (strictTransformSeq_bot), whose support is everything, so the predicate reads "the center Z_i has a point over x" (restrictedCenterHasPointOver_bot_iff). Along cons X D rest the base points are those of D and the images under D.blowUpπ of the base points of rest (exists_restrictedCenterHasPointOver_bot_cons_iff); the deletion keeps a nonempty first center and, for an empty one (D = ⊤, no base point), carries the tail back along the isomorphism inv (blowUpπ X ⊤), which is a flat pull-back (exists_restrictedCenterHasPointOver_bot_eraseEmpty_iff).

theorem Hironaka.Sequence.restrictedCenterHasPointOver_bot_iff {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (i : Fin S.length) (x : ↥X) : AlgebraicGeometry.RestrictedCenterHasPointOver S ⊥ i x ↔ ∃ p ∈ (S.center i).support, (S.stageMap i.castSucc) p = x

At the zero ideal the restricted-center predicate reads "the center Z_i has a point over x": the strict transform of ⊥ is ⊥ (strictTransformSeq_bot), whose support is the whole stage.

theorem Hironaka.Sequence.exists_restrictedCenterHasPointOver_pullback_iff {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (J : X.IdealSheafData) (y : ↥Y) : (∃ (i : Fin (S.pullback h).length), AlgebraicGeometry.RestrictedCenterHasPointOver (S.pullback h) (J.comap h) i y) ↔ ∃ (i : Fin S.length), AlgebraicGeometry.RestrictedCenterHasPointOver S J i (h y)

Some restricted center of the pull-back along a flat h has a point over y iff some restricted center of S has a point over h y (restrictedCenterHasPointOver_pullback_iff with the index bijection pullbackCenterIdx).

theorem Hironaka.Sequence.exists_restrictedCenterHasPointOver_bot_cons_iff {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (x : ↥X) : (∃ (i : Fin (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest).length), AlgebraicGeometry.RestrictedCenterHasPointOver (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) ⊥ i x) ↔ x ∈ D.support ∨ ∃ (q : ↥D.blowUp), D.blowUpπ q = x ∧ ∃ (j : Fin rest.length), AlgebraicGeometry.RestrictedCenterHasPointOver rest ⊥ j q

The base points under some center of cons X D rest are the points of D and the images under D.blowUpπ of the base points under some center of rest.

theorem Hironaka.Sequence.exists_restrictedCenterHasPointOver_bot_eraseEmpty_iff {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (x : ↥X) : (∃ (i : Fin S.eraseEmpty.length), AlgebraicGeometry.RestrictedCenterHasPointOver S.eraseEmpty ⊥ i x) ↔ ∃ (i : Fin S.length), AlgebraicGeometry.RestrictedCenterHasPointOver S ⊥ i x

Deleting the empty blow-ups [Kol07, 32] leaves the set of base points under some center unchanged: an empty first center (D = ⊤) has no base point and its tail is carried back along the isomorphism inv (blowUpπ X ⊤), a flat pull-back; a nonempty first center is kept.