Negativity of contracted curves on regular surfaces

Given: A field $k$, an integral regular projective surface $X$ over $k$, an integral regular finite-type $k$-scheme $Y$ of pure dimension two, a proper birational morphism $f\text{\hspace{0.17em}⁣}:X\to Y$, and an integral curve $E\subseteq X$ with $f(E)$ a single closed point $y\in Y$.

cor-degree-additive-proper-curve. Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field and let $C$ be a proper $k$-scheme (def-proper-morphism) whose underlying topological space has dimension at most one (def-dimension-noetherian-topological-space). For all invertible ${\mathcal{O}}_C$-modules $\mathcal{L}$ and $\mathcal{M}$ (def-invertible-sheaf): 1. (Degree is additive on invertible sheaves over a proper curve)

def-axiom-of-choice. The Axiom of Choice (AC) is the following statement. > Every family of nonempty sets has a choice function > (def-choice-function). Written out: for every set $\mathcal{F}$ all of whose members are nonempty, there exists a function $g$ with domain $\mathcal{F}$ satisfying $g(S)\in S$ for all $S\in \mathcal{F}$. (The Axiom of Choice)

def-cartier-divisor. Let $X$ be a scheme and let $K_X$ be its sheaf of meromorphic functions, with the injective structure map ${\mathcal{O}}_X\to K_X$ (def-sheaf-total-quotient-rings, def-sheaf-on-topological-space). (Cartier divisor)

def-degree-invertible-sheaf-proper-dimension-one. Assume the Axiom of Choice, inherited from the Euler-characteristic supplier below (The Axiom of Choice). Let $k$ be a field (def-field) and let $C$ be a proper $k$-scheme (def-proper-morphism) whose underlying topological space is Noetherian of dimension at most one (def-dimension-noetherian-topological-space, def-locally-noetherian-and-noetherian-scheme). (Degree of an invertible sheaf on a proper one-dimensional scheme)

def-divisor-intersection-number-on-smooth-projective-surface. Assume the Axiom of Choice, inherited from the Euler-characteristic supplier below (The Axiom of Choice). Let $k$ be a field and let $X$ be an integral (Integral schemes), regular (embedding dimension and regular local ring), projective (Projective morphisms before Proj) $k$-scheme of pure dimension two (def-dimension-noetherian-topological-space). (Intersection numbers of Cartier divisors on a smooth projective surface)

def-embedding-dimension-and-regular-local-ring. For a nonzero commutative Noetherian local ring $(R,\mathfrak{m},k)$, define $\mathrm{edim}R={\dim }_k(\mathfrak{m}\mathrm{/}{\mathfrak{m}}^2)$. The ring is regular local when $\mathrm{edim}R=\dim R$. The cotangent space is intrinsic, and is finite-dimensional because $\mathfrak{m}$ is finitely generated. (embedding dimension and regular local ring)

def-integral-scheme. An integral scheme is a nonempty scheme that is reduced and whose underlying topological space is irreducible. Equivalently, it is nonempty and every nonempty affine open is the spectrum of a domain. The latter criterion is independent of the chosen affine open cover. (Integral schemes)

def-projective-morphism-pre-proj. For an arbitrary base scheme $S$, a morphism $f:X\to S$ is projective on this page if for some integer $n\ge 0$ it factors over $S$ as $X\stackrel{i}{\to }{\mathbb{P}}_S^n⟶S,$ where $i$ is a closed immersion and the second arrow is the projection. (def-projective-morphism-pre-proj)

lem-positive-conormal-degree-of-a-fibre-divisor. Assume the Axiom of Choice. Let $k$, $X$, $Y$, $f\text{\hspace{0.17em}⁣}:X\to Y$ and $y\in Y$ be as in lem-fibre-components-of-a-proper-birational-morphism-of-regular-surfaces, and let $Z\subseteq X$ be a nonzero effective Cartier divisor with $Z\subseteq f^{-1}(y)$ set-theoretically. (A divisor supported in a special fibre has positive conormal degree on some component)

thm-intersection-with-curve-as-degree-of-restriction. Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be a field, let $X$ be an integral regular projective surface over $k$ (Intersection numbers of Cartier divisors on a smooth projective surface) and let $C$ and $D$ be effective Cartier divisors on $X$ (def-effective-cartier-divisor, Cartier divisor) with associated line bundles ${\mathcal{O}}_X(C)$ and (Intersection with a curve is the degree of the restriction)

thm-nonaffine-regular-local-ring-is-ufd. Assume the Axiom of Choice. Every regular local ring is a unique factorization domain. In particular every smooth finite-type scheme over a field is locally factorial. (Regular local rings are unique factorization domains)