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 morphism from an open subset of a classical affine variety to an affine variety
Definition
Let be open in an affine algebraic set and let be an affine algebraic set. A set map is a morphism over if for every . For a map whose target is an open subset of an affine algebraic set, the phrase locally regular morphism means a continuous map pulling regular functions on each target open back to regular functions on its inverse image. An isomorphism between open subsets of affine algebraic sets is a bijection for which the map and its inverse are locally regular morphisms. Continuity and this local pullback property for the affine-target definition will be established in the next lemma; they are not assumed in the affine-target test.
Sources
Source comparison: Milne, Algebraic Geometry, v6.10, §3d and Proposition 3.26, pp. 64–67. Conventions here distinguish arbitrary affine algebraic sets from nonempty irreducible varieties.
Depends on
Used by
- A classical affine open subset and its coordinate ring Definition
- A rational map as an equivalence class of morphisms on nonempty opens Definition
- Images and set-theoretic fibres of classical regular maps Definition
- Integral classical varieties in the compatible affine-atlas register Definition
- A classical morphism pulls Zariski closed sets back to closed sets Lemma
- Affine-source morphisms agreeing on a dense open agree everywhere Lemma
- Compatible classical morphisms to an affine target glue over an open cover Lemma
- Morphisms defined on an open source and agreeing on a dense open agree on their common domain Lemma
- Classical affine morphisms are contravariantly equivalent to coordinate-ring homomorphisms Theorem
- Every nonempty principal open is a classical affine variety Theorem
Dependency tree · two levels
5 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, §3d and Proposition 3.26, pp. 64–67 (standard reference, not scraped)