DefinitionDefinition: Literature-sourcedProof: Not applicablePipeline-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 objects, morphisms and properties

Definition

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 Existence of all scheme fibre products; the meaning of $S$ -morphism is Schemes and morphisms over a 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”.

Depends on

Used by

Euler characteristic in a proper flat family is locally constant Corollary
Nontrivial degree-zero line bundles have no sections Corollary
Upper semicontinuity of fibre cohomology dimensions Corollary
Nonflat base change of a blowup can fail Counterexample
The affine line is not proper Counterexample
Exceptional subscheme of a blowup Definition
Group schemes over a base scheme Definition
Open and universally open morphisms of schemes Definition
Scheme-theoretic fibre Definition
Universally closed morphisms Definition
Incidence projection has closed determinantal image Example
Affine charts after extension of the ground field Lemma
Base change and products of abelian schemes Lemma
Base change of immersions Lemma
Blowups restrict to open subschemes of the base Lemma
Closed immersions are affine quotients and survive base change Lemma
Étale stability Lemma
Fibres of a smooth morphism are smooth Lemma
Finite projective complex for proper flat coherent cohomology Lemma
Flatness is stable under arbitrary base change Lemma
Fpqc descent of properness components Lemma
Good reduction is stable under base change of the base Lemma
Iterated base change Lemma
Morphisms from a proper scheme to a separated one are proper Lemma
Properness survives composition Lemma
Relative very ampleness implies relative ampleness Lemma
Separatedness survives base change Lemma
The submersion criterion between smooth varieties Lemma
Universal finite projective cohomology complex over any base Lemma
Valuation lifts detect universal closedness Lemma
Cohomology and base change for proper flat coherent families Theorem
Flat base change for blowups, and failure without flatness Theorem
Flat finite-presentation morphisms are open Theorem
Proper morphisms are closed Theorem
Properness descends through fpqc base change Theorem
Relative Proj commutes with arbitrary base change Theorem
Smoothness survives base change and composition Theorem
Submersion criterion for locally standard smooth morphisms Theorem
The exceptional divisor is the projectivized normal cone Theorem

Dependency tree · two levels

6 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.18.1 and 26.18.3 (standard reference, not scraped)