LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)

How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

Positive conormal degree for a fibre divisor on a normal surface

Statement

Assume AC and DC. Let $A$ be a normal Noetherian local domain of dimension two and $f : X \to Spec A$ a normal integral modification. For any nonempty effective Cartier divisor $Z$ supported in the special fibre, some integral component $C$ of $Z$ satisfies $\deg_{C} (O_{X} (- Z) ∣_{C}) > 0$ . In particular its conormal bundle is not trivial.

Facts & Assumptions

Given: A normal Noetherian local domain $A$ of dimension two, a normal integral modification $f ⁣ : X \to Spec A$ , and a nonempty effective Cartier divisor $Z$ supported in the special fibre.

[F1]

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 $F$ all of whose members are nonempty, there exists a function $g$ with domain $F$ satisfying $g (S) \in S$ for all $S \in F$ . (The Axiom of Choice)

[F2]

def-dependent-choice. Let $X$ be a set and let $R \subseteq X \times X$ be a binary relation on $X$ . Call $R$ entire on $X$ when $for every x \in X there is y \in X with x R y .$ The Axiom of Dependent Choice, written $D C$ , is the following statement. (The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

[F3]

def-normal-surface-modification-and-normalized-point-blowup. Normal schemes. A locally Noetherian scheme is normal if every local ring $O_{X, x}$ is an integrally closed domain (def-normal-noetherian-ring). This is a local condition on the local rings and is checked on an affine open cover; it does not require the global section ring to be a domain. The empty scheme is normal vacuously. (Normal scheme modifications and normalized point blowups)

[F4]

lem-local-normal-surface-modification-dimension-and-projective-cohomology. Assume AC and DC. Let $(A, m)$ be a normal Noetherian local domain of dimension two and $f : X \to Spec A$ an integral modification. Then $X$ has dimension two, all closed points have local dimension two, $f$ is an isomorphism off the closed point, $f_{*} O_{X} = O_{Spec A}$ , and its special fibre has dimension at most one. (Dimension and cohomology of local normal surface modifications)

[F5]

lem-normal-domain-implies-s-two. Assume the Axiom of Choice (The Axiom of Choice). Every commutative Noetherian integrally closed domain satisfies $(S_{2})$ . (normal domain implies s two)

[F6]

cor-regular-quotient-cohen-macaulay-equivalence. Assume the Axiom of Choice (The Axiom of Choice). Under the hypotheses of lem-regular-quotient-preserves-depth-dimension-gap, $M$ is Cohen--Macaulay if and only if $M / x M$ is Cohen--Macaulay. (Cohen--Macaulayness and a regular parameter quotient)

[F7]

cor-cohen-macaulay-modules-have-no-embedded-associated-primes. Under the hypotheses of lem-associated-primes-of-cohen-macaulay-module-have-full-dimension, every associated prime of $M$ is minimal in ${Supp}_{R} (M)$ . Thus $M$ has no embedded associated primes. (Cohen--Macaulay modules have no embedded associated primes)

[F8]

thm-one-dimensional-regular-local-rings-are-dvrs. Assume the Axiom of Choice (The Axiom of Choice). A nonzero Noetherian local ring of dimension one is regular if and only if it is a discrete valuation ring. Fields are excluded from the term DVR. (one dimensional regular local rings are dvrs)

[F9]

lem-normal-domain-implies-r-one. Every commutative Noetherian integrally closed domain satisfies $(R_{1})$ . (normal domain implies r one)

[F10]

lem-nonzero-section-vanishing-at-a-point-has-positive-degree. Assume the Axiom of Choice. Let $k$ be a field, let $C$ be an integral proper $k$ -scheme of dimension one and let $L$ be an invertible $O_{C}$ -module with a nonzero global section $s \in Γ (C, L)$ . If $s$ vanishes at some closed point of $C$ , then $\deg_{C} (L) > 0$ for the degree of def-degree-invertible-sheaf-proper-dimension-one. (A nonzero section vanishing at a point forces positive degree)

[F11]

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 $O_{C}$ -modules $L$ and $M$ (def-invertible-sheaf): 1. (Degree is additive on invertible sheaves over a proper curve)

Proof

1.1F3F4given

Write the one-dimensional fibre components as $C_{j}$ and choose closed points $x_{j}$ on $C_{j}$ lying on no other component; these exist because each is a proper finite-type curve over the residue field of $A$ .

2.1F3F8F9step 1.1

Choose $g_{j} \in m_{X, x_{j}}$ with nonzero image in $O_{C_{j}, x_{j}}$ ; in the common function field write $g_{j} = a_{j} / b_{j}$ with $a_{j}, b_{j} \in A$ and put $u = \prod_{j} a_{j}$ . Each $a_{j}$ lies in the maximal ideal, since otherwise $g_{j} b_{j} = a_{j}$ would make $g_{j}$ a unit; hence $u$ has positive orders $e_{j}$ at the generic discrete valuation rings of the fibre curves and factors as $u = g_{j} h_{j}$ near $x_{j}$ .

3.1F8step 2.1

Write $d_{j} = v_{C_{j}} (Z)$ , choose $i$ maximizing $d_{i} / e_{i}$ , and rescale $u \mapsto u^{d_{i}}$ , $Z \mapsto e_{i} Z$ ; then $v_{C_{j}} (u) \geq v_{C_{j}} (Z)$ for every $j$ with equality at $i$ .

4.1F5F6F7step 3.1

Normal surface local rings are Cohen--Macaulay, and their effective Cartier quotients are Cohen--Macaulay because a nonzerodivisor extends to a parameter tuple by the support-dimension argument; such quotients therefore have no embedded associated points. The section $u$ vanishes at the generic point of every component of $Z$ , hence at every associated point, so $u$ is zero in $O_{Z}$ and belongs to the Cartier ideal $I = O_{X} (- Z)$ ; its restriction to $C_{i}$ is nonzero at the generic point by equality of orders at $i$ .

5.1F6F7step 4.1

Near $x_{i}$ only the component $C_{i}$ occurs in $Z$ , and the factor $g_{i}$ (raised to the rescaling power) is nonzero at the unique associated generic point of $O_{Z}$ there, so it is a nonzerodivisor on $O_{Z}$ ; if $I = (t)$ , then $g_{i} h_{i} \in (t)$ implies $h_{i} \in (t)$ , whence the section coefficient $u / t = g_{i} (h_{i} / t)$ vanishes at $x_{i}$ .

6.1F1F2F10F11step 5.1∎

The proper integral-curve section criterion applied to the nonzero section $u / t$ of $I ∣_{C_{i}}$ vanishing at the closed point $x_{i}$ gives positive degree for the rescaled conormal bundle, and additivity of degree under tensor powers divides out the positive rescaling factor, giving $\deg_{C_{i}} (O_{X} (- Z) ∣_{C_{i}}) > 0$ ; the Axiom of Choice and the Axiom of Dependent Choice are inherited from the cited suppliers.

Remarks

This is the normal-surface version of the regular-surface conormal computation; the Cohen-Macaulay quotient property replaces the use of regularity of the ambient ring.
The rescaling step is what allows the section to vanish at all components while staying nonzero on the chosen one.

Depends on

Used by

H1 of a normal surface modification injects off its special fibre Lemma

Dependency tree · two levels

66 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

The Stacks Project, Resolution of Surfaces, Lemmas 54.7.3–8 (complete proofs read; normal-surface arguments reconstructed) (standard reference, not scraped)