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.

Base change of immersions

Statement

Open immersions, closed immersions and immersions (equivalently locally closed immersions) remain of the same kind after arbitrary base change. If a closed subscheme $Z ↪ S$ has ideal sheaf $I$ , its pullback under $g : Y \to S$ has ideal $Im (g^{*} I ⟶ O_{Y}) .$ On affine charts $A \to C$ this is the extended ideal $I C$ . No injectivity of $g^{*} I \to O_{Y}$ is asserted.

Facts & Assumptions

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

[F1]

Let $h : S^{'} \to S$ . For an $S$ -scheme $f : X \to S$ , its base change is $X_{S^{'}} = X \times_{S} S^{'}$ , with structure map the second projection. For an $S$ -morphism $u : X \to Y$ , define $u_{S^{'}} : X_{S^{'}} \to Y_{S^{'}}$ by its projections $u \circ {pr}_{X}$ and ${pr}_{S^{'}}$ . Existence and uniqueness follow from thm-fibre-products-of-schemes-exist; the meaning of $S$ -morphism is def-scheme-over-base. These formulas preserve identities and composition because their projections do, so they define a functor. A property of morphisms is stable under arbitrary base change when every pullback of a morphism with that property again has it. No restriction such as flatness is implicit in “arbitrary”. (Base change of objects, morphisms and properties)

[F2]

Suppose $P = X \times_{S} Y$ exists, with projections $p, q$ . If opens $V \subseteq X$ , $W \subseteq Y$ map into an open $U \subseteq S$ , then the open subscheme $Q = p^{- 1} (V) \cap q^{- 1} (W)$ represents $V \times_{U} W$ , and also $V \times_{S} W$ . Independently, for $f : X \to S$ and an open $U \subseteq S$ , the open subscheme $f^{- 1} (U)$ represents $X \times_{S} U$ . (Restricting fibre products to open subschemes)

[F3]

Let $A \to C$ be a unital ring map. For any set of variables $(t_{i})$ and any ideal $I \subseteq A [t_{i}]$ , $(A [t_{i}] / I) \otimes_{A} C ≅ C [t_{i}] / I C [t_{i}] .$ Here the extended ideal is generated by the coefficient images of all elements of $I$ . For a multiplicative subset $M \subseteq A$ , $(M^{- 1} A) \otimes_{A} C ≅ {\overline{M}}^{- 1} C .$ These are ring isomorphisms; no flatness, finite-generation or nonzero-ring hypothesis is required. (Presentations and localization under base extension)

[F4]

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

1.1

For an open immersion, F2 identifies its pullback with an open inverse image, proving the assertion including the empty and full open.

givenF2

1.2

For a closed immersion, F4 describes it over $Spec A$ as $Spec (A / I)$ . Over a compatible affine chart $Spec C$ of the new base, F3 gives the pullback ring $C / I C$ . By F4 this is a closed immersion; these local descriptions glue because restriction localizes both the quotient and its extended ideal. The ideal is exactly the image of the pulled-back ideal sheaf.

F3F4algebra

2.1

An immersion factors as a closed immersion into an open subscheme. Pull back the two stages and apply the preceding two steps; directly, a test pair factors through the intermediate pullback, so their composite is the pullback immersion. For an $S$ -morphism $X \to Y$ , F1 identifies its scalar extension with the pullback along $Y_{S^{'}} \to Y$ , by the same compatible-pair check. Thus this case is covered too. Every immersion is injective on underlying points, being a composite of two subspace inclusions; its arbitrary base changes are immersions by this argument, hence are also injective.

F1step 1.1step 1.2

3.1

The ideal cases $I = 0$ and $I = A$ give the full and empty closed subschemes. Local principality also survives, since the image ideal of $(a)$ is $(g^{*} a)$ . Regularity of the generator does not follow: for $A = k [t]$ , $I = (t)$ and $C = A / (t)$ , the nonzero module $I \otimes_{A} C ≅ C$ maps to zero in $C$ . Thus the image qualification is necessary without flatness.

step 1.2algebra∎

Depends on

Used by

Scheme-theoretic inverse images of subschemes Definition

Dependency tree · two levels

16 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

Stacks 26.17.6 and 26.18.2 (standard reference, not scraped)