Centres missing a subset of the base, and sequences with empty centres

Clause (b) of Włodarczyk's embedded desingularization theorem [Wlo05, Theorem 1.0.2] says that all centres are disjoint from the set of points where the subvariety Y is smooth. For the embedded desingularization sequence of Hironaka.Resolution.Algebraic.Wlo05.Embedded it is proved locally, on an affine open of X meeting Y in one smooth component, by Włodarczyk's remark that "the generic points would be transformed isomorphically" [Wlo05, 4.6]. This file holds the general facts about blow-up sequences used in that argument, none of which mentions the loop:

• CentersMiss S U: no point of a centre of S lies over the set U ⊆ X; its rules for cons, concat and take, and the case of a sequence of order ≥ 1 whose ideal's support misses U (stageMap_mem_support_of_mem_center);
• centerContains_take_iff: the predicate CenterContains on a prefix is the predicate on the sequence, at indices below the prefix length;
• exists_mem_center_support_of_eraseEmpty_eq_cons: a point of the first centre of S.eraseEmpty is the image of a point of the first nonempty centre of S, all earlier centres being empty (the deletion of empty blow-ups, [Kol07, 32]);
• the transforms along a sequence all of whose centres are empty: marked and strict transforms are the inverse images (markedTransform_top_left, strictTransform_top_left), the total transform of a family with empty members has empty members (exceptionalDivisor_top), and the stage maps are isomorphisms (isIso_stageMap_of_center_eq_top);
• center_pullback_eq_top_iff: a centre of the pullback along a flat h is empty if and only if no point of the centre lies over the image of h [Kol07, Definition 30, 30.1];
• isGenericPoint_of_mem_genericPoints_comap: the image under an open immersion of a generic point of h⁻¹ V(Z), for an irreducible V(Z), is the generic point of V(Z).

Centres missing a subset of the base

def Hironaka.Resolution.CentersMiss {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (U : Set ↥X) : Prop

No centre of S has a point over U ⊆ X. For U the set of smooth points of a subvariety Y this is clause (b) of [Wlo05, Theorem 1.0.2]: "all centers are disjoint from Reg(Y)".

Equations

• Hironaka.Resolution.CentersMiss S U = ∀ (i : Fin S.length), ∀ x ∈ (S.center i).support, (S.stageMap i.castSucc) x ∉ U

def Hironaka.Resolution.CentersMissBefore {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (U : Set ↥X) (n : ℕ) : Prop

CentersMiss for the centres of index < n only.

Equations

• Hironaka.Resolution.CentersMissBefore S U n = ∀ (i : Fin S.length), ↑i < n → ∀ x ∈ (S.center i).support, (S.stageMap i.castSucc) x ∉ U

theorem Hironaka.Resolution.centersMiss_nil {X : AlgebraicGeometry.Scheme} (U : Set ↥X) : CentersMiss (AlgebraicGeometry.Scheme.BlowUpSequence.nil X) U

theorem Hironaka.Resolution.centersMiss_cons_iff {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (U : Set ↥X) : CentersMiss (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) U ↔ (∀ x ∈ D.support, x ∉ U) ∧ CentersMiss rest (⇑D.blowUpπ ⁻¹' U)

CentersMiss on a cons: the first centre misses U and the tail misses its preimage under the first blow-up.

theorem Hironaka.Resolution.centersMiss_concat {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (T : S.last.BlowUpSequence) (U : Set ↥X) : CentersMiss S U → CentersMiss T (⇑S.composite ⁻¹' U) → CentersMiss (S.concat T) U

CentersMiss on a concatenation (the composites Π_{ij} of [Kol07, Definition 29]): the first piece misses U and the second misses the preimage of U under the composite of the first.

theorem Hironaka.Resolution.centersMiss_take_of_centersMissBefore {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (U : Set ↥X) (n : ℕ) : CentersMissBefore S U n → CentersMiss (S.take n) U

The prefix S.take n misses U when the centres of S of index < n do.

theorem Hironaka.Resolution.centersMiss_of_isOrderGeSeq {X : AlgebraicGeometry.Scheme} {k : Type u} [Field k] [CharZero k] (f : X ⟶ AlgebraicGeometry.Spec ↧k) (n : ℕ) [AlgebraicGeometry.SmoothOfRelativeDimension n f] {S : X.BlowUpSequence} {I : X.IdealSheafData} {E : X.DivisorFamily} {m : ℕ} (hS : S.IsOrderGeSeq f I m E) (hm : 1 ≤ m) (U : Set ↥X) (hU : ∀ x ∈ I.support, x ∉ U) : CentersMiss S U

The centres of a sequence of order ≥ m ≥ 1 for (I, E) lie over V(I) Kol07, Definition 60 (stageMap_mem_support_of_mem_center), so they miss every set disjoint from V(I).

The stop rule on a prefix

theorem Hironaka.Resolution.centerContains_cons_succ_iff {X : AlgebraicGeometry.Scheme} (D : X.IdealSheafData) (rest : D.blowUp.BlowUpSequence) (c : X.IdealSheafData) (i : ℕ) : CenterContains (AlgebraicGeometry.Scheme.BlowUpSequence.cons X D rest) c (i + 1) ↔ CenterContains rest (c.strictTransform D) i

The predicate CenterContains on a cons at a positive index is the predicate on the tail for the strict transform.

theorem Hironaka.Resolution.centerContains_take_iff {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (c : X.IdealSheafData) (n i : ℕ) : i < n → (CenterContains (S.take n) c i ↔ CenterContains S c i)

The predicate CenterContains at an index below n on the prefix S.take n is the predicate on S.

The first centre of eraseEmpty

theorem Hironaka.Resolution.exists_mem_center_support_of_eraseEmpty_eq_cons {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) {D₀ : X.IdealSheafData} {rest₀ : D₀.blowUp.BlowUpSequence} : S.eraseEmpty = AlgebraicGeometry.Scheme.BlowUpSequence.cons X D₀ rest₀ → ∀ {q : ↥X}, q ∈ D₀.support → ∃ (n : ℕ) (hn : n < S.length), ∃ q' ∈ (S.center ⟨n, hn⟩).support, (S.stageMap ⟨n, ⋯⟩) q' = q ∧ ∀ (i : ℕ) (hi : i < n), S.center ⟨i, ⋯⟩ = ⊤

The deletion of empty blow-ups [Kol07, 32]: a point q of the first centre of S.eraseEmpty is the image of a point q' of the first nonempty centre of S, at an index n all of whose predecessors are empty centres.

Sequences all of whose centres are empty

theorem Hironaka.Resolution.markedTransformSeq_eq_comap_of_forall_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : (∀ (i : Fin S.length), S.center i = ⊤) → ∀ (K : X.IdealSheafData) (m : ℕ) (i : Fin (S.length + 1)), S.markedTransformSeq K m i = K.comap (S.stageMap i)

Along a sequence all of whose centres are empty the marked transform of K is its inverse image under the stage map (markedTransform_top_left at every step).

theorem Hironaka.Resolution.strictTransformSeq_eq_comap_of_forall_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : (∀ (i : Fin S.length), S.center i = ⊤) → ∀ (K : X.IdealSheafData) (i : Fin (S.length + 1)), S.strictTransformSeq K i = K.comap (S.stageMap i)

Along a sequence all of whose centres are empty the strict transform of K is its inverse image under the stage map (strictTransform_top_left at every step).

theorem Hironaka.Resolution.totalTransformSeq_component_eq_top_of_forall_center_eq_top {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) : (∀ (i : Fin S.length), S.center i = ⊤) → ∀ (E : X.DivisorFamily), (∀ (e : E.ι), E.component e = ⊤) → ∀ (i : Fin (S.length + 1)) (e : (S.totalTransformSeq E i).ι), (S.totalTransformSeq E i).component e = ⊤

Along a sequence all of whose centres are empty, the total transform of a family all of whose members are empty has only empty members (strictTransform_top_right, exceptionalDivisor_top).

Empty centres of a pullback

theorem Hironaka.Resolution.center_pullback_eq_top_iff {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (j : ℕ) (hj : j < S.length) : (S.pullback h).center (S.pullbackCenterIdx h ⟨j, hj⟩) = ⊤ ↔ ∀ x ∈ (S.center ⟨j, hj⟩).support, (S.stageMap ⟨j, ⋯⟩) x ∉ Set.range ⇑h

The pullback of a blow-up sequence [Kol07, Definition 30, 30.1], read pointwise: a centre of the pullback along a flat h is empty if and only if no point of the centre of S lies over the image of h (center_pullback_mk, range_pullbackStageHom).

theorem Hironaka.Resolution.forall_center_pullback_eq_top_of_centersMiss {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (hmiss : CentersMiss S (Set.range ⇑h)) (i : Fin (S.pullback h).length) : (S.pullback h).center i = ⊤

All centres of the pullback along a flat h are empty when the centres of S miss the image of h.

theorem Hironaka.Resolution.centersMissBefore_of_forall_center_pullback_eq_top {X Y : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (h : Y ⟶ X) [AlgebraicGeometry.Flat h] (n : ℕ) (htop : ∀ i < n, ∀ (hi' : i < S.length), (S.pullback h).center (S.pullbackCenterIdx h ⟨i, hi'⟩) = ⊤) : CentersMissBefore S (Set.range ⇑h) n

The centres of S of index < n miss the image of h when the corresponding centres of the pullback are empty.

Generic points along an open immersion

theorem Hironaka.Resolution.isIrreducible_support_of_isIntegral {X : AlgebraicGeometry.Scheme} (Z : X.IdealSheafData) [AlgebraicGeometry.IsIntegral Z.subscheme] : IsIrreducible ↑Z.support

The support of an integral closed subscheme is an irreducible closed subset.

theorem Hironaka.Resolution.isGenericPoint_of_mem_genericPoints_comap {X W : AlgebraicGeometry.Scheme} (j : W ⟶ X) [AlgebraicGeometry.IsOpenImmersion j] (Z : X.IdealSheafData) (hirr : IsIrreducible ↑Z.support) {w : ↥W} (hw : w ∈ (Z.comap j).support.genericPoints) : IsGenericPoint (j w) ↑Z.support

The generic point seen on an open [Kol07, Corollary 22, proof]: for an open immersion j and an irreducible V(Z), the image of a generic point of j⁻¹ V(Z) (Closeds.genericPoints) is the generic point of V(Z). The generic point ξ of V(Z) generalises j w, so it lies in the open image of j, and an open embedding reflects specialisation.