ExampleConstruction: AI-generatedVerification: AI-adaptedPipeline-generatedaudited 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.

A linear system with and without a base point

Example

Assume the Axiom of Choice as inherited from the projective-space constructions (The Axiom of Choice). On $P_{k}^{1}$ with coordinate $t$ and $D = 2 [\infty]$ (Two-affine projective line and its twists, Divisors on a smooth proper curve), put $V = span (1, t^{2}) \subseteq L (D), W = span (t, t^{2}) \subseteq L (D) .$ Both are two-dimensional subspaces of $L (D)$ (The space L(D)), so base-point-freeness is a property of the chosen subsystem and not of its degree. The subspace $V$ is base-point-free and defines the degree-two morphism $φ_{V} : P_{k}^{1} \to P_{k}^{1}$ , $[1 : t] \mapsto [1 : t^{2}]$ ; the subspace $W$ has $t = 0$ as its unique base point, and its associated rational map is $[t : t^{2}] = [1 : t]$ on $P_{k}^{1} ∖ {0}$ , which extends to the identity morphism of $P_{k}^{1}$ . The pair $(t, t^{2})$ does not generate $O (D)$ at its base point, so the base-point-free construction for this line bundle does not apply to that pair. In the set identification $∣ D ∣ ≅ P (L (D)) ≅ P_{k}^{2} (k)$ of Divisors and complete linear systems on the projective line, use coordinates $(a, b, c)$ for $a + b t + c t^{2}$ . The associated projective parameter scheme is $P (L (D)) ≅ P_{k}^{2}$ ; the intersections below are scheme intersections in this parameter scheme. If $char k \neq 2$ , the discriminant conic $b^{2} = 4 a c$ is smooth, $P (W) : a = 0$ is tangent to it at $2 [0]$ , and $P (V) : b = 0$ is the secant through $2 [0]$ and $2 [\infty]$ . If $char k = 2$ , the discriminant scheme is the double line $b^{2} = 0$ ; its reduced support $b = 0$ is the geometric doubled-divisor locus, and the coordinate-square map $[T : S] \mapsto [T^{2} : 0 : S^{2}]$ is onto that support as a morphism. Then $P (V)$ is the support line, while $P (W)$ meets it at $2 [0]$ and meets the double discriminant in a length-two point. Over an imperfect field, not every $k$ -point of the support need come from a $k$ -rational doubled divisor.

Facts & Assumptions

Given: A field $k$ , the projective line $P_{k}^{1}$ with coordinate $t$ on $U_{0} = Spec k [t]$ , the point at infinity $\infty$ the pole of $t$ , the divisor $D = 2 [\infty]$ , and the two subspaces $V = span (1, t^{2})$ , $W = span (t, t^{2})$ of $L (D)$ .

[F1]

On $P_{k}^{1}$ one has $div (t) = [0] - [\infty]$ and, for a nonzero polynomial $p$ of degree $m$ , $div (p) = Z (p) - m [\infty]$ , where $Z (p)$ is the effective divisor of the affine zeros of $p$ ; $\deg_{k} (2 [\infty]) = 2$ , and the constant function $1$ has $div (1) = 0$ . (Divisors and complete linear systems on the projective line, Divisors on a smooth proper curve, Degree divisor proper curve)

[F2]

$L (D) = {f \in k (P^{1})^{\times} : div (f) + D \geq 0} \cup {0}$ is the $k$ -subspace of rational functions with poles bounded by $D$ . (The space L(D))

[F3]

A nonzero $f \in L (D)$ vanishes at a closed point $x$ when ${ord}_{x} (f) + n_{x} \geq 1$ , where $n_{x}$ is the coefficient of $D$ at $x$ ; $x$ is a base point of a subspace $V \subseteq L (D)$ when every nonzero $f \in V$ vanishes at $x$ ; $V$ is base-point-free when it has no base point, equivalently when the evaluation morphism of a basis of $V$ is surjective. (Base points and base-point-free linear systems)

[F4]

A base-point-free subspace $V \subseteq L (D)$ of dimension $r + 1 \geq 1$ determines a $k$ -morphism $φ_{V} : P_{k}^{1} \to P_{k}^{r}$ with $φ_{V}^{*} O (1) ≅ O (D)$ under which the coordinate sections pull back to a basis of $V$ ; for generating sections $s_{0}, \dots, s_{r}$ the chart formula $x_{j}^{(i)} \circ φ = s_{j} / s_{i}$ holds on the locus where $s_{i}$ is invertible, and two morphisms to the separated reduced $k$ -scheme $P_{k}^{r}$ agreeing on a dense open are equal. (A base-point-free linear system defines a morphism to projective space, Generating line-bundle sections define a morphism to projective space, Agreement on a schematically dense open)

[F5]

For $d \geq 0$ the complete linear system $∣ d [\infty] ∣$ is in bijection with $P (L (d [\infty]))$ , the set of $k$ -lines in $L (d [\infty])$ , and consists of the effective divisors of degree $d$ ; for $D = 2 [\infty]$ the associated morphism of the complete system is the degree-two Veronese map $ν_{1, 2} : P_{k}^{1} \to P_{k}^{2}$ , $[x_{0} : x_{1}] \mapsto [x_{0}^{2} : x_{0} x_{1} : x_{1}^{2}]$ , and $∣ D ∣ ≅ P (L (D)) ≅ P_{k}^{2} (k)$ . The projective parameter scheme $P (L (D)) ≅ P_{k}^{2}$ has this set of $k$ -points, with coefficient coordinates $(a, b, c)$ for $a + b t + c t^{2}$ ; the inclusions of $V, W$ give projective linear subschemes $P (V), P (W)$ in it. (Divisors and complete linear systems on the projective line, Complete linear system)

[F6]

The divisor-doubling map in coefficient coordinates is $[T : S] \mapsto [T^{2} : - 2 T S : S^{2}]$ and lies in the discriminant scheme $b^{2} = 4 a c$ . If $char k \neq 2$ , its image is the smooth conic, and its $k$ -points are exactly the squares of linear forms up to nonzero scalar. If $char k = 2$ , the discriminant scheme is $b^{2} = 0$ , a double line with reduced support $b = 0$ ; the doubling map becomes $[T : S] \mapsto [T^{2} : 0 : S^{2}]$ and has that reduced line as its scheme-theoretic image. It is surjective onto the support geometrically, while its image on $k$ -points can be smaller over an imperfect field. (Divisors and complete linear systems on the projective line, Complete linear system)

[F7]

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

Proof

technique · direct; test the two subspaces against the vanishing criterion, compute their chart maps, and read their pencils off the model of the projective line

1.1F1F2F5

The two subspaces. By [F1], $div (1) + 2 [\infty] = 2 [\infty] \geq 0$ , $div (t) + 2 [\infty] = [0] + [\infty] \geq 0$ , $div (t^{2}) + 2 [\infty] = 2 [0] \geq 0$ , so $1, t, t^{2} \in L (2 [\infty])$ and $V, W$ are subspaces of $L (D)$ ; the pairs $(1, t^{2})$ and $(t, t^{2})$ are linearly independent over $k$ , so $\dim_{k} V = \dim_{k} W = 2$ and $V, W$ are two-dimensional subsystems of the degree-two complete system $∣ D ∣$ .

1.2F1F3F4

$V$ is base-point-free and defines $t \mapsto t^{2}$ . Since $div (1) + 2 [\infty] = 2 [\infty]$ is supported at $\infty$ , the function $1$ does not vanish at any closed point $x \neq \infty$ , so no point other than possibly $\infty$ is a base point of $V$ ; and since $div (t^{2}) + 2 [\infty] = 2 [0]$ is supported at the origin, $t^{2}$ does not vanish at $\infty$ , so $\infty$ is not a base point either [F3]. Hence $V$ is base-point-free, and [F4] attaches to $V$ a morphism $φ_{V} : P_{k}^{1} \to P_{k}^{1}$ with $φ_{V}^{*} O (1) ≅ O (D)$ , whose coordinate sections pull back to $1, t^{2}$ ; on the chart where $1$ is invertible, which is $P_{k}^{1} ∖ {\infty}$ , the chart formula gives $φ_{V} ([1 : t]) = [1 : t^{2}]$ , the degree-two map $t \mapsto t^{2}$ .

1.3F1F3F4

$W$ has the base point $0$ , but its rational map extends. Every nonzero $f = α t + β t^{2} = t (α + β t) \in W$ has ${ord}_{0} (f) \geq 1$ while the coefficient of $D$ at $0$ is $n_{0} = 0$ , so every such $f$ vanishes at the origin [F3]; and no other point is a base point, since $t$ does not vanish at closed points $x \neq 0, \infty$ while $t^{2}$ does not vanish at $\infty$ [F1, F3]. Hence the base locus of $W$ is exactly ${0}$ , and its two sections do not generate $O (D)$ there, so [F4]'s base-point-free construction does not attach a morphism from this pair with pullback line bundle $O (D)$ . On the complement of $0$ , however, the pair defines $[t : t^{2}] = [1 : t]$ , the identity rational map, which extends to the identity morphism of $P_{k}^{1}$ . The rational map extension is unique because morphisms to the separated target $P_{k}^{1}$ agreeing on a dense open are equal [F4].

2.1F5F6step 1.1step 1.2step 1.3

The pencil picture in the parameter scheme $P (L (D)) ≅ P_{k}^{2}$ . By [F5], this scheme has coefficient coordinates $(a, b, c)$ for $a + b t + c t^{2}$ , and the subspaces correspond to $P (V) : b = 0$ and $P (W) : a = 0$ . The divisor-doubling map of [F6] is $[T : S] \mapsto [T^{2} : - 2 T S : S^{2}]$ ; its coefficient image satisfies $b^{2} = 4 a c$ , with $2 [0] = (0, 0, 1)$ and $2 [\infty] = (1, 0, 0)$ . If $char k \neq 2$ , this is a smooth conic. On $P (W)$ , $a = 0$ forces $b^{2} = 0$ , so the intersection is the length-two point $2 [0]$ and $P (W)$ is tangent there. On $P (V)$ , $b = 0$ forces $a c = 0$ , giving the two distinct points $2 [0]$ and $2 [\infty]$ ; thus $P (V)$ is a secant. In this characteristic, a pencil has a base point exactly when its line is tangent to the doubled-divisor conic, consistent with steps 1.2 and 1.3.

If $char k = 2$ , the discriminant scheme is $b^{2} = 0$ , the double of the reduced support line $b = 0$ . The doubling map becomes $[T : S] \mapsto [T^{2} : 0 : S^{2}]$ ; on either standard affine chart its coordinate map is $w \mapsto w^{2}$ , so it is finite and surjective onto that support as a morphism, although it need not be onto its $k$ -points when $k$ is imperfect. Thus $P (V)$ is the reduced support of the geometric doubled-divisor locus, while $P (W)$ meets that support at $2 [0]$ . Its intersection with the double discriminant has local ring $k [b] / (b^{2})$ at that point and therefore length two. The characteristic-not-two tangent/secant description is not asserted in characteristic two. [F6]

3.1F4F7step 1.2step 1.3step 2.1∎

Conclusion. On $P_{k}^{1}$ with $D = 2 [\infty]$ , $V = span (1, t^{2})$ is base-point-free and defines $[1 : t] \mapsto [1 : t^{2}]$ , while $W = span (t, t^{2})$ has the single base point $0$ and its rational map extends to the identity morphism (steps 1.2–1.3). Both subsystems have degree two, so base-point-freeness depends on the chosen subsystem and not its degree. Their pencil geometry is the tangent/secant picture of step 2.1 in characteristic not two; in characteristic two, $P (V)$ is the reduced support of the double discriminant and $P (W)$ meets the doubled scheme in a length-two point. The Axiom of Choice is inherited from the projective-space constructions of [F4] and [F7], and no further selection is used.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

92 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, Algebraic Curves (tag 0BRV) (standard reference, not scraped)
Ravi Vakil, The Rising Sea (version of October 21, 2025), Chs. 19 and 21 (standard reference, not scraped)