ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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 affine line is an algebraic space

Example

Assume the Axiom of Choice inherited from the quotient/sheaf and descent suppliers (The Axiom of Choice). Let $k$ be a field and let $A_{k}^{1} = Spec k [x]$ be the affine line (Affine schemes and their coordinate rings, Schemes and morphisms over a base). Then $A_{k}^{1}$ is an algebraic space over $k$ (Algebraic spaces over a scheme, defined as fppf sheaves). A presentation is given by $U = A_{k}^{1}$ , the diagonal equivalence relation $R = Δ (A_{k}^{1}) \subseteq A_{k}^{1} \times_{k} A_{k}^{1}$ with its two projections (Groupoids in schemes, relations and etale equivalence relations), and the identity $U \to A_{k}^{1}$ ; more generally every $k$ -scheme is an algebraic space (Every representable functor is an algebraic space).

Verification

Given: A field $k$ , the affine line $A_{k}^{1} = Spec k [x]$ , and the represented presheaf $h_{A_{k}^{1}}$ .

[F1] Every $k$ -scheme $T$ represents an algebraic space $h_{T}$ over $k$ : $h_{T}$ is an fppf sheaf, its diagonal is representable by schemes, and the identity is a representable etale surjective cover (Every representable functor is an algebraic space).

[F2] The diagonal $Δ ⁣ : A_{k}^{1} \to A_{k}^{1} \times_{k} A_{k}^{1}$ is a closed immersion and the two projections $R = Δ (A_{k}^{1}) \to A_{k}^{1}$ are isomorphisms; diagonals are monomorphisms, so $R \to A_{k}^{1} \times_{k} A_{k}^{1}$ is a monomorphism and $R$ is an étale equivalence relation on $A_{k}^{1}$ with respect to the projections (Groupoids in schemes, relations and etale equivalence relations, Fibre product of schemes).

1.1F1

$h_{A_{k}^{1}}$ is an algebraic space over $k$ by [F1] applied to $T = A_{k}^{1}$ , with the identity as its etale scheme cover.

2.1F1F2∎

The presentation $R ⇉ U \to A_{k}^{1}$ with $U = A_{k}^{1}$ , $R = Δ (A_{k}^{1})$ and the two projections is exactly the kernel pair of the identity: the projections are isomorphisms, the comparison map $R = U \times_{A_{k}^{1}} U$ is the diagonal, and the coequalizer of the two projections is $A_{k}^{1}$ itself; by [F2] the diagonal relation is an equivalence relation on $U$ over $k$ , and both projections are etale because they are isomorphisms. This exhibits the asserted presentation, and the final claim that every $k$ -scheme is an algebraic space is [F1].

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

22 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, Chapter 65 (Algebraic Spaces), Lemma 65.6.2 (standard reference, not scraped)