LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-07

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 and affine localizations are monomorphisms

Statement

Open immersions, closed immersions, and localization morphisms $Spec (M^{- 1} A) \to Spec A$ are monomorphisms of schemes. Any composite of these, in particular a locally closed immersion, is a monomorphism. Here monomorphism means that for every scheme $T$ the induced map on sets of morphisms from $T$ is injective.

Facts & Assumptions

Given: The objects, hypotheses and conventions in the statement above.

[F1]

An open immersion is a monomorphism of schemes, and a composite of open immersions is an open immersion. (Open immersions are monomorphisms)

[F2]

For a scheme $X$ and a ring $A$ , taking global sections induces a natural bijection $Hom (X, Spec A) ≅ {Hom}_{C R i n g} (A, Γ (X, O_{X})) .$ (Morphisms to an affine scheme and global sections)

[F3]

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)

[F4]

Compatible morphisms of schemes on an open cover of a scheme $X$ glue uniquely to a morphism from $X$ ; two morphisms out of $X$ are equal if their restrictions to an open cover are equal. Both assertions may be checked after affine-open refinement of source and target. (Morphisms of schemes are local on compatible open covers)

Proof

1.1

Open immersions are monomorphisms by F1. For an affine localization, F2 identifies maps from arbitrary $T$ into its source with ring maps $M^{- 1} A \to Γ (T, O_{T})$ . Such a map, when it exists, is uniquely determined by its restriction to $A$ , because every fraction must map to the image of its numerator times the inverse image of its denominator. This includes localization at zero.

givenF1F2

1.2

For an affine closed immersion, F3 gives $Spec (A / I) \to Spec A$ . By F2 a map out of $A / I$ is uniquely determined by its composite with the surjection $A \to A / I$ . For a general closed immersion and two lifts of the same $T \to X$ , cover $T$ by inverse images of affine opens of $X$ . The affine uniqueness just proved makes the lifts equal on that cover, hence globally by F4. This includes $I = 0, (1)$ and arbitrary nilpotent ideals.

F2F3F4

2.1

If $j$ and $i$ are monomorphisms and $j i α = j i β$ , cancel $j$ and then $i$ to obtain $α = β$ . This proves the composite assertion; a locally closed immersion has the indicated open/closed factorization. Empty test schemes and identity maps meet the same uniqueness condition.

step 1.1step 1.2algebra∎

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

12 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

Vakil 10.2.G (standard reference, not scraped)