Alphabeta MathHow 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.
Finite morphisms of schemes
Definition
A morphism of schemes is finite if, for every affine open , its inverse image is affine, , and the induced -algebra is module-finite over in the sense of Subalgebra generated by a subset, algebras of finite type, and module-finite algebras. The affineness language agrees with Affine morphisms. The zero ring is allowed, so an empty inverse image satisfies the condition.
Depends on
Used by
- Finite morphisms are proper Corollary
- Global functions on geometrically connected and geometrically reduced proper schemes Corollary
- Frobenius on the affine line is finite flat but not smooth Counterexample
- Closed immersion from a quotient ring Example
- Finite field extensions and etaleness Example
- Finite power map of the affine line Example
- The empty morphism is finite, proper and projective Example
- Closed immersions are proper Lemma
- Finite decomposition around isolated fibre points after an elementary étale change Lemma
- Finite is affine and local on its target Lemma
- Finite morphisms survive base change and composition Lemma
- Finite neighbourhood of an isolated fibre point after elementary etale change Lemma
- Finite pullback preserves absolute ampleness Lemma
- Finite-fibre and pointwise characterizations of quasi-finiteness Lemma
- Scheme Zariski Main factorization for separated quasi-finite morphisms Lemma
- A proper quasi-finite morphism is finite Theorem
- Finite and finite type etale schemes over an algebraically closed field Theorem
- Finite morphisms are integral and universally closed Theorem
Dependency tree · two levels
9 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
- Stacks Project, Morphisms of Schemes §29.45 (standard reference, not scraped)
- Vakil, The Rising Sea §§8.3, 11.3, 17.4 (standard reference, not scraped)