TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedaudited 2026-09-09

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 rational map to an affine target has a unique maximal open domain

Statement

The candidate domain of a rational map $Φ : X ⇢ Y$ with affine target supports a unique morphism restricting to every representative. It is a representative of $Φ$ , and is the unique maximal representative domain.

Facts & Assumptions

Given: A rational-map class $Φ : X ⇢ Y$ for affine varieties over algebraically closed $k$ .

[F1]

The candidate domain is the union of all representative domains (The candidate domain of a rational map).

[F2]

Equivalence of representatives is an equivalence relation (The rational-map relation is transitive).

[F3]

Equivalent maps agree on their entire common domain (Morphisms defined on an open source and agreeing on a dense open agree on their common domain).

[F4]

Compatible morphisms on an open cover glue uniquely (Compatible classical morphisms to an affine target glue over an open cover).

Proof

technique · direct

1.1

Any two representatives belong to the same equivalence class, so F2 supplies agreement on a nonempty common open. F3 extends this to their whole overlap. Thus the representatives form a compatible open cover of the candidate domain D from F1. F4 glues them to a unique morphism $ϕ_{D} : D \to Y$ .

F1F2F3F4given

2.1

The set D is nonempty open, and its glued map agrees with any given representative on that representative’s nonempty domain. Thus $(D, ϕ_{D})$ belongs to $Φ$ . Every representative domain is contained in D by its definition. Consequently D is maximal and any other maximal representative domain must equal D; F4 gives uniqueness of the map there as well.

F1F4step 1.1∎

Sources

Source comparison: Milne, Algebraic Geometry, v6.10, §5l p. 117. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.

Depends on

Used by

Dependency tree · two levels

10 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

J. S. Milne, Algebraic Geometry v6.10, §5l p. 117 (standard reference, not scraped)