Schematic density of the generic fibre

For a flat scheme over a commutative ring, scalar extension along an injective algebra map is scheme-theoretically dominant. For a domain and its fraction field, this is the canonical generic-fibre inclusion. Consequently, two morphisms into a separated target agree whenever their restrictions to this fibre agree. Neither reducedness nor finite presentation of the source is needed.

This is the density argument used for uniqueness of extensions on flat models over valuation rings; see Q. Liu, Algebraic Geometry and Arithmetic Curves, §4.3. The construction uses Mathlib's stability of schematic dominance under flat base change.

theorem TauCeti.isSchemeTheoreticallyDominant_genericFiberι (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X : AlgebraicGeometry.Scheme} (hRK : Function.Injective ⇑(algebraMap R K)) (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) [AlgebraicGeometry.Flat toBase] : AlgebraicGeometry.IsSchemeTheoreticallyDominant (genericFiberι R K toBase)

Scalar extension of a flat scheme along an injective algebra map is schematically dominant. For a domain and its fraction field, the generic fibre is schematically dense in the total space.

theorem TauCeti.ext_of_genericFiberι_eq (R K : Type u) [CommRing R] [CommRing K] [Algebra R K] {X Y : AlgebraicGeometry.Scheme} (hRK : Function.Injective ⇑(algebraMap R K)) (toBase : X ⟶ AlgebraicGeometry.Spec ↧R) [AlgebraicGeometry.Flat toBase] (s : Y ⟶ AlgebraicGeometry.Spec ↧R) [AlgebraicGeometry.IsSeparated s] {f g : X ⟶ Y} (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (hK : CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) f = CategoryTheory.CategoryStruct.comp (genericFiberι R K toBase) g) : f = g

Morphisms over a ring from a flat source to a separated target are determined by their restriction after an injective scalar extension. In particular the source need not be reduced.