Schematic density and separated targets

Morphisms over a base into a separated scheme are determined by their restriction along a scheme-theoretically dominant morphism. Unlike the corresponding statement for topologically dominant morphisms, this requires no reducedness hypothesis on the source. In particular, it applies to flat models with a possibly nonreduced generic fibre.

The equalizer argument extends Mathlib's AlgebraicGeometry.ext_of_isDominant_of_isSeparated, by Christian Merten and Andrew Yang: schematic density makes the closed equalizer the entire source as a scheme, not just as a space.

theorem TauCeti.ext_of_isSchemeTheoreticallyDominant {W X Y S : AlgebraicGeometry.Scheme} (ι : W ⟶ X) [AlgebraicGeometry.IsSchemeTheoreticallyDominant ι] {f g : X ⟶ Y} (s : Y ⟶ S) [AlgebraicGeometry.IsSeparated s] (h : CategoryTheory.CategoryStruct.comp f s = CategoryTheory.CategoryStruct.comp g s) (hι : CategoryTheory.CategoryStruct.comp ι f = CategoryTheory.CategoryStruct.comp ι g) : f = g

Two morphisms into a separated scheme over a base agree if they agree after precomposition with a scheme-theoretically dominant morphism. The source need not be reduced.