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.

First blowup of the node y^2=x^3+x^2 separates its branches

Example

Let $C = V (y^{2} - x^{3} - x^{2})$ over a field $k$ of characteristic not $2$ , with its node at the origin. In the chart $y = x s$ the total transform is $x^{2} (s^{2} - x - 1)$ , so the strict transform is $V (s^{2} - x - 1)$ , which meets $E$ at the two distinct points $s = + 1$ and $s = - 1$ ; the other chart contributes no additional points of $E$ . Hence the two branches of the node are separated by one point blowup, and the strict transform is regular and transverse to $E$ .

Facts & Assumptions

Given: A field $k$ of characteristic not $2$ , the nodal plane curve $C = V (y^{2} - x^{3} - x^{2}) \subseteq A_{k}^{2}$ with node at the origin, the blowup of the origin with exceptional curve $E$ , its two standard charts, and the strict transform $C^{'}$ .

[A1]

Choice. The Axiom of Choice is inherited from the blowup construction; the explicit chart computations below use no further choice. (The Axiom of Choice).

[F1]

Strict-transform equation by removing the maximal exceptional power: In the chart with coordinates $(x, s)$ where $y = x s$ , the total transform equation of a curve of multiplicity $m$ is $f (x, x s) = x^{m} g (x, s)$ with $g (0, s) = f_{m} (1, s)$ the leading form evaluated at $(1, s)$ , and the strict transform is defined by $g = 0$ ; symmetrically in the other chart.

[F2]

The blowup of the plane at the origin as an incidence scheme: For ${Bl}_{0} A_{k}^{2}$ the two standard charts are $Spec k [x, T]$ with $y = x T$ and $Spec k [y, U]$ with $x = y U$ , glued by inverting $T$ and $U$ with $T U = 1$ ; the exceptional divisor $E$ is $V (x)$ and $V (y)$ respectively and is $P_{k}^{1}$ .

[F3]

Strict transform of a closed subscheme: The strict transform is the scheme-theoretic closure of the inverse image of the complement of the center; in a chart where the ideal of $E$ is invertible it is cut by the saturation of the inverse-image ideal by that ideal.

[F4]

Strict transforms of plane curves record tangent directions: For a reduced plane curve $C = V (f)$ through the origin of multiplicity $m$ with leading form $f_{m}$ , the scheme $C^{'} \cap E$ is cut out on $E$ by the form $f_{m}$ : its closed points correspond to the irreducible factors of $f_{m}$ , a factor of multiplicity $s$ contributes with multiplicity $s$ , and the $0$ -cycle has total degree $m$ ; over a field over which $f_{m}$ splits these points are exactly the tangent directions of $C$ at the origin, and if $f_{m}$ is squarefree the strict transform meets $E$ transversally at each of them.

Verification

1.1A1F1F3given

In the first chart of [F2] write $s = T = y / x$ , so the chart ring is $k [x, s]$ with $y = x s$ and $E = V (x)$ , and let $f = y^{2} - x^{3} - x^{2}$ , a reduced equation of $C$ of multiplicity $m = 2$ at the origin with leading form $f_{2} = y^{2} - x^{2} = (y - x) (y + x)$ , which is squarefree because the characteristic is not $2$ ; substituting $y = x s$ gives $f (x, x s) = x^{2} s^{2} - x^{3} - x^{2} = x^{2} (s^{2} - x - 1)$ with $s^{2} - x - 1$ not divisible by $x$ , since its reduction modulo $x$ is $s^{2} - 1$ , so the strict transform is cut in this chart by $g = s^{2} - x - 1$ by [F1] and [F3].

2.1F3F4step 1.1

In this chart $C^{'} \cap E = V (x, s^{2} - x - 1) = V (x, s^{2} - 1)$ , the two distinct points $s = 1$ and $s = - 1$ ; at each of them the local ring of $C^{'}$ is $k [s]_{(s \mp 1)}$ with the equation of $E$ restricting to $s^{2} - 1 = (s - 1) (s + 1)$ , which has a simple zero at each point, so the contact order is one and $C^{'}$ meets $E$ transversally there; this agrees with [F4], since $f_{2} (1, s) = s^{2} - 1 = (s - 1) (s + 1)$ is squarefree with the two distinct roots $s = \pm 1$ , the two tangent directions of $C$ at the origin. The curve $C^{'} = V (s^{2} - x - 1)$ is regular, its gradient $(- 1, 2 s)$ being nowhere zero, so the strict transform is regular at both points.

3.1F1F2F3step 2.1

In the second chart of [F2] write $U = x / y$ , so the chart ring is $k [y, U]$ with $x = y U$ and $E = V (y)$ ; substituting gives $f = y^{2} - y^{3} U^{3} - y^{2} U^{2} = y^{2} (1 - U^{2} - y U^{3})$ , so the strict transform is cut in this chart by $1 - U^{2} - y U^{3}$ and meets $E$ where $y = 0$ and $1 - U^{2} = 0$ , namely at $U = 1$ and $U = - 1$ ; these are the same two points as $s = 1$ and $s = - 1$ , because $U = 1 / s$ on the overlap $T U = 1$ of [F2], and there is no further point of $E$ on $C^{'}$ in this chart, so the other chart contributes no additional points of $E$ .

4.1F4step 2.1step 3.1∎

Consequently $C^{'} \cap E$ consists exactly of the two distinct points over the node, one for each of the two factors $y - x$ and $y + x$ of the leading form, so the two branches of the node, whose tangent directions are those two factors, arrive at distinct points of $E$ and are separated by the one point blowup; the strict transform $C^{'}$ is regular and transverse to $E$ at both points, and in the first chart it is the smooth conic-like curve $V (s^{2} - x - 1)$ while in the second chart it is $V (1 - U^{2} - y U^{3})$ , the two descriptions agreeing on the overlap.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

30 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, Foundations of Algebraic Geometry, June 27, 2011 draft (author-hosted 'Early (out-of-date) version of The Rising Sea') (standard reference, not scraped)
Roman Bezrukavnikov et al., MIT 18.725 Algebraic Geometry (Fall 2015) consolidated lecture notes (standard reference, not scraped)
J. S. Milne, Algebraic Geometry v6.10 (standard reference, not scraped)