TheoremStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-sol)audited 2026-09-27

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.

Immersions are monomorphisms locally of finite type

Statement

Every immersion of schemes is a monomorphism and is locally of finite type, and is therefore separated as a morphism. No finite presentation is claimed: for a closed immersion given by a non-finitely-generated ideal the argument supplies only finite type.

Facts & Assumptions

Given: An immersion $f : Z \to X$ of schemes with a factorization $f = j \circ i$ into a closed immersion $i : Z \to U$ and an open immersion $j : U ↪ X$ .

[F1]

An immersion is a morphism factoring as a closed immersion into an open subscheme of its target. (Immersion of schemes)

[F2]

An open immersion identifies its source isomorphically with an open subscheme of its target. (Open immersions of schemes)

[F3]

A closed immersion has underlying map a homeomorphism onto a closed subset and surjective structure map. (Closed immersions of schemes)

[F4]

Open immersions and closed immersions are monomorphisms of schemes, and any composite of these is a monomorphism; monomorphism means injectivity of the induced map on morphism sets. (Immersions and affine localizations are monomorphisms)

[F5]

A monomorphism $j : X \to Y$ is separated, its diagonal $Δ_{X / Y}$ being an isomorphism. (Monomorphisms and diagonals)

[F6]

A morphism is locally of finite type when every point of the source has an affine open neighbourhood mapping into an affine open of the target over which the corresponding ring map is of finite type. (Locally finite type and finite type morphisms)

[F7]

Being locally of finite type is affine-local on source and target. (Finite type is affine-local on source and target)

[F8]

Every point of a scheme has an open neighbourhood which, with the restricted structure sheaf, is an affine scheme; hence the affine open subschemes form a basis of the topology. (Schemes)

[F9]

For a ring $A$ , closed immersions $Z \to Spec A$ are, up to unique isomorphism over $Spec A$ , precisely the morphisms $Spec (A / I) \to Spec A$ for ideals $I \subseteq A$ . (Closed immersions into affine schemes are quotient spectra)

Proof

technique · direct

1.1

The composite $f = j \circ i$ of the open immersion $j$ and the closed immersion $i$ is a monomorphism by [F4]; hence by [F5] the morphism $f$ is separated.

F1F4F5given

1.2

If $A \to B$ and $B \to C$ are ring maps of finite type, then $A \to C$ is of finite type: choosing finitely many generators of $B$ over $A$ and of $C$ over $B$ , their union generates $C$ over $A$ .

given

1.3

An open immersion $j$ is locally of finite type: by [F2] it identifies its source with an open subscheme of the target, so a point $u$ of the source lies in some affine open $Spec A \subseteq X$ contained in the image of $j$ , by [F8]; then $j^{- 1} (Spec A)$ is an affine open neighbourhood of $u$ carrying an isomorphism onto $Spec A$ via $j$ , and the corresponding ring map is the identity of $A$ , which is of finite type by [F6].

F2F6F8

1.4

A closed immersion is locally of finite type: for a point of its source choose an affine open $Spec A \subseteq X$ containing its image; the restriction $i^{- 1} (Spec A) \to Spec A$ again has underlying map a homeomorphism onto a closed subset and surjective structure map, so is a closed immersion by [F3], hence is $Spec (A / I) \to Spec A$ for some ideal $I \subseteq A$ by [F9]; the map $A \to A / I$ is generated as an $A$ -algebra by the class of $1$ , hence of finite type, with [F7] giving the general case.

F3F7F9

2.1

Applying step 1.2 fibrewise over a common affine chart and using locality [F7], the composite of two morphisms that are locally of finite type is locally of finite type.

F7step 1.2

2.2

The argument for the closed immersion used only that $A \to A / I$ is generated by one element, so it gives finite type and not finite presentation; the ideal $I$ is not assumed finitely generated, and no finite presentation of $f$ should be read off from [F6].

step 1.4

3.1

By steps 1.3 and 1.4 both $i$ and $j$ are locally of finite type, so their composite $f$ is locally of finite type by step 2.1.

step 1.3step 1.4step 2.1

4.1

Steps 1.1 and 3.1 show that $f$ is a monomorphism, locally of finite type and separated, which is the assertion.

step 1.1step 3.1step 2.2∎

Depends on

Used by

Open and closed immersions are separated Lemma

Dependency tree · two levels

26 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

The Stacks Project, Morphisms of Schemes, Section 29.15 and Schemes, Section 26.23.8, printed pp.61, 48 (standard reference, not scraped)