No restricted centre over a smooth point

Kollár's argument that a functorial resolution is an isomorphism over the smooth locus [Kol07, 4.2; Theorem 27, proof]: a resolution is birational, hence an isomorphism over some smooth point; any two smooth points are étale equivalent; and a resolution functorial under étale morphisms therefore is an isomorphism over every smooth point. For the resolution of an embedded affine scheme, the truncated restriction ((BP TA).take j).pullback emb of Hironaka.Resolution.Algebraic.Kol07.Thm36.Affine, the statement transported is that no restricted centre Z_i ∩ X̄_i, i < j, has a point over x (RestrictedCenterHasPointOver), and the functoriality used is that of the whole principalization sequence under smooth surjections Kol07, Theorem 35 (4); 34.1. Two smooth points of X are made étale equivalent as embedded points by an étale pair ψ, ψ' : W ⟶ A over k with the same inverse image of I_X, and the pair is completed to surjective étale maps (exists_completion_isPullbackOf) so that the functoriality applies.

The theorems are stated for an arbitrary assignment F of a blow-up sequence to every triple that is functorial under smooth surjections (the hypothesis hfun), and for a truncation index j such that no restricted centre has a point over the generic point of X (the hypothesis ha); they are applied to F := BP at the first-centre index in Hironaka.Resolution.Algebraic.Kol07.Thm36.AffineTheorem36IsoSnc.

Main results

• isClosed_setOf_restrictedCenterHasPointOver: the set of points of X over which some restricted centre has a point is closed, being the finite union of the images of the closed centres of the restriction under its proper stage maps.
• restrictedCenterHasPointOver_iff_of_etale_pair: along an étale pair ψ, ψ' as above, the predicate at ψ q is equivalent to the predicate at ψ' q.
• not_restrictedCenterHasPointOver_of_mem_smoothLocus: for an integral X, if no restricted centre has a point over the generic point of X, then none has a point over any point of the smooth locus of X. Closed points of the finite-type scheme X meet every nonempty locally closed subset (Jacobson), which reduces the statement to closed points; the étale pair is taken on the open U₁ = A ∖ emb(X ∖ X^{ns}), over which X ∩ U₁ = X^{ns} is smooth of one relative dimension, between a closed point of X^{ns} outside the closed exceptional set and any closed point of X^{ns}.

Bookkeeping

theorem Hironaka.Resolution.restrictedCenterHasPointOver_congr {Y : AlgebraicGeometry.Scheme} {S₁ S₂ : Y.BlowUpSequence} (e : S₁ = S₂) {J₁ J₂ : Y.IdealSheafData} (eJ : J₁ = J₂) {i₁ : Fin S₁.length} {i₂ : Fin S₂.length} (hi : ↑i₁ = ↑i₂) (y : ↥Y) : AlgebraicGeometry.RestrictedCenterHasPointOver S₁ J₁ i₁ y ↔ AlgebraicGeometry.RestrictedCenterHasPointOver S₂ J₂ i₂ y

The predicate RestrictedCenterHasPointOver along an equality of sequences and of ideal sheaves, with indices of the same value.

theorem Hironaka.Resolution.isClosed_setOf_restrictedCenterHasPointOver {A X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsLocallyNoetherian X] (S : A.BlowUpSequence) (emb : X ⟶ A) [AlgebraicGeometry.IsClosedImmersion emb] : IsClosed {x : ↥X | ∃ (i : Fin S.length), AlgebraicGeometry.RestrictedCenterHasPointOver S (AlgebraicGeometry.Scheme.Hom.ker emb) i (emb x)}

The set of points of the closed subscheme X over which some restricted centre has a point is closed: it is the finite union of the images of the (closed) centres of the restriction of the sequence to X under the proper stage maps Kol07, Definition 30, 30.2, with the properness of the stage maps.

theorem Hironaka.Resolution.exists_mem_support_iff_of_heq {X Y₁ Y₂ : AlgebraicGeometry.Scheme} (e : Y₁ = Y₂) {c₁ : Y₁.IdealSheafData} {c₂ : Y₂.IdealSheafData} (hc : c₁ ≍ c₂) {t₁ : Y₁.IdealSheafData} {t₂ : Y₂.IdealSheafData} (ht : t₁ ≍ t₂) {f₁ : Y₁ ⟶ X} {f₂ : Y₂ ⟶ X} (hf : f₁ ≍ f₂) (x : ↥X) : (∃ p ∈ c₁.support, p ∈ t₁.support ∧ f₁ p = x) ↔ ∃ p ∈ c₂.support, p ∈ t₂.support ∧ f₂ p = x

The predicate, on data given up to equality of the stage and heterogeneous equality of the centre, the strict transform and the stage map (the shape of the transport lemmas for truncated sequences in Hironaka.Scheme.BlowUpSequence.Truncate).

theorem Hironaka.Resolution.restrictedCenterHasPointOver_take_mk {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (k m : ℕ) (hm : m < (S.take k).length) (hm' : m < S.length) (x : ↥X) : AlgebraicGeometry.RestrictedCenterHasPointOver (S.take k) J ⟨m, hm⟩ x ↔ AlgebraicGeometry.RestrictedCenterHasPointOver S J ⟨m, hm'⟩ x

The restricted centres of the truncation S.take k are those of S at the same index (through the transports of stage, centre, strict transform and stage map of Hironaka.Scheme.BlowUpSequence.Truncate).

theorem Hironaka.Resolution.restrictedCenterHasPointOver_take {X : AlgebraicGeometry.Scheme} (S : X.BlowUpSequence) (J : X.IdealSheafData) (k : ℕ) (i : Fin (S.take k).length) (x : ↥X) : AlgebraicGeometry.RestrictedCenterHasPointOver (S.take k) J i x ↔ AlgebraicGeometry.RestrictedCenterHasPointOver S J ⟨↑i, ⋯⟩ x

restrictedCenterHasPointOver_take_mk in the Fin form.

Transport along an étale pair

theorem Hironaka.Resolution.restrictedCenterHasPointOver_iff_of_etale_pair {k : Type u} [Field k] [CharZero k] (F : (T : AlgebraicGeometry.Triple k) → T.X.left.BlowUpSequence) (TA : AlgebraicGeometry.Triple k) (hfun : ∀ (T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ TA.X.left) [AlgebraicGeometry.Smooth g], Function.Surjective ⇑g → T'.IsPullbackOf TA g → F T' = (F TA).pullback g) (hE : IsEmpty TA.E.ι) (j : ℕ) {W : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine W] (ψ ψ' : W ⟶ TA.X.left) [AlgebraicGeometry.Etale ψ] [AlgebraicGeometry.Etale ψ'] (hover : CategoryTheory.CategoryStruct.comp ψ (TA.X.left ↘ AlgebraicGeometry.Spec ↧k) = CategoryTheory.CategoryStruct.comp ψ' (TA.X.left ↘ AlgebraicGeometry.Spec ↧k)) (hI : TA.I.comap ψ = TA.I.comap ψ') (q : ↥W) (i : Fin ((F TA).take j).length) : AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (ψ q) ↔ AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (ψ' q)

Transport along an étale pair [Kol07, 4.2; 34.1]: for an assignment F of a blow-up sequence to every triple that is functorial under smooth surjections (hfun), a triple TA with empty boundary, and an étale pair ψ, ψ' : W ⟶ TA.X.left over k with the same inverse image of TA.I, the restricted centres of the truncation (F TA).take j have a point over ψ q if and only if they have one over ψ' q. The surjective completion T' of the pair carries the pullback data along both completed maps g, g', so (F TA).pullback g = F T' = (F TA).pullback g'; truncation commutes with pullback, and the predicate transports along the flat stage maps of a pullback, read at a point y of T' over ψ q and over ψ' q.

The smooth locus

theorem Hironaka.Resolution.not_restrictedCenterHasPointOver_of_mem_smoothLocus {k : Type u} [Field k] [CharZero k] (TA : AlgebraicGeometry.Triple k) {X : AlgebraicGeometry.Scheme} [X.Over (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.LocallyOfFiniteType (X ↘ AlgebraicGeometry.Spec ↧k)] (emb : X ⟶ TA.X.left) [AlgebraicGeometry.IsClosedImmersion emb] [AlgebraicGeometry.Scheme.Hom.IsOver emb (AlgebraicGeometry.Spec ↧k)] [AlgebraicGeometry.IsIntegral X] (hE : IsEmpty TA.E.ι) (hI : AlgebraicGeometry.Scheme.Hom.ker emb = TA.I) (F : (T : AlgebraicGeometry.Triple k) → T.X.left.BlowUpSequence) (hfun : ∀ (T' : AlgebraicGeometry.Triple k) (g : T'.X.left ⟶ TA.X.left) [AlgebraicGeometry.Smooth g], Function.Surjective ⇑g → T'.IsPullbackOf TA g → F T' = (F TA).pullback g) (j : ℕ) (ha : ∀ (i : Fin ((F TA).take j).length), ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb (genericPoint ↥X))) {x : ↥X} (hx : x ∈ AlgebraicGeometry.Scheme.Hom.smoothLocus (X ↘ AlgebraicGeometry.Spec ↧k)) (i : Fin ((F TA).take j).length) : ¬AlgebraicGeometry.RestrictedCenterHasPointOver ((F TA).take j) TA.I i (emb x)

No restricted centre over a smooth point [Kol07, Theorem 27, proof; 4.2]: for an integral scheme X embedded in the ambient of the triple TA (empty boundary, ideal the ideal of X), an assignment F of blow-up sequences to triples that is functorial under smooth surjections (hfun), and a truncation index j such that no restricted centre Z_i ∩ X̄_i of (F TA).take j has a point over the generic point of X (ha), no restricted centre has a point over any point of the smooth locus of X.