DefinitionDefinition: Literature-sourcedProof: Not applicablejudge pass (gpt-5.6-terra)audited 2026-09-06

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.

projective space points

Definition

Fix an algebraically closed field $k$ . For $n \geq 0$ , define $P_{k}^{n} = (k^{n + 1} ∖ {0}) / \sim$ , where $a \sim b$ exactly when $b = λ a$ for some $λ \in k^{\times}$ . Write a class as $[a_{0} : \dots : a_{n}]$ . Thus $P_{k}^{0} = {[1]}$ .

Used by

A line meets a degree-d curve in d points counted with multiplicity Corollary
General hypersurfaces give smooth complete intersections Corollary
Bezout fails on the affine plane because points at infinity are missing Counterexample
inhomogeneous equation not projectively well defined Counterexample
The Euler characteristic does not determine the signature Counterexample
Linear systems of plane curves and their base loci Definition
Linear systems, base loci, and general members Definition
morphism to projective space homogeneous coordinates Definition
Plane projective curves and their components Definition
projective algebraic set Definition
Projective scheme of a homogeneous quotient and its standard affine charts Definition
The degree-d Veronese map Definition
The Segre point map from two projective spaces Definition
A binary resultant detects a common root at infinity lost by naive dehomogenization Example
A nondegenerate projective quadric Example
A projective cone with a smooth conic base Example
A singular cubic outside the lattice family Example
Nonsingular affine and projective curves as Riemann surfaces Example
projective line two affine charts Example
Resultant of two binary linear forms Example
Curves without a common component meet finitely often Lemma
Hilbert divisor charts and the Picard diagonal Lemma
homogeneous polynomial zero locus well defined Lemma
Intersection with a line is the order of vanishing of the restricted equation Lemma
Local holomorphic charts on nonsingular complex algebraic curves Lemma
Scaling, specialization, and the affine and infinite charts of a binary resultant Lemma
standard projective opens are affine spaces Lemma
The resultant detects finitely many common projective points Lemma
Bertini smoothness away from the base locus Theorem
Closed projective embedding from a radical homogeneous ideal Theorem
Nonvanishing of the lattice discriminant Theorem
The binary Sylvester resultant detects a common geometric projective root Theorem
The chord-tangent group law and elliptic uniformization Theorem
The chord-tangent group law on a smooth short Weierstrass cubic Theorem
The torus is biholomorphic to its Weierstrass cubic Theorem

Dependency tree · 0 levels

Nothing. This result depends on no other item in the library.

Sources

J. S. Milne, Algebraic Geometry, Chapter 6 (standard reference, not scraped)
Michael Artin, Algebraic Geometry, Chapter 3 (standard reference, not scraped)