ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck pass

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.

The intersection form of the blown-up projective plane

Example

Assume the Axiom of Choice, inherited through the Euler-characteristic and blowup suppliers (The Axiom of Choice). Let $k$ be a field, $X = P_{k}^{2}$ , let $p \in X (k)$ be a $k$ -rational point, let $π : X^{'} = {Bl}_{p} X \to X$ be the blowup (Blowup of a scheme along an ideal sheaf), let $E = π^{- 1} (p)$ be the exceptional curve (Exceptional subscheme of a blowup) and let $l : = π^{*} O_{X} (1)$ in $Pic (X^{'})$ (the pullback of the hyperplane class; it is also the strict transform of any line not passing through $p$ ). Then $l \cdot l = 1, l \cdot E = 0, E \cdot E = - 1,$ so the intersection form on the sublattice $Z l + Z E$ of $Pic (X^{'})$ has matrix $(\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array}) .$ Moreover the strict transform $m : = π^{*} O (1) - E$ of a line through $p$ (Strict transform of a closed subscheme) satisfies $m = l - E$ , $m \cdot E = 1$ and $m \cdot m = 0$ .

Facts & Assumptions

Given: a field $k$ , the plane $X = P_{k}^{2}$ , a $k$ -rational point $p \in X (k)$ , the blowup $π : X^{'} = {Bl}_{p} X \to X$ with exceptional curve $E = π^{- 1} (p)$ , the class $l = π^{*} O_{X} (1)$ , and the Axiom of Choice (The Axiom of Choice).

[F1]

The plane $X$ is an integral regular projective surface over $k$ ; the intersection product $C \cdot D$ of Cartier divisors is defined, symmetric and bilinear, and $O (d) \cdot O (e) = d e$ on $X$ , in particular $O (1) \cdot O (1) = 1$ (Intersection numbers of Cartier divisors on a smooth projective surface, The surface intersection product is symmetric and bilinear, The intersection pairing on the projective plane, Integral schemes).

[F2]

Blowup calculus at a $k$ -rational point: since $p$ is $k$ -rational its residue field is $κ (p) = k$ and $r = [κ (p) : k] = 1$ ; the blowup $X^{'}$ is an integral regular projective surface over $k$ , $E$ is an effective Cartier divisor with $E ≅ P_{k}^{1}$ and $O_{E} (E) ≅ O_{P_{k}^{1}} (- 1)$ ; for all Cartier divisors $D, D^{'}$ on $X$ one has $E \cdot π^{*} D = 0$ and $π^{*} D \cdot π^{*} D^{'} = D \cdot D^{'}$ ; and for a reduced effective Cartier divisor $C$ through $p$ with multiplicity $m \geq 1$ and strict transform $C^{'}$ one has $π^{*} C = C^{'} + m E$ , $C^{'} \cdot E = m$ and $C^{'} \cdot C^{'} = C \cdot C - m^{2}$ (The intersection matrix of a point blowup of a regular surface, $r = 1$ ; The normal bundle of the exceptional curve is O(-1), Pullback of a Cartier divisor).

[F3]

Pullback of divisor classes: for a Cartier divisor $D$ the total transform $π^{*} D$ is the pullback Cartier divisor with $O_{X^{'}} (π^{*} D) ≅ π^{*} O_{X} (D)$ (Total transform of a Cartier divisor, Pullback of a Cartier divisor computes the pullback of its line bundle); hence $l = [O_{X^{'}} (π^{*} L)]$ for any line $L$ on $X$ , and the total transform of a line $L$ not through $p$ is its strict transform because $π$ is an isomorphism away from $p$ . For a line $L$ through $p$ the multiplicity of a local equation at $p$ is $1$ , so $π^{*} L = m + E$ with $m$ the strict transform (Total transform equals strict transform plus multiplicity times the exceptional divisor, Effective cartier divisor).

[F4]

The Axiom of Choice enters through the blowup, Euler-characteristic and bilinearity suppliers of [F1]–[F3]; the point, the lines and the blowup are given data and no selection is made below.

Verification

Given: a field $k$ , the plane $X = P_{k}^{2}$ , a $k$ -rational point $p$ , the blowup $π : X^{'} = {Bl}_{p} X \to X$ , its exceptional curve $E$ , the class $l = π^{*} O_{X} (1)$ , and a line $L$ through $p$ .

1.1F2

The blowup data. Since $p$ is $k$ -rational, $r = 1$ ; the surface $X^{'}$ is integral regular projective and $E$ is an effective Cartier divisor isomorphic to $P_{k}^{1}$ with $O_{E} (E) ≅ O (- 1)$ , so the intersection product is defined on $X^{'}$ and $E^{2} = - r = - 1$ ; moreover $E \cdot π^{*} D = 0$ and $π^{*} D \cdot π^{*} D^{'} = D \cdot D^{'}$ for all Cartier divisors $D, D^{'}$ on $X$ .

1.2F1F2F3

$l \cdot l = 1$ . Choose a line $L^{'}$ on $X$ ; its class satisfies $[O_{X} (L^{'})] = [O_{X} (1)]$ , so $l \cdot l = π^{*} O_{X} (L^{'}) \cdot π^{*} O_{X} (L^{'}) = O_{X} (L^{'}) \cdot O_{X} (L^{'}) = 1$ by the pullback identity and the plane computation.

1.3F2F3

$l \cdot E = 0$ . With $D$ the Cartier divisor of any line on $X$ , so that $π^{*} D$ has class $l$ , the orthogonality clause gives $E \cdot π^{*} D = 0$ , that is, $l \cdot E = E \cdot l = 0$ by symmetry.

2.1F2step 1.1

$E \cdot E = - 1$ . This is the self-intersection formula of step 1.1 with $r = 1$ .

3.1F1step 1.2step 1.3step 2.1

The matrix. Steps 1.2, 1.3 and 2.1 give $l \cdot l = 1$ , $l \cdot E = 0 = E \cdot l$ and $E \cdot E = - 1$ ; if $a l + b E = 0$ in $Pic (X')$ , pairing with $l$ gives $a = 0$ and pairing with $E$ gives $- b = 0$ . Thus these classes freely generate the stated sublattice; by bilinearity its Gram matrix of the sublattice $Z l + Z E$ in the basis $(l, E)$ is $(\begin{array}{cc} 1 & 0 \\ 0 & - 1 \end{array})$ .

3.2F1F2F3step 1.2step 1.3step 2.1

The strict transform of a line through $p$ . Let $L$ be a line through $p$ with strict transform $m$ . The line is reduced and its multiplicity at $p$ is $1$ , so $π^{*} L = m + E$ and $m \cdot E = 1$ and $m \cdot m = L \cdot L - 1 = 0$ ; equivalently, taking classes and using $O_{X^{'}} (π^{*} L) ≅ π^{*} O_{X} (1)$ , the class of $m$ is $l - E$ , and bilinearity and steps 1.2–2.1 give $m \cdot E = l \cdot E - E \cdot E = 0 + 1 = 1$ and $m \cdot m = l \cdot l - 2 l \cdot E + E \cdot E = 1 - 0 - 1 = 0$ , in agreement.

4.1F4step 3.1step 3.2∎

Conclusion and choice accounting. Steps 1.2, 1.3 and 2.1 give the matrix of the intersection form on $Z l + Z E$ , and step 3.2 gives $m = l - E$ , $m \cdot E = 1$ , $m \cdot m = 0$ for the strict transform of a line through $p$ . The Axiom of Choice enters through the suppliers recorded in [F4]; the point, the lines and the blowup are given data and no selection is made in the computations.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

106 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

Ravi Vakil, The Rising Sea: Foundations of Algebraic Geometry, pre-publication version 2025-10-21 (standard reference, not scraped)
The Stacks Project, Varieties, Section 33.45 (Numerical intersections) (standard reference, not scraped)