Restricted centers and their points over the base

The restriction of a blow-up sequence on A to a closed subscheme X ⊆ A [Kol07, 30.2] intersects the centers Z_i with the birational transforms X̄_i. In the proof that the resolution of a quasi-projective variety is an isomorphism over the smooth locus ([Kol07, Theorem 36 (2)], following the proof of [Kol07, Theorem 27] and the locality of functorial resolutions in [Kol07, 4.2]), the statement "the restricted center Z_i ∩ X̄_i has a point over the point x of X" is transported along the functoriality of the whole sequence under a smooth surjection (the first clause of [Kol07, 34.1]). This module holds that bookkeeping, for arbitrary schemes:

• take_pullback: truncation commutes with pullback, (S.take k).pullback h = (S.pullback h).take k, a structural induction, so that a statement about the pulled-back whole sequence restricts to its first j steps;
• RestrictedCenterHasPointOver S J i x: the i-th center of S meets the i-th strict transform of V(J) at a point lying over x, i.e. Kollár's restricted center Z_i ∩ X̄_i has a point over x;
• restrictedCenterHasPointOver_pullback_iff: along a flat h : Y ⟶ X the predicate for the pulled-back sequence at y is the predicate for S at h y: the stage square X_i ×_X Y is cartesian (isPullback_pullbackStageHom), the centers and strict transforms pull back (center_pullback, strictTransformSeq_pullback), and a point of the fibre product exists over every compatible pair (Scheme.exists_preimage_of_isPullback);
• restrictedCenterHasPointOver_iff_of_isClosedImmersion: along a closed immersion emb : X ⟶ A the centers of the restriction S.pullback emb have a point over x ∈ X iff the restricted center of S has a point over emb x: the stage lift X_i ↪ A_i is a closed immersion onto the strict transform (isClosedImmersion_pullbackStageHom, ker_pullbackStageHom).

Truncation commutes with pullback

theorem AlgebraicGeometry.take_pullback {X : Scheme} (S : X.BlowUpSequence) {Y : Scheme} (h : Y ⟶ X) (k : ℕ) : (S.take k).pullback h = (S.pullback h).take k

The pullback of the first k blow-ups is the first k blow-ups of the pullback.

The restricted center has a point over the base point

def AlgebraicGeometry.RestrictedCenterHasPointOver {X : Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (i : Fin S.length) (x : ↥X) : Prop

The restricted center Z_i ∩ X̄_i of [Kol07, 30.2] of the sequence S relative to the closed subscheme V(J) has a point over x: a point of the i-th stage lying in the center Z_i, in the i-th strict transform of V(J), and over x under the stage map Π_i.

Equations

• AlgebraicGeometry.RestrictedCenterHasPointOver S J i x = ∃ p ∈ (S.center i).support, p ∈ (S.strictTransformSeq J i.castSucc).support ∧ (S.stageMap i.castSucc) p = x

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

Along a flat h : Y ⟶ X, the restricted center of the pulled-back sequence relative to h⁻¹(V(J)) has a point over y iff the restricted center of S relative to V(J) has a point over h y: the stage squares are cartesian (isPullback_pullbackStageHom), so the points of the pulled-back stage over y are exactly the points of X_i ×_X Y over the points of X_i over h y.

The restriction to a closed subscheme

theorem AlgebraicGeometry.restrictedCenterHasPointOver_iff_of_isClosedImmersion {X Y : Scheme} (S : X.BlowUpSequence) (emb : Y ⟶ X) [IsClosedImmersion emb] (i : Fin S.length) (y : ↥Y) : (∃ p ∈ ((S.pullback emb).center (S.pullbackCenterIdx emb i)).support, ((S.pullback emb).stageMap (S.pullbackCenterIdx emb i).castSucc) p = y) ↔ RestrictedCenterHasPointOver S (Scheme.Hom.ker emb) i (emb y)

Along a closed immersion emb : X ⟶ A, the i-th center of the restriction S.pullback emb has a point over x ∈ X iff the restricted center Z_i ∩ X̄_i of S relative to V(emb.ker) has a point over emb x [Kol07, 30.2]: the stage lift X_i ↪ A_i is a closed immersion whose image is the strict transform X̄_i (isClosedImmersion_pullbackStageHom, ker_pullbackStageHom).