Documentation

Hironaka.Scheme.BlowUp.ExceptionalSetSmooth

The exceptional set of a blow-up with smooth centre of positive relative dimension #

For a sequence of nontrivial blow-ups the exceptional set is the total exceptional divisor [Kol07, Definition 25]; for a single blow-up π : B_Z X → X along a smooth centre Z of codimension at least two this is Ex(π) = |F|. The inclusion Ex(π) ⊆ |F| is Hironaka.Scheme.BlowUp.ExceptionalSet. The reverse inclusion is proved here from one fact about the exceptional divisor: F → Z is smooth of relative dimension r − 1 ≥ 1. The argument: if π were a local isomorphism at x' ∈ F, with π|_{U'} an open immersion on an open U' ∋ x', then F ∩ U' → Z would be an open immersion (the base change of π|_{U'} along Z → X), hence smooth of relative dimension 0; but it is also the restriction of F → Z to the open F ∩ U' ∋ x' of F, hence smooth of relative dimension r − 1; and a morphism with nonempty source has only one relative dimension (SmoothOfRelativeDimension.eq_of_nonempty: on an affine piece the Kähler differentials are free of rank the relative dimension, Mathlib's IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential, and a free module over a nontrivial ring has one rank). So r − 1 = 0, against r ≥ 2. The usual phrasing of the obstruction is through the fibre dimension r − 1 ≥ 1 of F → Z; relative dimension is the form Mathlib carries.

Main declarations #

source
theorem AlgebraicGeometry.exists_mem_basicOpen_of_span_eq_top {X : Scheme} {V : X.Opens} (s : Set ↑(X.presheaf.obj (Opposite.op V))) (hs : Ideal.span s = ⊤) {x : ↥X} (hx : x ∈ V) :
∃ t ∈ s, x ∈ X.basicOpen t

On an open V covered by the basic opens of a set s of sections spanning the unit ideal, every point lies in some D(t), t ∈ s (Mathlib's iSup_basicOpen_of_span_eq_top).

source
theorem AlgebraicGeometry.nontrivial_localizationAway_of_mem_basicOpen {X : Scheme} {V : X.Opens} (t : ↑(X.presheaf.obj (Opposite.op V))) {x : ↥X} (hx : x ∈ X.basicOpen t) :
Nontrivial (Localization.Away t)

A section that is a unit at a point is not nilpotent, so its localization is a nontrivial ring.

source
theorem AlgebraicGeometry.SmoothOfRelativeDimension.eq_of_nonempty {X Y : Scheme} (f : X ⟶ Y) [Nonempty ↥X] {n m : ℕ} [hn : SmoothOfRelativeDimension n f] [hm : SmoothOfRelativeDimension m f] :
n = m

A morphism with nonempty source has one relative dimension. If f is smooth of relative dimensions n and m, pick a point; the definition gives an affine pair on which Γ(Y, U) → Γ(X, V) is standard smooth of relative dimension n, Mathlib's HasRingHomProperty.appLE gives the relative dimension m locally on V, so on a basic open D(t) ∋ x both hold for Γ(Y, U) → Γ(X, V)_t; the Kähler differentials of that nontrivial algebra are free of rank n and of rank m (IsStandardSmoothOfRelativeDimension.rank_kaehlerDifferential).

source
theorem AlgebraicGeometry.Scheme.IdealSheafData.isOpenImmersion_subschemeMap_of_comap {X Y : Scheme} (f : Y ⟶ X) [IsOpenImmersion f] (I : X.IdealSheafData) (J : Y.IdealSheafData) (hJ : J = I.comap f) (H : I ≤ J.map f) :
IsOpenImmersion (J.subschemeMap I f H)

The map of closed subschemes V(J) → V(I) induced by an open immersion f : Y ⟶ X with J = I.comap f is an open immersion: it is the base change of f along V(I) → X (Mathlib's isPullback_of_isClosedImmersion).

source
theorem AlgebraicGeometry.Scheme.Opens.exists_ι_eq_of_mem {Z : Scheme} {U : Z.Opens} {u : ↥Z} (hu : u ∈ U) :
∃ (y : ↥↑U), U.ι y = u

A point of an open U is the image of a point of the open subscheme U.

source
theorem AlgebraicGeometry.support_comap_subset_exceptionalSet {B X : Scheme} (π : B ⟶ X) (Z : X.IdealSheafData) {m : ℕ} (hm : 1 ≤ m) [SmoothOfRelativeDimension m ((Z.comap π).subschemeMap Z π ⋯)] :
↑(Z.comap π).support ⊆ Scheme.Hom.exceptionalSet π

Every point of the exceptional divisor is exceptional when the divisor is smooth of positive relative dimension over the centre [Kol07, Definition 25]: if the induced map V(Z·𝒪_B) → V(Z) of a morphism π : B ⟶ X is smooth of relative dimension m ≥ 1, then every point of V(Z·𝒪_B) lies in the exceptional set of π. A local isomorphism at such a point would make the restriction of V(Z·𝒪_B) → V(Z) to an open neighbourhood an open immersion, smooth of relative dimension 0 and m at once, on a nonempty scheme.