LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generatedjudge pass (gpt-6.1-sol)

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.

A surjective ring map induces a closed immersion of affine spectra

Statement

Let $φ ⁣ : B \to A$ be a surjective homomorphism of commutative unital rings and let $I = \ker φ$ , so that $A ≅ B / I$ . Then the induced morphism $Spec φ ⁣ : Spec A \to Spec B$ (The map of affine spectra induced by a ring homomorphism, Affine schemes and their coordinate rings) is a closed immersion in the sense of Closed immersions of schemes: its underlying map is a homeomorphism onto the closed subset $V (I)$ , and the map $O_{Spec B} \to (Spec φ)_{*} O_{Spec A}$ is surjective. No choice principle is used.

Facts & Assumptions

[F1]

A morphism is a closed immersion exactly when its underlying map is a homeomorphism onto a closed subset and its structure-sheaf map is surjective. (Closed immersions of schemes)

[F2]

A ring homomorphism $ψ ⁣ : B \to A$ induces the morphism $Spec ψ ⁣ : Spec A \to Spec B$ whose underlying map is contraction of primes, and whose map on the basic open $D (b)$ is the localization $B_{b} \to A_{ψ (b)}$ ; these section maps are compatible with restrictions. (The map of affine spectra induced by a ring homomorphism)

[F3]

If $π ⁣ : B \to B / I$ is a quotient map, then contraction along $π$ is a homeomorphism from $Spec (B / I)$ onto the closed subset $V (I)$ . (Prime ideals of a quotient ring are exactly the prime ideals containing the ideal, The spectrum of a quotient is a closed subspace)

[F4]

The first isomorphism theorem identifies $A$ with $B / I$ through $φ$ . (First isomorphism theorem for rings: $R / \ker f ≅ im f$ )

[F5]

For a prime $p \in Spec B$ the stalk of the structure sheaf at $p$ is $B_{p}$ , the localization at the multiplicative set $B ∖ p$ . (Localisation at a prime ideal: $R_{p} = (R ∖ p)^{- 1} R$ , The stalk of the affine structure sheaf at a prime is A_p)

[F6]

Localizing a surjective module homomorphism at a multiplicative set gives a surjective homomorphism. (Surjective module maps remain surjective after localisation)

[F7]

A sequence of sheaves of abelian groups is exact if and only if it is exact on every stalk; in particular a morphism of sheaves is surjective if and only if all its stalk maps are surjective. (A sequence of abelian sheaves is exact exactly when it is exact on every stalk)

Proof

Given: A surjective unital ring homomorphism $φ ⁣ : B \to A$ with $I = \ker φ$ , and the identification $A ≅ B / I$ from [F4].

1.1F2F3F4

Replacing $A$ by $B / I$ along the isomorphism of [F4], the morphism $Spec φ$ is the contraction map $Spec (B / I) \to Spec B$ of [F2], which by [F3] is a homeomorphism onto the closed subset $V (I)$ .

1.2F2F5F6

At a prime $p \supseteq I$ of $B$ , the sections of the direct image $(Spec φ)_{*} O_{Spec A}$ over a basic open $D (b) ∋ p$ are $A_{φ (b)} = (B / I)_{φ (b)}$ by [F2], and the basic opens $D (b) ∋ p$ are cofinal among the neighbourhoods of $p$ ; hence the stalk of the direct image at $p$ is $(B / I)_{p}$ , with stalk map $B_{p} \to (B / I)_{p}$ induced by localizing $φ$ at $B ∖ p$ . Localization of the surjection $φ$ at each multiplicative set is surjective by [F6], so this stalk map is surjective, and the identification of the source stalk is [F5].

1.3F2F5F6

At a prime $p ⊉ I$ of $B$ , choose $u \in I ∖ p$ ; then $D (u) ∋ p$ and the sections of the direct image over $D (u)$ are $(B / I)_{φ (u)} = (B / I)_{0} = 0$ , because $φ (u) = 0$ becomes invertible in the localization. Every smaller basic open containing $p$ also lies in $D (u)$ and has zero sections, so the stalk of the direct image at $p$ is the zero ring and the stalk map is surjective trivially.

2.1F1F7step 1.1step 1.2step 1.3∎

Steps 1.2 and 1.3 compute every stalk of the structure-sheaf map $O_{Spec B} \to (Spec φ)_{*} O_{Spec A}$ and show each is surjective, so by the stalk criterion [F7] the sheaf map is surjective. With the homeomorphism onto $V (I)$ from step 1.1, [F1] makes $Spec φ$ a closed immersion. Only the first isomorphism theorem, localizations of the given surjection and the stalk criterion were used, all applied to structures already determined by $φ$ ; no choice principle is used.

Depends on

Used by

Dependency tree · two levels

37 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

J. S. Milne, Algebraic Groups (corrected 2022 printing, Cambridge University Press) (standard reference, not scraped)
J. Swanson (notes), J. Pevtsova (lecturer), Algebraic Groups Lecture Notes, University of Washington, Fall 2014 (standard reference, not scraped)