ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedaudited 2026-09-27

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.

A tangent line and conic have one intersection point of local length two

Example

Assume the Axiom of Choice (The Axiom of Choice). Let $k$ be any field, let $F = x_{0} x_{2} - x_{1}^{2}$ (a conic) and $G = x_{2}$ (a line) in $k [x_{0}, x_{1}, x_{2}]$ , and let $X = Proj (k [x_{0}, x_{1}, x_{2}] / (F, G))$ . Then $X$ has exactly one point, $P = [1 : 0 : 0]$ . Writing $u = x_{1} / x_{0}$ and $v = x_{2} / x_{0}$ on the chart $x_{0} \neq 0$ , the chart ring is $k [u, v] / (v - u^{2}, v) ≅ k [u] / (u^{2})$ , the local algebra $O_{X, P}$ is this two-dimensional local $k$ -algebra, its length is $2$ , the residue field is $k$ with $[κ (P) : k] = 1$ , and ${len}_{k} (X) = 2 = \deg F \cdot \deg G$ .

Facts & Assumptions

Given: The Axiom of Choice, a field $k$ , the conic $F = x_{0} x_{2} - x_{1}^{2}$ of degree $2$ , the line $G = x_{2}$ of degree $1$ , the quotient $S = k [x_{0}, x_{1}, x_{2}] / (F, G)$ with its standard grading, and $X = Proj S$ with standard charts $D_{+} (x_{i}) = Spec (A_{i})$ (Projective scheme of a homogeneous quotient and its standard affine charts).

[L1]

Points of $X$ are the homogeneous primes $p \subseteq S$ with $S_{+} ⊈ p$ ; a chart $D_{+} (x_{i})$ is empty exactly when the localisation $S_{x_{i}}$ is the zero ring, and the point of the chart corresponding to $p \subseteq A_{i}$ is the point of $X$ it contracts from (Projective scheme of a homogeneous quotient and its standard affine charts, Prime and local-ring correspondence on standard projective charts).

[L2]

Assume AC. If $x \in D_{+} (x_{i})$ corresponds to the prime $p_{0} \subseteq A_{i}$ , then $O_{X, x} ≅ (A_{i})_{p_{0}}$ , the chart ring being the quotient $A_{i} ≅ k [y_{0}, y_{1}] / (f_{i}, g_{i})$ of the polynomial ring in the two chart coordinates by the dehomogenised equations (Two coprime projective plane forms meet in total length equal to their degree product, Prime and local-ring correspondence on standard projective charts).

[L3]

Assume AC. The total length of the zero-dimensional $X$ is ${len}_{k} (X) = \sum_{x \in X} ℓ_{O_{X, x}} (O_{X, x}) [κ (x) : k]$ , and for coprime plane forms of degrees $d, e$ it equals $d e$ (Total length of a zero-dimensional projective scheme, Algebraic Bezout formula as a sum of local scheme lengths).

[L4]

The length of a module is the number of factors in a composition series, whose factors are simple modules (Composition series and length of a module, Simple module: a nonzero module with no proper nonzero submodule).

Verification

technique · direct

1.1

In $S$ one has $x_{2} = 0$ and hence $x_{1}^{2} = x_{0} x_{2} = 0$ , so $x_{1}, x_{2}$ are nilpotent in $S$ and the localisations $S_{x_{1}}, S_{x_{2}}$ are the zero ring: the charts $D_{+} (x_{1})$ and $D_{+} (x_{2})$ are empty; moreover $S ≅ k [x_{0}, x_{1}] / (x_{1}^{2})$ by $x_{2} \mapsto 0$ , whose only homogeneous prime not containing $(x_{0}, x_{1})$ is $(x_{1})$ , so $X$ has exactly one point, namely the point $P = [1 : 0 : 0]$ cut out by $(x_{1}, x_{2})$ .

L1algebra

2.1

In the chart $D_{+} (x_{0})$ the dehomogenised equations are $v - u^{2}$ and $v$ with $u = x_{1} / x_{0}$ , $v = x_{2} / x_{0}$ , so $A_{0} ≅ k [u, v] / (v - u^{2}, v) ≅ k [u] / (u^{2})$ , and this is the chart through $P$ by step 1.1; this ring has the unique prime $(u)$ with $A_{0} / (u) ≅ k$ , so $O_{X, P} ≅ A_{0}$ and $κ (P) = k$ , that is $[κ (P) : k] = 1$ .

L2step 1.1

3.1

In $A_{0} = k [u] / (u^{2})$ the chain $0 ⊊ (u) ⊊ A_{0}$ is a composition series: $(u) = k \cdot u$ is a simple module (it is annihilated by $(u)$ , so it is the simple $A_{0}$ -module $k$ ) and $A_{0} / (u) ≅ k$ is simple, so by [L4] the length is $ℓ_{O_{X, P}} (O_{X, P}) = ℓ_{A_{0}} (A_{0}) = 2$ .

L4step 2.1algebra

4.1

Since $X$ has the single point $P$ with local length $2$ and residue degree $1$ , [L3] gives ${len}_{k} (X) = 2 \cdot 1 = 2$ , which agrees with the Bezout value $\deg F \cdot \deg G = 2 \cdot 1 = 2$ for the coprime forms $F, G$ .

L3step 1.1step 2.1step 3.1algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

55 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

A. Gathmann, Algebraic Geometry class notes (2002), Example 6.2.3, pp. 96-97 (standard reference, not scraped)