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.
regular function projective variety
Definition
For a classical projective variety , the homogeneous coordinate ring is a graded domain by the choice-free irreducibility clause of projective irreducibility homogeneous prime. Its fraction field exists by is a field and embeds the integral domain . Define its field of rational functions to be the degree-zero subfield This is a subfield: multiplying fractions adds numerator and denominator degrees equally, adding them uses a common homogeneous denominator, and a nonzero fraction is inverted by interchanging its numerator and denominator. Zero is represented by .
A rational function is regular at if for such homogeneous with . It is regular on if it is regular at every point of . Evaluation is independent of a homogeneous representative because the numerator and denominator scale by the same power; two expressions for the same fraction have equal cross products and hence equal values wherever both denominators are nonzero.
For an open subset , write for the ring of actual functions that are locally evaluations of such equal-degree fractions with nonvanishing denominator. For this is the one-element zero ring. For nonempty , these functions identify with the rational functions regular everywhere on : any two local representatives agree as fractions, since their cross difference is homogeneous and vanishes on a nonempty open of the irreducible space , hence on . Nonempty opens intersect, and a homogeneous zero locus is closed, which justifies this assertion. Thus any one local representative gives the common rational function. This construction uses no Axiom of Choice.