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.
Morphisms from a proper scheme to a separated one are proper
Statement
Assume the Axiom of Choice. Let be proper and let be separated. Then every -morphism is proper. No Noetherian, reducedness or nonemptiness hypothesis is used, and the empty source is included.
Facts & Assumptions
Given: The Axiom of Choice, a proper morphism , a separated morphism and an -morphism .
A morphism is proper if and only if it is separated, of finite type and universally closed. (Proper morphisms)
A morphism is separated exactly when its diagonal is a closed immersion. (Separated morphism of schemes)
For an -morphism the graph morphism is ; its first projection is the identity and its second projection is , and the definition alone does not assert that its image is closed. (The graph morphism over a base)
For an -morphism , with , the square with top arrow , bottom arrow , left arrow and right arrow is Cartesian; thus is the base change of along . (The graph is a pullback of the diagonal)
Assume AC. Every base change of a closed immersion is a closed immersion. (Closed immersions are affine quotients and survive base change)
Assume AC. Every closed immersion is finite, hence proper; the empty closed immersion is included. (Closed immersions are proper)
For a morphism and an -scheme , the base change is with structure map the second projection. (Base change of objects, morphisms and properties)
Assume AC. Properness survives arbitrary base change. (Properness survives arbitrary base change)
Assume AC. A composite of proper morphisms is proper. (Properness survives composition)
The Axiom of Choice states that every family of nonempty sets has a choice function. (The Axiom of Choice)
Proof
Since is separated, [F2] makes the diagonal a closed immersion.
Let be the second projection. By [F7] the fibre product with its projection to is the base change of along ; since is proper, the AC-qualified [F8] makes proper.
Put , and let be the graph of . By [F4] the square with top arrow , bottom arrow , left arrow and right arrow is Cartesian, so is the base change of along . By step 1.1 the diagonal is a closed immersion, so the AC-qualified [F5] makes a closed immersion.
By [F3] the second projection of the graph is , so .
By the AC-qualified [F6] the closed immersion is finite, hence proper.
Thus is the composite of the proper morphism of step 3.1 with the proper morphism of step 1.2; by the AC-qualified [F9] the -morphism is proper.
The Axiom of Choice [F10] is assumed and is used only through the four AC-qualified suppliers [F5], [F6], [F8] and [F9], in steps 2.1, 3.1, 1.2 and 4.1; the diagonal, graph and pullback identifications of steps 1.1, 2.1 and 2.2 are choice-free. If then and are empty morphisms and the same steps apply, the cited results allowing the empty fibred and zero-ring charts; if then because maps into ; if then and , so the conclusion is the properness of itself. No Noetherian, reducedness or nonemptiness hypothesis is used.
Depends on
Proper morphisms
Separated morphism of schemes
The graph morphism over a base
The graph is a pullback of the diagonal
Closed immersions are affine quotients and survive base change
Closed immersions are proper
Base change of objects, morphisms and properties
Properness survives arbitrary base change
Properness survives composition
The Axiom of Choice