ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passaudited 2026-09-30

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 conic map from O(2)

Example

Let $k$ be a field and let $P_{k}^{1}$ have homogeneous coordinates $x_{0}, x_{1}$ , with twisting sheaf $O (2) = O (1)^{\otimes 2}$ (Relative very ampleness in the finite projective-space convention). Then:

the three global sections $x_{0}^{2}, x_{0} x_{1}, x_{1}^{2}$ generate $O (2)$ (Global generation by the evaluation map) and define a closed immersion $ν_{2} : P_{k}^{1} ⟶ P_{k}^{2}, [x_{0} : x_{1}] ⟼ [x_{0}^{2} : x_{0} x_{1} : x_{1}^{2}],$ the degree-two Veronese, with $ν_{2}^{*} O (1) ≅ O (2)$ (Veronese embedding pulls O(1) back to O(d));
the image of $ν_{2}$ is the plane conic $V_{+} (Z_{0} Z_{2} - Z_{1}^{2}) \subseteq P_{k}^{2},$ where $Z_{0}, Z_{1}, Z_{2}$ are the target coordinates; on the chart $Z_{0} \neq 0$ the map is $[1 : x_{1} / x_{0}] \mapsto [1 : x_{1} / x_{0} : (x_{1} / x_{0})^{2}]$ , so $ν_{2}$ identifies $P_{k}^{1}$ with that conic;
since $ν_{2}$ is a closed immersion, the scheme-theoretic image of $ν_{2}$ is exactly the conic $V_{+} (Z_{0} Z_{2} - Z_{1}^{2})$ .

The computation is valid over an arbitrary field, with no restriction on the characteristic: the conic equation $Z_{0} Z_{2} - Z_{1}^{2}$ and the kernel computations below are polynomial identities with integer coefficients.

Facts & Assumptions

Given: A field $k$ , the projective line $P_{k}^{1}$ with coordinates $x_{0}, x_{1}$ and twisting sheaf $O (2)$ , the projective plane $P_{k}^{2}$ with coordinates $Z_{0}, Z_{1}, Z_{2}$ and twisting sheaf $O (1)$ , and the Axiom of Choice as inherited from the projective-space and sheaf constructions.

[A1]

The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)

[F1]

(Veronese in degrees $n = 1$ , $d = 2$ .) The monomial sections $s_{(2, 0)} = x_{0}^{2}$ , $s_{(1, 1)} = x_{0} x_{1}$ , $s_{(0, 2)} = x_{1}^{2}$ generate $O (2)$ , and the associated morphism $ν_{2} : P_{k}^{1} \to P_{k}^{2}$ is a closed immersion with $ν_{2}^{*} O (1) ≅ O (2)$ carrying the target coordinate $y_{m}$ to $s_{m}$ ; here $N = (\binom{1 + 2}{2}) - 1 = 2$ . (Veronese embedding pulls O(1) back to O(d))

[F2]

For a morphism $φ$ attached to generating sections $t_{m}$ of an invertible sheaf: $φ^{- 1} (D_{+} (y_{m})) = X_{t_{m}}$ and, on the chart where $t_{m_{0}}$ is a trivialising section, the chart coordinates satisfy $(y_{m} / y_{m_{0}}) \circ φ = t_{m} / t_{m_{0}}$ . In particular, if $φ^{*} y_{m} = t_{m}$ for all $m$ then the ratios of the sections are the ratios of their pullbacks. (Generating line-bundle sections define a morphism to projective space, Veronese embedding pulls O(1) back to O(d))

[F3]

On the standard chart $U_{i} = D_{+} (x_{i})$ of $P_{k}^{1}$ the sheaf $O (1)$ has frame $x_{i}$ , so $O (2)$ has frame $x_{i}^{2}$ , the section $x_{i}$ is a unit on $U_{i}$ , and $X_{x_{i}} = U_{i}$ ; the charts $U_{0}, U_{1}$ are $Spec k [x_{1}^{(0)}]$ and $Spec k [x_{0}^{(1)}]$ with $x_{1}^{(0)} = x_{1} / x_{0}$ and $x_{0}^{(1)} = x_{0} / x_{1}$ on the overlap. The standard charts of $P_{k}^{2}$ are the three affine planes $Spec k [Z_{1} / Z_{0}, Z_{2} / Z_{0}]$ , $Spec k [Z_{0} / Z_{1}, Z_{2} / Z_{1}]$ , $Spec k [Z_{0} / Z_{2}, Z_{1} / Z_{2}]$ . (Relative projective space from standard charts, Relative very ampleness in the finite projective-space convention)

[F4]

For a commutative ring $A$ , an integer $n \geq 0$ , $B = A [x_{0}, \dots, x_{n}]$ and a homogeneous ideal $I \subseteq B$ , the closed subscheme $V_{+} (I) ↪ P_{A}^{n}$ has $V_{+} (I) \cap D_{+} (x_{i}) = Spec (B_{(x_{i})} / I_{(x_{i})})$ ; every closed subscheme of $P_{A}^{n}$ is recovered from its chart ideals, and $V_{+} (I) = V_{+} (J)$ as closed subschemes exactly when $I$ and $J$ have the same saturation. (Closed subschemes of projective space and saturated ideals)

[F5]

Kernel computations over a field $k$ : the $k$ -algebra homomorphism $k [u, v] \to k [t]$ with $u \mapsto t$ , $v \mapsto t^{2}$ has kernel $(v - u^{2})$ , because $k [u, v] / (v - u^{2}) ≅ k [u]$ via elimination of $v$ and $k [u] \to k [t]$ , $u \mapsto t$ , is injective; the homomorphism $k [u, v] \to k [t, t^{- 1}]$ with $u \mapsto t^{- 1}$ , $v \mapsto t$ has kernel $(u v - 1)$ by the same elimination, using $k [u, v] / (u v - 1) ≅ k [u, u^{- 1}]$ ; and the homomorphism $k [a, b] \to k [t^{- 1}]$ with $a \mapsto t^{- 2}$ , $b \mapsto t^{- 1}$ has kernel $(a - b^{2})$ . [algebra]

[F6]

A morphism of affine schemes whose associated ring map is surjective with kernel $K$ has image the closed subscheme $Spec (k [u, v] / K)$ , and a closed immersion is in particular injective, so its image is the closed subscheme it defines. (Closed subschemes of projective space and saturated ideals, Immersion of schemes)

Verification

technique · direct: invoke the Veronese theorem in degree two on the projective line, read the chart formulas for the ratios of the monomial sections, compute the chart rings of the conic $Z_0Z_2-Z_1^2$, and compare them with the chartwise images of the morphism

1.1F1F3

The monomials and the morphism. Put $M = {(2, 0), (1, 1), (0, 2)}$ , so $∣ M ∣ = 3 = (\binom{1 + 2}{2})$ and $N = 2$ , and set $s_{m} = x^{m}$ . By [F1] the sections $s_{(2, 0)} = x_{0}^{2}$ , $s_{(1, 1)} = x_{0} x_{1}$ , $s_{(0, 2)} = x_{1}^{2}$ generate the invertible sheaf $O (2)$ , and $ν_{2} : P_{k}^{1} \to P_{k}^{2}$ is a closed immersion with $ν_{2}^{*} O (1) ≅ O (2)$ , carrying the target coordinate $y_{m}$ to $s_{m}$ ; write $Z_{0} = y_{(2, 0)}$ , $Z_{1} = y_{(1, 1)}$ , $Z_{2} = y_{(0, 2)}$ .

1.2F1F2F3algebra

The chart formulas for $ν_{2}$ . On $U_{0} = D_{+} (x_{0})$ the section $s_{(2, 0)} = x_{0}^{2}$ is a frame of $O (2)$ by [F3], and by [F2] $ν_{2}^{- 1} (D_{+} (Z_{0})) = X_{s_{(2, 0)}} = U_{0}$ , with $(Z_{1} / Z_{0}) \circ ν_{2} = s_{(1, 1)} / s_{(2, 0)} = x_{1} / x_{0}$ and $(Z_{2} / Z_{0}) \circ ν_{2} = s_{(0, 2)} / s_{(2, 0)} = (x_{1} / x_{0})^{2}$ on $U_{0}$ . Symmetrically on $U_{1} = D_{+} (x_{1})$ one has $ν_{2}^{- 1} (D_{+} (Z_{2})) = U_{1}$ , $(Z_{0} / Z_{2}) \circ ν_{2} = (x_{0} / x_{1})^{2}$ and $(Z_{1} / Z_{2}) \circ ν_{2} = x_{0} / x_{1}$ , while on the overlap $U_{0} \cap U_{1} = X_{s_{(1, 1)}}$ one has $(Z_{0} / Z_{1}) \circ ν_{2} = x_{0} / x_{1}$ and $(Z_{2} / Z_{1}) \circ ν_{2} = x_{1} / x_{0}$ . In particular, on the chart $Z_{0} \neq 0$ the morphism sends a point with coordinate $u = x_{1} / x_{0}$ to $[1 : u : u^{2}]$ , which is the displayed formula $[x_{0} : x_{1}] \mapsto [x_{0}^{2} : x_{0} x_{1} : x_{1}^{2}]$ .

1.3F4algebra

The conic and its chart rings. Let $F = Z_{0} Z_{2} - Z_{1}^{2} \in k [Z_{0}, Z_{1}, Z_{2}]$ , homogeneous of degree $2$ . By [F4] the closed subscheme $V_{+} (F) \subseteq P_{k}^{2}$ has chart ideals generated by the dehomogenisations: $(F)_{(Z_{0})} = (Z_{2} / Z_{0} - (Z_{1} / Z_{0})^{2})$ , $(F)_{(Z_{1})} = ((Z_{0} / Z_{1}) (Z_{2} / Z_{1}) - 1)$ and $(F)_{(Z_{2})} = (Z_{0} / Z_{2} - (Z_{1} / Z_{2})^{2})$ , so its chart rings are $k [u, v] / (v - u^{2})$ with $u = Z_{1} / Z_{0}$ , $v = Z_{2} / Z_{0}$ ; $k [u, v] / (u v - 1)$ with $u = Z_{0} / Z_{1}$ , $v = Z_{2} / Z_{1}$ ; and $k [a, b] / (a - b^{2})$ with $a = Z_{0} / Z_{2}$ , $b = Z_{1} / Z_{2}$ .

2.1F5F6step 1.2step 1.3algebra

The image on each target chart. On $D_{+} (Z_{0})$ the morphism $ν_{2}$ restricts on $U_{0}$ to the morphism corresponding to the $k$ -algebra map $k [u, v] \to k [t]$ , $u \mapsto x_{1} / x_{0} = t$ , $v \mapsto t^{2}$ by step 1.2, whose kernel is $(v - u^{2})$ by [F5]; hence the image of $U_{0}$ is the closed subscheme cut out by $v - u^{2}$ , which is exactly $V_{+} (F) \cap D_{+} (Z_{0})$ by step 1.3, and $U_{0} \to V_{+} (F) \cap D_{+} (Z_{0})$ is an isomorphism. On $D_{+} (Z_{1})$ the restriction corresponds on $U_{0} \cap U_{1}$ to $k [u, v] \to k [t, t^{- 1}]$ , $u \mapsto t^{- 1}$ , $v \mapsto t$ , with kernel $(u v - 1)$ ; on $D_{+} (Z_{2})$ the restriction corresponds on $U_{1}$ to $k [a, b] \to k [t^{- 1}]$ , $a \mapsto t^{- 2}$ , $b \mapsto t^{- 1}$ , with kernel $(a - b^{2})$ . In each case the image chart is the corresponding chart of $V_{+} (F)$ from step 1.3 and the restriction is an isomorphism onto it.

3.1F1F4step 1.3step 2.1

The image is the conic. The morphism $ν_{2}$ is a closed immersion by [F1], so its image is a closed subscheme $Z \subseteq P_{k}^{2}$ ; by [F4] such a closed subscheme is recovered from its chart ideals. Step 2.1 computes the chart of $Z$ over each of $D_{+} (Z_{0})$ , $D_{+} (Z_{1})$ , $D_{+} (Z_{2})$ to be the corresponding chart of $V_{+} (F)$ computed in step 1.3, so $Z = V_{+} (Z_{0} Z_{2} - Z_{1}^{2})$ : the image of the Veronese $ν_{2}$ is exactly the conic $Z_{0} Z_{2} = Z_{1}^{2}$ , and $ν_{2}$ identifies $P_{k}^{1}$ with it.

4.1

Conclusion. Steps 1.1 and 1.2 show that the global sections $x_{0}^{2}, x_{0} x_{1}, x_{1}^{2}$ generate $O (2)$ and define the degree-two Veronese closed immersion $[x_{0} : x_{1}] \mapsto [x_{0}^{2} : x_{0} x_{1} : x_{1}^{2}]$ with $ν_{2}^{*} O (1) ≅ O (2)$ , and steps 1.3 to 3.1 identify its image, hence its scheme-theoretic image, with the conic $Z_{0} Z_{2} - Z_{1}^{2} = 0$ . No division by $2$ or by any other nonzero scalar occurs: the quadratic equation is integral and the kernels $(v - u^{2})$ , $(u v - 1)$ , $(a - b^{2})$ of [F5] are computed by elimination of a variable in every characteristic, so the verification is uniform, including characteristic two. The Axiom of Choice [A1] is inherited from the Veronese and projective-space suppliers; the only objects chosen are the three monomials and the three target charts, so no choice is made here. [A1, F1, F5, step 1.2, step 3.1, cases: characteristic two and general characteristic] \qed

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

32 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, Constructions of Schemes, Sections 27.8-27.21 (standard reference, not scraped)
Ravi Vakil, The Rising Sea, 29 August 2022, Sections 4.5, 7.4, 9.3, 10.6, 17.4, 17.6, 18.2 (standard reference, not scraped)
Gao-Zhang, Lectures on Algebraic Geometry, Chapter 5 (standard reference, not scraped)