ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6.1-sol)audited 2026-10-02

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.

Adjunction on a smooth plane cubic: the canonical bundle is trivial

Example

Assume the Axiom of Choice; it supplies Dependent Choice through AC implies DC implies countable choice. Let $k$ be a field and let $C = V_{+} (F) \subseteq P_{k}^{2}$ be a smooth plane cubic: a smooth projective plane curve of degree $d = 3$ , so $C$ is a smooth projective geometrically integral curve over $k$ .

Adjunction for smooth plane curves gives $ω_{C} ≅ O_{C} (d - 3) = O_{C} (0) = O_{C},$ and the genus formula gives $g (C) = (d - 1) (d - 2) / 2 = 1$ , consistently with $\deg_{k} ω_{C} = d (d - 3) = 0 = 2 g - 2$ . Since $h^{0} (C, ω_{C}) = g = 1$ and $ω_{C}$ has degree $0$ with a nonzero global section, $ω_{C}$ is trivial; equivalently, every canonical divisor of $C$ is a principal divisor, and the canonical class is the zero element of ${Pic}^{0} (C)$ .

The complete canonical linear system therefore has dimension $0$ and its associated canonical morphism has target $P_{k}^{0}$ . Thus the complete canonical linear system has no positive-dimensional projective target. This is the exceptional case of the genus-one behaviour: the degree-three line bundle $O_{C} (3 p_{0})$ at a $k$ -rational point $p_{0}$ is what embeds such a curve as a plane cubic, conversely to the computation above.

Facts & Assumptions

Given: the Axiom of Choice and its consequence Dependent Choice; a field $k$ and a smooth plane cubic $C = V_{+} (F) \subseteq P_{k}^{2}$ of degree $d = 3$ .

[F1]

For a smooth plane curve $C = V_{+} (F) \subseteq P_{k}^{2}$ of degree $d$ , adjunction gives $ω_{C} ≅ O_{C} (d - 3)$ , and the genus is $(d - 1) (d - 2) / 2$ ; the degree of the degree- $d$ hypersurface is $\deg F = d$ . (Adjunction for smooth plane curves, The genus of a smooth plane curve in terms of its degree, degree projective hypersurface)

[F2]

For a smooth proper geometrically integral curve of genus $g$ , $\deg_{k} ω_{C} = 2 g - 2$ and $h^{0} (C, ω_{C}) = g$ , with $ω_{C} = O_{C} (K_{C})$ the canonical bundle. (The canonical divisor has degree 2g - 2, The canonical bundle has exactly g independent sections, Canonical bundle and canonical divisors, Degree divisor proper curve)

[F3]

An invertible sheaf of degree $0$ on a smooth proper curve that has a nonzero global section is trivial; equivalently, an effective divisor of degree $0$ is $0$ , so a degree-zero divisor whose sheaf has a section is principal. (A degree-zero line bundle with a nonzero section is trivial, Rational sections of line bundles are Cartier divisors, Invertible sheaves)

[F4]

A genus-one curve over $k$ with a $k$ -rational point $p_{0}$ embeds as a smooth plane cubic via the degree-three very ample invertible sheaf $O_{C} (3 p_{0})$ ; and on a genus-one curve the canonical bundle is trivial. (A genus-one curve with a rational point embeds as a plane cubic, The canonical bundle of a genus-one curve is trivial)

[F5]

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

[F6]

In ZF, the Axiom of Choice implies Dependent Choice; this supplies the Dependent Choice premise of the Cartier-to-Weil dictionary used in [F3] and the cited genus-one and degree suppliers. (AC implies DC implies countable choice, The axiom of dependent choice: a relation in which every element is related to something admits an $N$ -indexed chain)

Verification

Proof technique: specialize adjunction and the genus formula to $d = 3$ , then apply the degree-zero triviality criterion.

1.1F1

By [F1] with $d = 3$ , $ω_{C} ≅ O_{C} (0) = O_{C}$ and $g (C) = (3 - 1) (3 - 2) / 2 = 1$ .

2.1F2F3step 1.1

By [F2] with $g = 1$ , $\deg_{k} ω_{C} = 0$ and $h^{0} (C, ω_{C}) = g = 1$ ; the unique one-dimensional space of sections is nonzero, so [F3] applies to the degree-zero invertible sheaf $ω_{C}$ and shows $ω_{C} ≅ O_{C}$ ; equivalently every canonical divisor is principal and the canonical class is $0$ in ${Pic}^{0} (C)$ .

2.2F4step 1.1

Conversely, if $C$ is a genus-one curve over $k$ with a $k$ -rational point $p_{0}$ , then $O_{C} (3 p_{0})$ has degree $3 = 2 g + 1$ , so by [F4] it is very ample and embeds $C$ as a plane cubic; thus every genus-one curve with a rational point has a smooth plane-cubic model. The forward calculation applies to every smooth plane cubic without assuming a rational point: its canonical class is zero in ${Pic}^{0}$ . This proves the stated converse implication and does not imply that every smooth plane cubic has a rational point.

3.1F2F4step 2.1

Since $h^{0} (C, ω_{C}) = 1$ , the complete canonical linear system has dimension $ℓ (K_{C}) - 1 = 0$ and its associated complete canonical morphism has target $P_{k}^{0}$ ; it supplies no positive-dimensional canonical target. This matches the direct computation $ω_{C} ≅ O_{C}$ of Step 2.1 and the general genus-one statement [F4].

4.1F5F6F1F2F3F4step 2.2∎

The Axiom of Choice is used through the cohomology, degree, and divisor suppliers; [F6] supplies the Dependent Choice premise used by the Cartier-to-Weil divisor dictionary.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

120 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

William Fulton, Algebraic Curves (Internet Archive copy) (standard reference, not scraped)
The Stacks Project, Algebraic Curves (tag 0BRV) (standard reference, not scraped)