The exceptional set of a morphism

The exceptional set of a birational morphism g : X' → X is the set of points x' ∈ X' at which g is not a local isomorphism, denoted Ex(g) [Kol07, Definition 25]. Here "local isomorphism at x'" is read as: there is an open U' ∋ x' on which g restricts to an open immersion, IsOpenImmersion (U'.ι ≫ g). Mathlib's IsLocalIso g is the global property (every point has such a neighbourhood), so Ex(g) = ∅ ↔ IsLocalIso g (exceptionalSet_eq_empty_iff).

For a blow-up π : B_Z X ⟶ X the exceptional set is contained in the exceptional divisor F = π⁻¹(Z) ([TSPA, Tag 02OS]; the easy half of Kollár's remark that Ex(Π) = Ex_tot(Π) for a sequence of nontrivial blow-ups [Kol07, Definition 25]): off Z the blow-up map is an isomorphism, so a point of B over X ∖ Z lies in the open π⁻¹(X ∖ Z), on which π is the isomorphism π ∣_ (X ∖ Z) followed by the open immersion of X ∖ Z, hence an open immersion. This is exceptionalSet_subset_support_comap, stated for any morphism that is an isomorphism over the complement of the centre; Hironaka.Scheme.BlowUp.ExceptionalSetSupport applies it to the monoidal transformation of the vocabulary. The reverse inclusion for a blow-up along a smooth centre of codimension at least two (the other half of Kollár's remark) is proved in Hironaka.Scheme.BlowUp.ExceptionalSetSmooth and ExceptionalSetSmoothCodim.

The definition is placed in Mathlib's namespace AlgebraicGeometry.Scheme.Hom so that it reads g.exceptionalSet; nothing here assumes g birational, the source's standing hypothesis, which is not needed for the definition or for these lemmas.

def AlgebraicGeometry.Scheme.Hom.exceptionalSet {X Y : Scheme} (f : X ⟶ Y) : Set ↥X

The exceptional set of f [Kol07, Definition 25]: the set of points at which f is not a local isomorphism — points with no open neighbourhood U such that U.ι ≫ f is an open immersion.

Equations

• AlgebraicGeometry.Scheme.Hom.exceptionalSet f = {x : ↥X | ¬∃ (U : X.Opens), x ∈ U ∧ AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)}

theorem AlgebraicGeometry.Scheme.Hom.mem_exceptionalSet_iff {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} : x ∈ exceptionalSet f ↔ ¬∃ (U : X.Opens), x ∈ U ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)

Membership in the exceptional set, by definition.

theorem AlgebraicGeometry.Scheme.Hom.notMem_exceptionalSet_iff {X Y : Scheme} (f : X ⟶ Y) {x : ↥X} : x ∉ exceptionalSet f ↔ ∃ (U : X.Opens), x ∈ U ∧ IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)

A point is not exceptional iff f is an open immersion on some open neighbourhood of it.

theorem AlgebraicGeometry.Scheme.Hom.exceptionalSet_eq_empty_iff {X Y : Scheme} (f : X ⟶ Y) : exceptionalSet f = ∅ ↔ IsLocalIso f

The comparison with Mathlib's global notion: f is a local isomorphism (IsLocalIso f, source-locally an open immersion) iff its exceptional set is empty.

theorem AlgebraicGeometry.Scheme.Hom.exceptionalSet_eq_empty {X Y : Scheme} (f : X ⟶ Y) [IsLocalIso f] : exceptionalSet f = ∅

A local isomorphism has empty exceptional set.

theorem AlgebraicGeometry.Scheme.Hom.notMem_exceptionalSet_of_isIso_restrict {X Y : Scheme} (f : X ⟶ Y) {V : Y.Opens} [CategoryTheory.IsIso (f ∣_ V)] {x : ↥X} (hx : f x ∈ V) : x ∉ exceptionalSet f

A point over an open V of the target on which f restricts to an isomorphism is not exceptional: on f⁻¹(V) the morphism is f ∣_ V followed by the open immersion V.ι.

theorem AlgebraicGeometry.Scheme.Hom.exceptionalSet_subset_compl_preimage {X Y : Scheme} (f : X ⟶ Y) {V : Y.Opens} [CategoryTheory.IsIso (f ∣_ V)] : exceptionalSet f ⊆ (↑((TopologicalSpace.Opens.map f.base).obj V))ᶜ

If f is an isomorphism over an open V, its exceptional set lies over the complement.

theorem AlgebraicGeometry.Scheme.Hom.exceptionalSet_subset_support_comap {X B : Scheme} (π : B ⟶ X) (I : X.IdealSheafData) [CategoryTheory.IsIso (π ∣_ I.support.compl)] : exceptionalSet π ⊆ ↑(I.comap π).support

The exceptional set lies in the exceptional divisor |F| = |π⁻¹(Z)|, the support of the inverse image ideal sheaf I·𝒪_B, for any morphism π : B ⟶ X that is an isomorphism over the complement of the centre Z = V(I) ([TSPA, Tag 02OS]; the easy half of Ex(Π) = Ex_tot(Π) in [Kol07, Definition 25]).