Alphabeta MathFinite Proper and Projective Morphisms
About this page
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.
✓ 35 results · all verified · 28 also independently AI-judged
Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 7 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.
1 · Prerequisites
Abstract Algebra
- Algebraic Closure, Embeddings, and Separability
- Algebraic Extensions, Extension Degree, and Finite Fields
- Binary Operations, Monoids, Groups and Subgroups
- Chain Conditions, Semisimple Modules and the Wedderburn–Artin Theorem
- Cosets, Index and Lagrange's Theorem
- Divisibility, Euclidean Domains, Principal Ideal Domains and Unique Factorisation
- Finite Fields and Cyclotomic Extensions
- Free Modules, Exact Sequences, Projective and Injective Modules
- Group Actions, Orbits, Stabilisers and Cayley's Theorem
- Group Homomorphisms and the Isomorphism Theorems
- Ideals, Quotient Rings and the Isomorphism Theorems for Rings
- Modules, Submodules, Quotient Modules and the Isomorphism Theorems
- Normal Subgroups and Quotient Groups
- Polynomial Rings, the Division Algorithm and Roots
- Rings, Subrings, Integral Domains and Fields
- Simple Field Extensions and the Construction of the Complex Numbers
- Splitting Fields
- Tensor Products of Modules
- The Field of Fractions and Localisation
Algebraic Geometry
Category Theory
Commutative Algebra
- Algebraic Zariski Main for Quasi-Finite Morphisms
- Flatness and Faithful Flatness
- Homogeneous Resultants and Projective Intersection Length
- Integral Extensions and Going Up
- Localisation of Modules and Support
- Noether Normalisation and Nullstellensatz
- Noetherian Rings and Hilbert Basis
- Prime Spectra and Radicals
- Regular Local Rings and Homological Dimension
- Valuation Rings and Discrete Valuation Rings
- Zariski Topology on Prime Spectra
Linear Algebra
- Determinants of Matrices over a Commutative Ring
- Eigenvalues, Eigenvectors and the Characteristic Polynomial
- Linear Independence, Bases and Dimension
- Linear Transformations, Rank-Nullity and Quotient Spaces
- The Determinant of a Linear Operator, Cofactors and Cramer's Rule
- Vector Spaces, Linear Subspaces, Span and Direct Sums
Real Analysis
- Construction of the Real Numbers via Cauchy Sequences
- Construction of the Real Numbers via Dedekind Cuts
- Countability and Uncountability
- Foundations of the Real Numbers for Analysis
- Monotone Sequences, Bolzano-Weierstrass, and Cauchy Completeness
- Roots, Rational Powers, and Classical Inequalities
- Suprema and Infima
- Topology of ℝ
Scheme Theory
- Affine Schemes and the Structure Sheaf
- Diagonals Separated Morphisms and Valuative Uniqueness
- Fibre Products Base Change and Scheme Theoretic Fibres
- Presheaves Sheaves Stalks and Sheafification
- Schemes Subschemes and Morphisms Locally of Finite Type
- Sheaf Operations Exactness Ringed Spaces and Module Pullback
Set Theory
- Cardinal Arithmetic, Cofinality and the Alephs
- Construction of the Natural Numbers
- Order, Zorn's Lemma, and the Axiom of Choice
- Ordinal Arithmetic and the First Uncountable Ordinal
- Ordinals, Cardinals, and Transfinite Recursion
- Relations, Functions, and Quotients
- The ZFC Axioms and the Basic Set Constructions
2 · Logical flowchart
3 · Items
Definition
Affine-local quasi-coherent algebras before general sheaf theory
Definition
Fpqc covering morphisms
Lemma
Fpqc covers are universally submersive
Lemma
Fpqc descent of properness components
Definition
Projective morphisms before Proj
Definition
Quasi-finite morphisms of schemes
Lemma
Finite-fibre and pointwise characterizations of quasi-finiteness
Definition
Universally closed morphisms
Definition
Finite morphisms of schemes
Lemma
Finite is affine and local on its target
Lemma
Finite morphisms survive base change and composition
Definition
Proper morphisms
Lemma
Properness survives arbitrary base change
Lemma
Properness survives composition
Lemma
Properness is local on the target
Definition
Complete varieties
Definition
Quasi-projective morphisms before Proj
Lemma
Affine pushforward algebra localizes
Lemma
Glue relative spectra of affine-local algebras
Theorem
Affine morphisms are relative spectra
Lemma
Closed immersions are affine quotients and survive base change
Lemma
Function field of an integral finite-type scheme
Lemma
A quasi-compact image stable under specialization is closed
Lemma
Valuation lifts detect universal closedness
Definition
Algebraic independence in a field extension
Lemma
A finite-type field has finite relative algebraic constants
Lemma
Line bundles on projective three-space and their restrictions
Theorem
Proper morphisms are closed
Theorem
Valuative criterion for properness
Lemma
Fibres of proper morphisms are proper
Remark
Properness is not a compactness claim on rational points
Theorem
Finite morphisms are integral and universally closed
Definition
Birational morphisms of integral finite-type schemes
Lemma
Birational morphisms restrict to isomorphisms between principal affine opens
Lemma
Proper closed subsets of a curve are finite
Corollary
Proper birational normal curves agree off finitely many points
Lemma
Projective space is of finite type over its base
Theorem
Finite-dimensional projective space is proper over every base
Lemma
Pushouts of closed immersions exist
Lemma
Closed gluing of two projective three-spaces is proper
Theorem
Properness descends through fpqc base change
Corollary
Finite morphisms are proper
Lemma
Closed immersions are proper
Lemma
Morphisms from a proper scheme to a separated one are proper
Theorem
Projective morphisms are proper
Lemma
The twist index on the projective line is an isomorphism invariant
Remark
Projective and proper are distinct notions
Theorem
Global functions on proper integral schemes form a finite extension of the base field
Corollary
Maps from proper integral schemes to the affine line have closed-point image
Sources
- Stacks Project, Morphisms of Schemes §§29.11, 29.42–45
- Stacks Project, Schemes, §26.5 Definition 26.5.3 and Lemma 26.5.4
- Stacks Project, Morphisms of Schemes, §29.26 Definition 29.26.1
- Stacks Project, Étale Cohomology, §59.15 Definition 59.15.1 and Example 59.15.3(3)
- Stacks Project, Topologies on Schemes, §34.9 Definition 34.9.1
- Stacks Project, Morphisms of Schemes, §29.26, Lemmas 29.26.2, 29.26.3, 29.26.8, and 29.26.12
- Stacks Project, Commutative Algebra, Lemma 10.41.5
- \"Stacks Project, Descent, §35.23, Lemmas 35.23.1, 35.23.3, 35.23.6, 35.23.12, 35.23.14, and 35.23.16\"
- \"Stacks Project, Commutative Algebra, Lemma 10.126.1\"
- \"Stacks Project, Morphisms of Schemes, Lemma 29.26.12\"
- Stacks Project, Morphisms of Schemes, §29.44 Definition 29.44.1(2)
- Stacks Project, Morphisms of Schemes, §29.21 Definition 29.21.1 and Lemma 29.21.6
- Stacks Project, Commutative Algebra, §10.122 Definition 10.122.3
- Stacks Project, Morphisms of Schemes, §29.21 Definition 29.21.1 and Lemmas 29.21.3, 29.21.5–7, 29.21.10
- Stacks Project, Commutative Algebra, Lemma 10.122.1
- Stacks Project, Commutative Algebra, Lemma 10.122.2
- Stacks Project, Commutative Algebra, Definition 10.122.3
- Stacks Project, Varieties, Lemma 33.20.2
- Stacks Project, Schemes, §26.20 Definition 26.20.1
- Stacks Project, Morphisms of Schemes §29.45
- Vakil, The Rising Sea §§8.3, 11.3, 17.4
- Stacks Project, Morphisms of Schemes, Lemma 29.45.3
- Stacks Project, Algebra, Lemma 10.36.14(2)
- Stacks Project, Morphisms of Schemes, §§29.11 and 29.45
- Stacks Project, Morphisms of Schemes, Lemmas 29.45.5–29.45.6
- Stacks Project, Algebra, Lemma 10.7.3
- Stacks Project, Algebra, Lemma 10.36.13
- Stacks Project, Morphisms of Schemes, §29.42 Definition 29.42.1
- Stacks Project, Morphisms of Schemes, Lemma 29.42.5 (tag 01W4)
- Stacks Project, Morphisms of Schemes, Lemma 29.42.4 (tag 01W3)
- Stacks Project, Schemes, Lemma 26.21.12 (tag 01KU)
- Stacks Project, Schemes, Lemma 26.21.9 (tag 01KR)
- Stacks Project, Morphisms of Schemes, Lemma 29.15.3 (tag 01T3)
- Stacks Project, Schemes, Lemma 26.19.4 (tag 01K6)
- The Stacks Project, Morphisms of Schemes, Lemma 29.42.3 (tag 01W2)
- Ravi Vakil, Foundations of Algebraic Geometry, 2011 public draft, §11.3.1
- Stacks Project, Morphisms of Schemes, §29.41 Definition 29.41.1(2)
- Stacks Project, Morphisms of Schemes, §29.11 Lemma 29.11.3
- Stacks Project, Constructions of Schemes, §27.2 Lemma 27.2.1
- Stacks Project, Constructions of Schemes, §27.3 Relative spectrum via glueing
- Stacks Project, Morphisms of Schemes, Lemma 29.11.3
- The Stacks Project, Schemes, Lemma 26.8.2 (tag 01IH)
- The Stacks Project, Schemes, Lemma 26.10.1 (tag 01IN)
- The Stacks Project, Varieties, Definition 33.9.1 (tag 020H)
- The Stacks Project, Schemes, Lemma 26.19.7 (tag 05JL)
- The Stacks Project, Commutative Algebra, Lemma 10.41.5 (tag 00HY)
- Stacks Project, Schemes, Lemma 26.19.8 (tag 01K9)
- Stacks Project, Schemes, Lemmas 26.20.2, 26.20.4–5 and Proposition 26.20.6 (tags 01KC, 01J8, 01KE, 01KF)
- The Stacks Project, Fields, Definition 9.26.1 (tag 030D)
- The Stacks Project, Fields, Lemma 9.26.11 (tag 037J)
- The Stacks Project, Fields, Lemma 9.26.10 (tag 0G1M)
- The Stacks Project, Fields, Definition 9.26.9 (tag 037I)
- The Stacks Project, Fields, Lemma 9.8.6 (tag 09GH)
- Stacks Project, Divisors, Lemma 31.29.5
- Stacks Project, Divisors, Lemma 31.29.4
- Stacks Project, More on Algebra, Lemma 15.119.3
- Vakil, The Rising Sea §§17.4.8–12
- The Stacks Project, Morphisms of Schemes, Definition 29.42.1 (tag 01W0) and Section 29.41
- Vakil, The Rising Sea, Proposition 11.3.2 and the discussion of properness in §11.3
- The Stacks Project, Morphisms of Schemes, Lemma 29.43.1 (tag 0BX5), valuative criterion for properness
- The Stacks Project, Schemes, Lemma 26.22.1 (tag 01KZ) and Lemma 26.22.2 (tag 01L0)
- Vakil, The Rising Sea, Theorem 11.3.11 and the valuative criteria of §13.7
- The Stacks Project, Morphisms of Schemes, Lemma 29.42.5 and the fibre definition of Section 29.20
- Vakil, The Rising Sea, §11.3.4
- The Stacks Project, Morphisms of Schemes, Definition 29.42.1
- Vakil, The Rising Sea, §11.3.1, printed p.249
- The Stacks Project, Morphisms of Schemes, Lemma 29.45.4 (tag 01WG) and Lemma 29.44.4
- Vakil, The Rising Sea, §8.3.6 and Exercise 8.3.M
- The Stacks Project, Morphisms of Schemes, Definition 29.51.1 (tag 01RO)
- The Stacks Project, Morphisms of Schemes, Lemma 29.51.5 (tag 0BAC)
- The Stacks Project, Varieties, Section 33.43 (tag 0A22), where a closed subset of a finite-type k-scheme of dimension at most 1 avoiding the generic point is used as finite
- Milne, Algebraic Geometry, Section 2m (chain dimension of Noetherian spaces)
- The Stacks Project, Morphisms of Schemes, Lemma 29.51.5 (tag 0BAC) and Definition 29.51.1 (tag 01RO)
- The Stacks Project, Varieties, Section 33.43 (tag 0A22)
- Ravi Vakil, The Rising Sea, 2011 public draft, §17.4 on curves
- The Stacks Project, Morphisms of Schemes, Lemma 29.44.5 (tag 01WC), proof step checking local finite type on the standard charts
- The Stacks Project, Constructions, Section 27.8 (tags 01M3, 01MD), the standard charts and quasi-compactness of projective space
- The Stacks Project, Morphisms of Schemes, Lemma 29.44.5 (tag 01WC) and Section 29.42 (tag 01W0), properness of projective space
- The Stacks Project, Constructions, Lemma 27.8.11 (tag 01MF), universally closedness of projective space
- Vakil, The Rising Sea, sections on proper and projective morphisms and the valuative criteria
- The Stacks Project, More on Morphisms, Situation 37.67.1 (tag 0ECI), Lemma 37.67.2 (tag 0ECJ) and Proposition 37.67.3 (tag 0E25)
- The Stacks Project, More on Morphisms, Lemma 37.14.1 (tag 0ET0), the affine case of the pushout
- Vakil, The Rising Sea, Sections 17.4.9-17.4.12 (gluing two schemes along isomorphic closed subschemes)
- Vakil, The Rising Sea, Sections 17.4.8-17.4.12 (gluing two schemes along isomorphic closed subschemes; the proper nonprojective example)
- Stacks Project, Descent, §35.23 (tag 02YJ)
- Stacks Project, Descent, Lemma 35.23.16 (tag 02L1)
- The Stacks Project, Morphisms of Schemes, Lemma 29.44.4 and Lemma 29.45.4 (tag 01WG)
- The Stacks Project, Morphisms of Schemes, Lemmas 29.20.1-29.20.3 (tag 01K2)
- The Stacks Project, Morphisms of Schemes, Lemma 29.45.5 (tag 01WG) and Lemma 29.44.4
- The Stacks Project, Morphisms of Schemes, Lemma 29.44.8 (tag 01WG) and Lemma 29.42.4
- Vakil, The Rising Sea, Exercise 11.1.18 and Section 11.3, printed p.232
- The Stacks Project, Morphisms of Schemes, Lemma 29.44.5 (tag 01WC) and Lemma 29.44.4
- Vakil, The Rising Sea, Section 17.4 and Exercise 11.3.F
- Stacks Project, Varieties, Lemma 33.9.3 (tag 0BUG)
- The Stacks Project, Varieties, Section 33.9 (global functions on proper varieties and morphisms to the affine line)
- Vakil, The Rising Sea, Sections 8.3 and 11.3