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.1F1F4F5given

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.

1.2given

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$ .

1.3F2F6F8

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].

1.4F3F7F9

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.

2.1F7step 1.2

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.

2.2step 1.4

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].

3.1step 1.3step 1.4step 2.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.

4.1step 1.1step 3.1step 2.2∎

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

Depends on

Dependency tree · 2 levels

Sources

The Stacks Project, Morphisms of Schemes, Section 29.15 and Schemes, Section 26.23.8, printed pp.61, 48