The strict transforms along a sequence lie over each other

In the restriction of a blow-up sequence to a closed subscheme [Kol07, 30.2] the strict transform S_{i+1} ⊆ X_{i+1} of S_i ⊆ X_i maps into S_i. Along a blow-up sequence, a point of the strict transform X̄_i at stage i therefore maps to a point of the strict transform X̄_j at every earlier stage j ≤ i, and to V(J) at stage 0. The one-blow-up step is the description of the support of the strict transform as the closure of π⁻¹(V(J)) ∖ π⁻¹(V(D)) (coe_support_strictTransform), which lies in the closed set π⁻¹(V(J)).

• stageMap_mem_support_of_mem_support_strictTransformSeq: Π_i(X̄_i) ⊆ V(J).
• stageMapBetween_mem_support_strictTransformSeq: the stage maps carry X̄_i into X̄_j.

Used for clause (3) of [Kol07, Theorem 36]: a point of the end result X̄_r over an earlier center Z_m lies over the restricted center Z_m ∩ X̄_m.

theorem Hironaka.Sequence.blowUpπ_mem_support_of_mem_support_strictTransform {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (D J : X.IdealSheafData) {x' : ↥D.blowUp} (hx' : x' ∈ (J.strictTransform D).support) : D.blowUpπ x' ∈ J.support

One blow-up: a point of the strict transform of J maps to V(J) (coe_support_strictTransform: the support is the closure of a subset of π⁻¹(V(J))).

theorem Hironaka.Sequence.stageMap_mem_support_of_mem_support_strictTransformSeq_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) [AlgebraicGeometry.IsLocallyNoetherian X] (J : X.IdealSheafData) (j : ℕ) (hj : j < S.length + 1) (p : ↥(S.stage ⟨j, hj⟩)) : p ∈ (S.strictTransformSeq J ⟨j, hj⟩).support → (S.stageMap ⟨j, hj⟩) p ∈ J.support

[Kol07, 30.2] along a sequence (⟨j, hj⟩ form): Π_j maps the strict transform X̄_j of V(J) into V(J).

theorem Hironaka.Sequence.stageMap_mem_support_of_mem_support_strictTransformSeq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) (i : Fin (S.length + 1)) {p : ↥(S.stage i)} (hp : p ∈ (S.strictTransformSeq J i).support) : (S.stageMap i) p ∈ J.support

[Kol07, 30.2] along a sequence: Π_i maps the strict transform X̄_i of V(J) into V(J).

theorem Hironaka.Sequence.stageMapBetween_mem_support_strictTransformSeq_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) [AlgebraicGeometry.IsLocallyNoetherian X] (J : X.IdealSheafData) (i j : ℕ) (hi : i < S.length + 1) (hj : j < S.length + 1) (hji : j ≤ i) (p : ↥(S.stage ⟨i, hi⟩)) : p ∈ (S.strictTransformSeq J ⟨i, hi⟩).support → (S.stageMapBetween ⟨i, hi⟩ ⟨j, hj⟩ hji) p ∈ (S.strictTransformSeq J ⟨j, hj⟩).support

[Kol07, 30.2] along a sequence (⟨j, hj⟩ form): the stage map from stage i to an earlier stage j carries the strict transform X̄_i into X̄_j.

theorem Hironaka.Sequence.stageMapBetween_mem_support_strictTransformSeq {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : X.BlowUpSequence) (J : X.IdealSheafData) {i j : Fin (S.length + 1)} (hji : j ≤ i) {p : ↥(S.stage i)} (hp : p ∈ (S.strictTransformSeq J i).support) : (S.stageMapBetween i j hji) p ∈ (S.strictTransformSeq J j).support

[Kol07, 30.2] along a sequence: the stage map from stage i to an earlier stage j carries the strict transform X̄_i of V(J) into X̄_j.